Replace a call to error in our FFI with a safe alternative (#650)

* Replace a call to `error` in our FFI with a safe alternative

There was no need to be unsafe here. Our code just happened to not
match on that proof, but this could have broken at any time when doing
refactoring. In the Consensus spec, this actually caused a crash.

* Update src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda

Co-authored-by: Joosep Jääger <joosep.jaager@gmail.com>

---------

Co-authored-by: Joosep Jääger <joosep.jaager@gmail.com>

Author: WhatisRT

src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda

@@ -22,9 +22,9 @@ instance
       { Implementation
       ; isSigned         = λ a b m → extIsSigned (HSVKey.hvkVKey a) b m ≡ true
       ; sign             = λ _ _ → zero
-        -- we can't prove these properties since the functions are provided by the Haskell implementation
+        -- we can't prove correctness since the function is provided by the Haskell implementation
       ; isSigned-correct = error "isSigned-correct evaluated"
-      ; Dec-isSigned     = λ { {vk} {ser} {sig} → ⁇ (extIsSigned (HSVKey.hvkVKey vk) ser sig because error "Dec-isSigned evaluated") }
+      ; Dec-isSigned     = ⁇ (_ ≟ _)
       }
 
 -- No P2 scripts for now