Fix type and constraint errors

IntersectMBO · Jun 27, 2024 · 6ba21a1 · 6ba21a1
1 parent 5f1bf80
commit 6ba21a1
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 64 deletions.
diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -26,7 +25,7 @@ module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway (
 ) where
 
 import Cardano.Crypto.DSIGN (DSIGNAlgorithm (..), SignedDSIGN (..))
-import Cardano.Crypto.Hash (Hash, hashToBytes)
+import Cardano.Crypto.Hash (Hash)
 import Cardano.Crypto.Util (bytesToNatural)
 import Cardano.Ledger.Address (Addr (..), RewardAccount (..), serialiseAddr)
 import Cardano.Ledger.Alonzo (AlonzoTxAuxData, MaryValue)
@@ -103,7 +102,6 @@ import qualified Data.VMap as VMap
 import Data.Void (Void, absurd)
 import Data.Word (Word32, Word64)
 import GHC.Generics (Generic)
-import GHC.TypeLits
 import Lens.Micro
 import Lens.Micro.Extras (view)
 import qualified Lib as Agda
@@ -1192,17 +1190,8 @@ instance HasSimpleRep (EpochExecEnv era)
 instance (IsConwayUniv fn, Era era) => HasSpec fn (EpochExecEnv era)
 
 instance SpecTranslate ctx (EpochExecEnv era) where
-  type SpecRep (EpochExecEnv era) = Agda.NewEpochEnv
-
-  toSpecRep (EpochExecEnv stakeDistr) = do
-    let
-      transStakeDistr (c, s) = do
-        c' <- toSpecRep c
-        s' <- toSpecRep s
-        pure (Agda.CredVoter Agda.SPO c', s')
-      stakeDistrsMap = traverse transStakeDistr $ Map.toList stakeDistr
-      stakeDistrs = Agda.MkStakeDistrs . Agda.MkHSMap <$> stakeDistrsMap
-    Agda.MkNewEpochEnv <$> stakeDistrs
+  type SpecRep (EpochExecEnv era) = ()
+  toSpecRep _ = pure ()
 
 data ConwayExecEnactEnv era = ConwayExecEnactEnv
   { ceeeGid :: GovActionId (EraCrypto era)
@@ -1292,15 +1281,12 @@ instance
   , ToExpr (PParamsHKD StrictMaybe era)
   , SpecRep (TxOut era) ~ Agda.TxOut
   , SpecTranslate ctx (TxOut era)
-  , ProtVerLow era <= ProtVerHigh era
-  , MinVersion <= ProtVerLow era
-  , MinVersion <= ProtVerHigh era
   ) =>
   SpecTranslate ctx (EpochState era)
   where
   type SpecRep (EpochState era) = Agda.EpochState
 
-  toSpecRep (EpochState {esLState = esLState@LedgerState {..}, ..}) =
+  toSpecRep (EpochState {esLState = esLState@LedgerState {lsUTxOState}, ..}) =
     Agda.MkEpochState
       <$> toSpecRep esAccountState
       <*> toSpecRep esSnapshots
@@ -1311,21 +1297,8 @@ instance
       enactState = mkEnactState $ utxosGovState lsUTxOState
       ratifyState = RatifyState enactState mempty mempty False
 
-instance
-  ( EraPParams era
-  , ConwayEraGov era
-  , SpecTranslate ctx (PParamsHKD Identity era)
-  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
-  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
-  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
-  , Inject ctx [GovActionState era]
-  , ToExpr (PParamsHKD StrictMaybe era)
-  , SpecRep (TxOut era) ~ Agda.TxOut
-  , SpecTranslate ctx (TxOut era)
-  ) =>
-  SpecTranslate ctx (SnapShots era)
-  where
-  type SpecRep (SnapShots era) = Agda.Snapshots
+instance SpecTranslate ctx (SnapShots c) where
+  type SpecRep (SnapShots c) = Agda.Snapshots
 
   toSpecRep (SnapShots {..}) =
     Agda.MkSnapshots
@@ -1334,42 +1307,16 @@ instance
       <*> toSpecRep ssStakeGo
       <*> toSpecRep ssFee
 
-instance
-  ( EraPParams era
-  , ConwayEraGov era
-  , SpecTranslate ctx (PParamsHKD Identity era)
-  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
-  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
-  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
-  , Inject ctx [GovActionState era]
-  , ToExpr (PParamsHKD StrictMaybe era)
-  , SpecRep (TxOut era) ~ Agda.TxOut
-  , SpecTranslate ctx (TxOut era)
-  ) =>
-  SpecTranslate ctx (SnapShot era)
-  where
-  type SpecRep (SnapShot era) = Agda.Snapshot
+instance SpecTranslate ctx (SnapShot c) where
+  type SpecRep (SnapShot c) = Agda.Snapshot
 
   toSpecRep (SnapShot {..}) =
     Agda.MkSnapshot
       <$> toSpecRep ssStake
       <*> toSpecRep (VMap.toMap ssDelegations)
 
-instance
-  ( EraPParams era
-  , ConwayEraGov era
-  , SpecTranslate ctx (PParamsHKD Identity era)
-  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
-  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
-  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
-  , Inject ctx [GovActionState era]
-  , ToExpr (PParamsHKD StrictMaybe era)
-  , SpecRep (TxOut era) ~ Agda.TxOut
-  , SpecTranslate ctx (TxOut era)
-  ) =>
-  SpecTranslate ctx (Stake era)
-  where
-  type SpecRep (Stake era) = Agda.HSMap Agda.Credential Agda.Coin
+instance SpecTranslate ctx (Stake c) where
+  type SpecRep (Stake c) = Agda.HSMap Agda.Credential Agda.Coin
 
   toSpecRep (Stake stake) = toSpecRep $ VMap.toMap stake
 

diff --git a/libs/cardano-ledger-core/src/Cardano/Ledger/Keys/Internal.hs b/libs/cardano-ledger-core/src/Cardano/Ledger/Keys/Internal.hs
@@ -226,7 +226,8 @@ hashSignature = Hash.hashWith (DSIGN.rawSerialiseSigDSIGN . coerce)
 --------------------------------------------------------------------------------
 
 -- | Discriminated hash of public Key
-newtype KeyHash (discriminator :: KeyRole) c = KeyHash {unKeyHash :: Hash.Hash (ADDRHASH c) (DSIGN.VerKeyDSIGN (DSIGN c))}
+newtype KeyHash (discriminator :: KeyRole) c = KeyHash
+  {unKeyHash :: Hash.Hash (ADDRHASH c) (DSIGN.VerKeyDSIGN (DSIGN c))}
   deriving (Show, Eq, Ord)
   deriving newtype (NFData, NoThunks, Generic)