Removed hash size proofs

Author: Soupstraw

eras/alonzo/impl/src/Cardano/Ledger/Alonzo/TxOut.hs

@@ -12,7 +12,6 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE ViewPatterns #-}
@@ -82,11 +81,10 @@ import Data.Aeson (ToJSON (..), object, (.=))
 import qualified Data.Aeson as Aeson (Value (Null, String))
 import Data.Bits
 import Data.Maybe (fromMaybe)
-import Data.Typeable (Proxy (..), (:~:) (Refl))
+import Data.Typeable (Proxy (..))
 import Data.Word
 import GHC.Generics (Generic)
 import GHC.Stack (HasCallStack)
-import GHC.TypeLits
 import Lens.Micro
 import NoThunks.Class (InspectHeapNamed (..), NoThunks)
 
@@ -116,7 +114,6 @@ decodeAddress28 ::
   Addr28Extra ->
   Maybe Addr
 decodeAddress28 stakeRef (Addr28Extra a b c d) = do
-  Refl <- sameNat (Proxy @(SizeHash ADDRHASH)) (Proxy @28)
   let network = if d `testBit` 1 then Mainnet else Testnet
       paymentCred =
         if d `testBit` 0
@@ -163,7 +160,6 @@ decodeDataHash32 ::
   DataHash32 ->
   Maybe DataHash
 decodeDataHash32 (DataHash32 a b c d) = do
-  Refl <- sameNat (Proxy @(SizeHash HASH)) (Proxy @32)
   Just $! unsafeMakeSafeHash $ hashFromPackedBytes $ PackedBytes32 a b c d
 
 viewCompactTxOut ::
@@ -213,7 +209,7 @@ deriving via InspectHeapNamed "AlonzoTxOut" (AlonzoTxOut era) instance NoThunks
 encodeAddress28 ::
   Network ->
   PaymentCredential ->
-  Maybe (SizeHash ADDRHASH :~: 28, Addr28Extra)
+  Addr28Extra
 encodeAddress28 network paymentCred = do
   let networkBit, payCredTypeBit :: Word64
       networkBit =
@@ -226,26 +222,28 @@ encodeAddress28 network paymentCred = do
           ScriptHashObj {} -> 0
       encodeAddr ::
         Hash ADDRHASH a ->
-        Maybe (SizeHash ADDRHASH :~: 28, Addr28Extra)
+        Addr28Extra
       encodeAddr h = do
-        refl@Refl <- sameNat (Proxy @(SizeHash ADDRHASH)) (Proxy @28)
         case hashToPackedBytes h of
           PackedBytes28 a b c d ->
             let d' = (fromIntegral d `shiftL` 32) .|. networkBit .|. payCredTypeBit
