Try replacing 'term' with 'uni' in 'KnownType'

IntersectMBO · effectfully · Mar 23, 2022 · Mar 24, 2022 · Mar 24, 2022 · Apr 7, 2022
commit 14f322e3abcf7938adc295947477144c1daaced9
diff --git a/plutus-core/testlib/PlutusCore/Generators/Internal/Denotation.hs b/plutus-core/testlib/PlutusCore/Generators/Internal/Denotation.hs
@@ -35,7 +35,7 @@ data Denotation term object res = forall args. Denotation
       -- ^ How to embed the object into a term.
     , _denotationItself :: FoldArgs args res
       -- ^ The denotation of the object. E.g. the denotation of 'AddInteger' is '(+)'.
-    , _denotationScheme :: TypeScheme term args res
+    , _denotationScheme :: TypeScheme (UniOf term) args res
       -- ^ The 'TypeScheme' of the object. See 'intIntInt' for example.
     }
 
@@ -52,7 +52,8 @@ data DenotationContextMember term res =
 --   2. a bound variable of functional type with the result being @integer@
 --   3. the 'AddInteger' 'Builtin' or any other 'Builtin' which returns an @integer@.
 newtype DenotationContext term = DenotationContext
-    { unDenotationContext :: DMap (AsKnownType term) (Compose [] (DenotationContextMember term))
+    { unDenotationContext ::
+        DMap (AsKnownType (UniOf term)) (Compose [] (DenotationContextMember term))
     }
 
 -- Here the only search that we need to perform is the search for things that return an appropriate
@@ -61,20 +62,20 @@ newtype DenotationContext term = DenotationContext
 -- (without @Void@).
 
 -- | The resulting type of a 'TypeScheme'.
-typeSchemeResult :: TypeScheme term args res -> AsKnownType term res
+typeSchemeResult :: TypeScheme uni args res -> AsKnownType uni res
 typeSchemeResult TypeSchemeResult       = AsKnownType
 typeSchemeResult (TypeSchemeArrow schB) = typeSchemeResult schB
 typeSchemeResult (TypeSchemeAll _ schK) = typeSchemeResult schK
 
 -- | Get the 'Denotation' of a variable.
 denoteVariable
-    :: KnownType (Term TyName Name uni fun ()) res
+    :: KnownType uni res
     => Name -> res -> Denotation (Term TyName Name uni fun ()) Name res
 denoteVariable name meta = Denotation name (Var ()) meta TypeSchemeResult
 
 -- | Insert the 'Denotation' of an object into a 'DenotationContext'.
 insertDenotation
-    :: (GShow (UniOf term), KnownType term res)
+    :: (GShow (UniOf term), KnownType (UniOf term) res)
     => Denotation term object res -> DenotationContext term -> DenotationContext term
 insertDenotation denotation (DenotationContext vs) = DenotationContext $
     DMap.insertWith'
@@ -85,7 +86,7 @@ insertDenotation denotation (DenotationContext vs) = DenotationContext $
 
 -- | Insert a variable into a 'DenotationContext'.
 insertVariable
-    :: (GShow uni, KnownType (Term TyName Name uni fun ()) a)
+    :: (GShow uni, KnownType uni a)
     => Name
     -> a
     -> DenotationContext (Term TyName Name uni fun ())
@@ -98,9 +99,9 @@ insertBuiltin
     -> DenotationContext (Term TyName Name DefaultUni DefaultFun ())
     -> DenotationContext (Term TyName Name DefaultUni DefaultFun ())
 insertBuiltin fun =
-    case toBuiltinMeaning fun of
+    case toBuiltinMeaning @_ @_ @(Term TyName Name DefaultUni DefaultFun ()) fun of
         BuiltinMeaning sch meta _ ->
-           case typeSchemeResult @(Term TyName Name DefaultUni DefaultFun ()) sch of
+           case typeSchemeResult sch of
                AsKnownType ->
                    insertDenotation $ Denotation fun (Builtin ()) meta sch
 

diff --git a/plutus-core/testlib/PlutusCore/Generators/Internal/Dependent.hs b/plutus-core/testlib/PlutusCore/Generators/Internal/Dependent.hs
@@ -18,7 +18,6 @@ module PlutusCore.Generators.Internal.Dependent
 import PlutusPrelude
 
 import PlutusCore.Builtin
-import PlutusCore.Core
 
 import Data.GADT.Compare
 import Universe
@@ -29,16 +28,16 @@ liftOrdering LT = GLT
 liftOrdering EQ = error "'liftOrdering': 'Eq'"
 liftOrdering GT = GGT
 
-type KnownType val a = (KnownTypeAst (UniOf val) a, MakeKnown val a)
+type KnownType uni a = (KnownTypeAst uni a, MakeKnownIn uni a)
 
 -- | Contains a proof that @a@ is a 'KnownType'.
-data AsKnownType term a where
-    AsKnownType :: KnownType term a => AsKnownType term a
+data AsKnownType uni a where
+    AsKnownType :: KnownType uni a => AsKnownType uni a
 
-instance GShow (UniOf term) => Pretty (AsKnownType term a) where
-    pretty a@AsKnownType = pretty $ toTypeAst @_ @(UniOf term) a
+instance GShow uni => Pretty (AsKnownType uni a) where
+    pretty a@AsKnownType = pretty $ toTypeAst @_ @uni a
 
-instance GShow (UniOf term) => GEq (AsKnownType term) where
+instance GShow uni => GEq (AsKnownType uni) where
     a `geq` b = do
         -- TODO: there is a HUGE problem here. @EvaluationResult a@ and @a@ have the same string
         -- representation currently, so we need to either fix that or come up with a more sensible
@@ -49,11 +48,11 @@ instance GShow (UniOf term) => GEq (AsKnownType term) where
         guard $ display @String a == display b
         Just $ unsafeCoerce Refl
 
-instance GShow (UniOf term) => GCompare (AsKnownType term) where
+instance GShow uni => GCompare (AsKnownType uni) where
     a `gcompare` b
         | Just Refl <- a `geq` b = GEQ
         | otherwise              = liftOrdering $ display @String a `compare` display b
 
 -- | Turn any @proxy a@ into an @AsKnownType a@ provided @a@ is a 'KnownType'.
-proxyAsKnownType :: KnownType term a => proxy a -> AsKnownType term a
+proxyAsKnownType :: KnownType uni a => proxy a -> AsKnownType uni a
 proxyAsKnownType _ = AsKnownType
diff --git a/plutus-core/testlib/PlutusCore/Generators/Internal/Entity.hs b/plutus-core/testlib/PlutusCore/Generators/Internal/Entity.hs
@@ -78,7 +78,7 @@ instance (PrettyBy config head, PrettyBy config arg) => PrettyBy config (IterApp
         parens $ foldl' (\fun arg -> fun <+> prettyBy config arg) (prettyBy config appHead) appSpine
 
 -- | One iterated application of a @head@ to @arg@s represented in three distinct ways.
-data IterAppValue uni fun head arg r = KnownType arg r => IterAppValue
+data IterAppValue uni fun head arg r = KnownType (UniOf arg) r => IterAppValue
     { _iterTerm :: Plain Term uni fun  -- ^ As a PLC 'Term'.
     , _iterApp  :: IterApp head arg    -- ^ As an 'IterApp'.
     , _iterTbv  :: r                   -- ^ As a Haskell value.
@@ -111,8 +111,8 @@ revealUnique (Name name uniq) =
 -- TODO: we can generate more types here.
 -- | Generate a 'Builtin' and supply its typed version to a continuation.
 withTypedBuiltinGen
-    :: forall term m c uni. (uni ~ DefaultUni, HasConstantIn uni term, Monad m)
-    => (forall a. AsKnownType term a -> GenT m c) -> GenT m c
+    :: forall term m c uni. (uni ~ DefaultUni, Monad m)
+    => (forall a. AsKnownType uni a -> GenT m c) -> GenT m c
 withTypedBuiltinGen k = Gen.choice
     [ k @Integer       AsKnownType
     , k @BS.ByteString AsKnownType
@@ -124,7 +124,7 @@ withTypedBuiltinGen k = Gen.choice
 withCheckedTermGen
     :: forall m c uni fun. (uni ~ DefaultUni, fun ~ DefaultFun, Monad m)
     => TypedBuiltinGenT (Plain Term uni fun) m
-    -> (forall a. AsKnownType (Plain Term uni fun) a ->
+    -> (forall a. AssociateValueMake uni a (Plain Term uni fun) => AsKnownType uni a ->
             TermOf (Plain Term uni fun) (EvaluationResult (Plain Term uni fun)) ->
                 GenT m c)
     -> GenT m c
@@ -148,7 +148,7 @@ genIterAppValue (Denotation object embed meta scheme) = result where
     result = go scheme (embed object) id meta
 
     go
-        :: TypeScheme (Plain Term uni fun) args res
+        :: TypeScheme uni args res
         -> Plain Term uni fun
         -> ([Plain Term uni fun] -> [Plain Term uni fun])
         -> FoldArgs args res
@@ -184,7 +184,7 @@ genTerm genBase context0 depth0 = Morph.hoist runQuoteT . go context0 depth0 whe
     go
         :: DenotationContext (Plain Term uni fun)
         -> Int
-        -> AsKnownType (Plain Term uni fun) r
+        -> AsKnownType uni r
         -> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
     go context depth akt
         -- FIXME: should be using 'variables' but this is now the same as 'recursive'
@@ -231,7 +231,7 @@ genTermLoose = genTerm genTypedBuiltinDef typedBuiltins 4
 -- attach the 'TypedBuiltin' to the value part of the 'TermOf' and pass that to a continuation.
 withAnyTermLoose
      :: forall m c uni fun. (uni ~ DefaultUni, fun ~ DefaultFun, Monad m)
-     => (forall a. KnownType (Plain Term uni fun) a => TermOf (Plain Term uni fun) a -> GenT m c)
+     => (forall a. KnownType uni a => TermOf (Plain Term uni fun) a -> GenT m c)
      -> GenT m c
 withAnyTermLoose k =
     withTypedBuiltinGen @(Plain Term uni fun) $ \akt@AsKnownType -> genTermLoose akt >>= k
diff --git a/plutus-core/testlib/PlutusCore/Generators/Internal/TypeEvalCheck.hs b/plutus-core/testlib/PlutusCore/Generators/Internal/TypeEvalCheck.hs
@@ -91,7 +91,8 @@ type TypeEvalCheckM uni fun = Either (TypeEvalCheckError uni fun)
 -- See Note [Type-eval checking].
 -- | Type check and evaluate a term and check that the expected result is equal to the actual one.
 typeEvalCheckBy
-    :: ( uni ~ DefaultUni, fun ~ DefaultFun, KnownType (Term TyName Name uni fun ()) a
+    :: ( uni ~ DefaultUni, fun ~ DefaultFun
+       , KnownType uni a, AssociateValueMake uni a (Term TyName Name uni fun ())
        , PrettyPlc internal
        )
     => (Term TyName Name uni fun () ->
@@ -117,7 +118,9 @@ typeEvalCheckBy eval (TermOf term (x :: a)) = TermOf term <$> do
 -- | Type check and evaluate a term and check that the expected result is equal to the actual one.
 -- Throw an error in case something goes wrong.
 unsafeTypeEvalCheck
-    :: (uni ~ DefaultUni, fun ~ DefaultFun, KnownType (Term TyName Name uni fun ()) a)
+    :: ( uni ~ DefaultUni, fun ~ DefaultFun
+       , KnownType uni a, AssociateValueMake uni a (Term TyName Name uni fun ())
+       )
     => TermOf (Term TyName Name uni fun ()) a
     -> TermOf (Term TyName Name uni fun ()) (EvaluationResult (Term TyName Name uni fun ()))
 unsafeTypeEvalCheck termOfTbv = do

diff --git a/plutus-core/testlib/PlutusCore/Generators/Internal/TypedBuiltinGen.hs b/plutus-core/testlib/PlutusCore/Generators/Internal/TypedBuiltinGen.hs
@@ -48,7 +48,7 @@ data TermOf term a = TermOf
 
 -- | A function of this type generates values of built-in typed (see 'TypedBuiltin' for
 -- the list of such types) and returns it along with the corresponding PLC value.
-type TypedBuiltinGenT term m = forall a. AsKnownType term a -> GenT m (TermOf term a)
+type TypedBuiltinGenT term m = forall a. AsKnownType (UniOf term) a -> GenT m (TermOf term a)
 
 -- | 'TypedBuiltinGenT' specified to 'Identity'.
 type TypedBuiltinGen term = TypedBuiltinGenT term Identity
@@ -58,7 +58,7 @@ instance (PrettyBy config a, PrettyBy config term) =>
     prettyBy config (TermOf t x) = prettyBy config t <+> "~>" <+> prettyBy config x
 
 attachCoercedTerm
-    :: (Monad m, KnownType term a, PrettyConst a)
+    :: (Monad m, KnownType (UniOf term) a, AssociateValueMake (UniOf term) a term, PrettyConst a)
     => GenT m a -> GenT m (TermOf term a)
 attachCoercedTerm a = do
     x <- a
@@ -73,7 +73,10 @@ attachCoercedTerm a = do
 
 -- | Update a typed built-ins generator by overwriting the generator for a certain built-in.
 updateTypedBuiltinGen
-    :: forall a term m. (GShow (UniOf term), KnownType term a, PrettyConst a, Monad m)
+    :: forall a term m.
+        ( GShow (UniOf term), KnownType (UniOf term) a, AssociateValueMake (UniOf term) a term
+        , PrettyConst a, Monad m
+        )
     => GenT m a                  -- ^ A new generator.
     -> TypedBuiltinGenT term m   -- ^ An old typed built-ins generator.
     -> TypedBuiltinGenT term m   -- ^ The updated typed built-ins generator.