fix redundant IsConwayUniv constraint in GHC 8

IntersectMBO · Oct 11, 2024 · f4845e0 · f4845e0
1 parent 3e8efb9
commit f4845e0
Showing 1 changed file with 14 additions and 10 deletions.
diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/TxBodySpec.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/TxBodySpec.hs
@@ -35,11 +35,13 @@ import Data.Foldable (toList)
 import qualified Data.Map as Map
 import Data.Map.Strict (Map)
 import Data.Sequence.Internal (Seq)
-import Test.Cardano.Ledger.Constrained.Conway.Cert (EraCert (..))
+-- , certStateSpec)
+
+import Test.Cardano.Ledger.Constrained.Conway.Cert (EraCert (..), certStateSpec)
 import Test.Cardano.Ledger.Constrained.Conway.Certs (certsEnvSpec, projectEnv)
 import Test.Cardano.Ledger.Constrained.Conway.Instances
 import Test.Cardano.Ledger.Constrained.Conway.InstancesTxBody ()
-import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs (EraLedger (..), certStateSpec)
+import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs (EraLedger (..))
 import Test.Cardano.Ledger.Generic.PrettyCore (PrettyA (..))
 
 -- import qualified Test.Cardano.Ledger.Generic.Proof as Proof
@@ -50,7 +52,7 @@ import Prelude hiding (seq)
 -- Move these to the MapSpec
 
 subMap ::
-  (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v, IsConwayUniv fn) =>
+  (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
   Specification fn (Map k v, Map k v)
 subMap = constrained $ \ [var|pair|] ->
   match pair $ \ [var|sub|] [var|super|] ->
@@ -62,7 +64,7 @@ subMap = constrained $ \ [var|pair|] ->
     ]
 
 subMapSubDependsOnSuper ::
-  (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v, IsConwayUniv fn) =>
+  (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
   Term fn (Map k v) ->
   Term fn (Map k v) ->
   Pred fn
@@ -76,7 +78,7 @@ subMapSubDependsOnSuper sub super =
     ]
 
 subMapSuperDependsOnSub ::
-  (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v, IsConwayUniv fn) =>
+  (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
   Term fn (Map k v) ->
   Term fn (Map k v) ->
   Pred fn
@@ -143,14 +145,14 @@ bodyspec ::
     )
 bodyspec utxo certsenv certstate =
   constrained' $ \ [var|shelleyBody|] [var|inputUtxo|] [var|feeInput|] ->
-    match shelleyBody $ {- \tuple ->
-                        match tuple $  -}
+    match shelleyBody $
       \ [var|inputs|] [var|outputs|] [var|certs|] [var|rewAcct|] [var|fee|] _ [var|update|] _ ->
         [ dependsOn shelleyBody fee
         , dependsOn shelleyBody inputs
         , dependsOn shelleyBody outputs
         , dependsOn feeInput inputUtxo
         , dependsOn inputs inputUtxo
+        , dependsOn outputs inputUtxo
         , dependsOn fee feeInput
         , dependsOn outputs inputUtxo
         , satisfies inputUtxo (hasSize (rangeSize 2 4))
@@ -161,9 +163,10 @@ bodyspec utxo certsenv certstate =
         , assert $ inputs ==. dom_ inputUtxo
         , reify inputUtxo (map snd . Map.toList) $
             \ [var|txouts|] ->
-              [ assert $ (sumCoin_ @era outputs) ==. sumCoin_ @era txouts - fee
+              [ dependsOn outputs txouts
+              , assert $ (sumCoin_ @era outputs) ==. sumCoin_ @era txouts - fee
               ]
-        , forAll certs $ \x -> satisfies x (txCertSpec (projectEnv certsenv) certstate)
+        , forAll certs $ \ [var|oneCert|] -> satisfies oneCert (txCertSpec (projectEnv certsenv) certstate)
         , assert $ sizeOf_ certs <=. 4
         , assert $ rewAcct ==. lit Map.empty
         ]
@@ -184,7 +187,8 @@ go = do
   certState <-
     generate $
       genFromSpec @ConwayFn @(CertState era)
-        (certStateSpec (lit (AccountState (Coin 1000) (Coin 100))) (lit (EpochNo 100)))
+        (certStateSpec @ConwayFn @era) -- (lit (AccountState (Coin 1000) (Coin 100))) (lit (EpochNo 100)))
+        -- error "STOP"
   certsEnv <- generate $ genFromSpec @ConwayFn @(CertsEnv era) certsEnvSpec
 
   (basic, subutxo, feeinput) <- generate $ genFromSpec (bodyspec @era utxo certsEnv certState)