-             in Just (refl, Addr28Extra a b c d')
-          _ -> Nothing
+             in Addr28Extra a b c d'
+          _ ->
+            -- This case should never match, but if it does, we output garbage
+            Addr28Extra 0 0 0 0
   case paymentCred of
     KeyHashObj (KeyHash addrHash) -> encodeAddr addrHash
     ScriptHashObj (ScriptHash addrHash) -> encodeAddr addrHash
 
 encodeDataHash32 ::
   DataHash ->
-  Maybe (SizeHash HASH :~: 32, DataHash32)
+  DataHash32
 encodeDataHash32 dataHash = do
-  refl@Refl <- sameNat (Proxy @(SizeHash HASH)) (Proxy @32)
   case hashToPackedBytes (extractHash dataHash) of
-    PackedBytes32 a b c d -> Just (refl, DataHash32 a b c d)
-    _ -> Nothing
+    PackedBytes32 a b c d -> DataHash32 a b c d
+    _ ->
+      -- This case should never match, but if it does, we output garbage
+      DataHash32 0 0 0 0
 
 getAdaOnly ::
   forall era.
@@ -269,15 +267,16 @@ pattern AlonzoTxOut addr vl dh <-
   where
     AlonzoTxOut (Addr network paymentCred stakeRef) vl SNothing
       | StakeRefBase stakeCred <- stakeRef
-      , Just adaCompact <- getAdaOnly (Proxy @era) vl
-      , Just (Refl, addr28Extra) <- encodeAddress28 network paymentCred =
-          TxOut_AddrHash28_AdaOnly stakeCred addr28Extra adaCompact
+      , Just adaCompact <- getAdaOnly (Proxy @era) vl =
+        let addr28Extra = encodeAddress28 network paymentCred
+         in TxOut_AddrHash28_AdaOnly stakeCred addr28Extra adaCompact
     AlonzoTxOut (Addr network paymentCred stakeRef) vl (SJust dh)
       | StakeRefBase stakeCred <- stakeRef
-      , Just adaCompact <- getAdaOnly (Proxy @era) vl
-      , Just (Refl, addr28Extra) <- encodeAddress28 network paymentCred
-      , Just (Refl, dataHash32) <- encodeDataHash32 dh =
-          TxOut_AddrHash28_AdaOnly_DataHash32 stakeCred addr28Extra adaCompact dataHash32
+      , Just adaCompact <- getAdaOnly (Proxy @era) vl =
+        let
+          addr28Extra = encodeAddress28 network paymentCred
+          dataHash32 = encodeDataHash32 dh
+         in TxOut_AddrHash28_AdaOnly_DataHash32 stakeCred addr28Extra adaCompact dataHash32
     AlonzoTxOut addr vl mdh =
       let v = fromMaybe (error $ "Illegal value in TxOut: " ++ show vl) $ toCompact vl
           a = compactAddr addr

eras/babbage/impl/src/Cardano/Ledger/Babbage/TxOut.hs

@@ -114,7 +114,7 @@ import Data.Aeson (KeyValue, ToJSON (..), object, pairs, (.=))
 import qualified Data.ByteString.Lazy as LBS
 import Data.Maybe (fromMaybe)
 import qualified Data.Text as T
-import Data.Typeable (Proxy (..), (:~:) (Refl))
+import Data.Typeable (Proxy (..))
 import GHC.Generics (Generic)
 import GHC.Stack (HasCallStack)
 import Lens.Micro (Lens', lens, to, (^.))
@@ -379,16 +379,18 @@ mkTxOut ::
 mkTxOut addr _cAddr vl NoDatum SNothing
   | Just adaCompact <- getAdaOnly (Proxy @era) vl
   , Addr network paymentCred stakeRef <- addr
-  , StakeRefBase stakeCred <- stakeRef
-  , Just (Refl, addr28Extra) <- encodeAddress28 network paymentCred =
-      TxOut_AddrHash28_AdaOnly stakeCred addr28Extra adaCompact
+  , StakeRefBase stakeCred <- stakeRef =
+    let
+      addr28Extra = encodeAddress28 network paymentCred
+     in TxOut_AddrHash28_AdaOnly stakeCred addr28Extra adaCompact
 mkTxOut addr _cAddr vl (DatumHash dh) SNothing
   | Just adaCompact <- getAdaOnly (Proxy @era) vl
   , Addr network paymentCred stakeRef <- addr
-  , StakeRefBase stakeCred <- stakeRef
-  , Just (Refl, addr28Extra) <- encodeAddress28 network paymentCred
-  , Just (Refl, dataHash32) <- encodeDataHash32 dh =
-      TxOut_AddrHash28_AdaOnly_DataHash32 stakeCred addr28Extra adaCompact dataHash32
+  , StakeRefBase stakeCred <- stakeRef =
+    let
+      addr28Extra = encodeAddress28 network paymentCred
+      dataHash32 = encodeDataHash32 dh
+    in TxOut_AddrHash28_AdaOnly_DataHash32 stakeCred addr28Extra adaCompact dataHash32
 mkTxOut _addr cAddr vl d rs =
   let cVal = fromMaybe (error ("Illegal Value in TxOut: " ++ show vl)) $ toCompact vl
    in case rs of