Replace 'val' with 'uni' in 'TypeScheme'

IntersectMBO · Apr 7, 2022 · cf3f21e · cf3f21e
1 parent 3eb2222
commit cf3f21e
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 21 deletions.
diff --git a/plutus-core/cost-model/budgeting-bench/Benchmarks/Nops.hs b/plutus-core/cost-model/budgeting-bench/Benchmarks/Nops.hs
@@ -157,7 +157,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni NopFun where
     -- Built-in Bools
     toBuiltinMeaning
         :: forall val . HasConstantIn uni val
-           => NopFun -> BuiltinMeaning val NopCostModel
+           => NopFun -> BuiltinMeaning uni NopCostModel
     toBuiltinMeaning Nop1b =
         makeBuiltinMeaning
              @(Bool -> Bool)

diff --git a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
@@ -128,10 +128,13 @@ instance (ToBuiltinMeaning uni fun1, ToBuiltinMeaning uni fun2) =>
             ToBuiltinMeaning uni (Either fun1 fun2) where
     type CostingPart uni (Either fun1 fun2) = (CostingPart uni fun1, CostingPart uni fun2)
 
-    toBuiltinMeaning (Left  fun) = case toBuiltinMeaning fun of
+    toBuiltinMeaning
+        :: forall val. HasConstantIn uni val
+        => Either fun1 fun2 -> BuiltinMeaning val (CostingPart uni fun1, CostingPart uni fun2)
+    toBuiltinMeaning (Left  fun) = case toBuiltinMeaning @_ @_ @val fun of
         BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch immF defF toExF) ->
             BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch immF defF (toExF . fst))
-    toBuiltinMeaning (Right fun) = case toBuiltinMeaning fun of
+    toBuiltinMeaning (Right fun) = case toBuiltinMeaning @_ @_ @val fun of
         BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch immF defF toExF) ->
             BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch immF defF (toExF . snd))
 

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
@@ -61,7 +61,7 @@ type family FoldArgs args res where
 -- functions from a certain set, hence the @cost@ parameter.
 data BuiltinMeaning val cost =
     forall args res. BuiltinMeaning
-        (TypeScheme val args res)
+        (TypeScheme (UniOf val) args res)
         (FoldArgs args res)
         (BuiltinRuntimeOptions (Length args) val cost)
 
@@ -87,7 +87,7 @@ respectively. 'KnownMonotype' turns every argument that the Haskell denotation o
 receives into a 'TypeSchemeArrow'. We extract the arguments from the type of the Haskell denotation
 using the 'GetArgs' type family. 'KnownPolytype' turns every bound variable into a 'TypeSchemeAll'.
 We extract variables from the type of the Haskell denotation using the 'ToBinds' type family
-(in particular, see the @ToBinds (TypeScheme val args res)@ type instances). Variables are
+(in particular, see the @ToBinds (TypeScheme uni args res)@ type instances). Variables are
 collected in the order that they appear in (i.e. just like in Haskell). For example, processing
 a type signature like
 
@@ -150,7 +150,7 @@ type family GetArgs a where
 -- Similarly, we could've computed 'toImmediateF' and 'toDeferredF' from a 'TypeScheme' but not
 -- statically again, and that would break inlining and basically all the optimization.
 class KnownMonotype val args res a | args res -> a, a -> res where
-    knownMonotype :: TypeScheme val args res
+    knownMonotype :: TypeScheme (UniOf val) args res
     knownMonoruntime :: RuntimeScheme (Length args)
 
     -- | Convert the denotation of a builtin to its runtime counterpart with immediate unlifting.
@@ -181,7 +181,7 @@ instance
         ( KnownTypeAst (UniOf val) arg, MakeKnown val arg, ReadKnown val arg
         , KnownMonotype val args res a
         ) => KnownMonotype val (arg ': args) res (arg -> a) where
-    knownMonotype = TypeSchemeArrow knownMonotype
+    knownMonotype = TypeSchemeArrow $ knownMonotype @val
     knownMonoruntime = RuntimeSchemeArrow $ knownMonoruntime @val @args @res
 
     -- Unlift, then recurse.
@@ -207,12 +207,12 @@ instance
 -- | A class that allows us to derive a polytype for a builtin.
 class KnownMonotype val args res a =>
         KnownPolytype (binds :: [Some TyNameRep]) val args res a | args res -> a, a -> res where
-    knownPolytype :: TypeScheme val args res
+    knownPolytype :: TypeScheme (UniOf val) args res
     knownPolyruntime :: RuntimeScheme (Length args)
 
 -- | Once we've run out of type-level arguments, we start handling term-level ones.
 instance KnownMonotype val args res a => KnownPolytype '[] val args res a where
-    knownPolytype = knownMonotype
+    knownPolytype = knownMonotype @val
     knownPolyruntime = knownMonoruntime @val @args @res
 
 -- Here we unpack an existentially packed @kind@ and constrain it afterwards!
@@ -222,7 +222,7 @@ instance KnownMonotype val args res a => KnownPolytype '[] val args res a where
 -- | Every type-level argument becomes a 'TypeSchemeAll'.
 instance (KnownSymbol name, KnownNat uniq, KnownKind kind, KnownPolytype binds val args res a) =>
             KnownPolytype ('Some ('TyNameRep @kind name uniq) ': binds) val args res a where
-    knownPolytype = TypeSchemeAll @name @uniq @kind Proxy $ knownPolytype @binds
+    knownPolytype = TypeSchemeAll @name @uniq @kind Proxy $ knownPolytype @binds @val
     knownPolyruntime = RuntimeSchemeAll $ knownPolyruntime @binds @val @args @res
 
 -- See Note [Automatic derivation of type schemes]

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/TypeScheme.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/TypeScheme.hs
@@ -53,29 +53,29 @@ on readability of the Core output.
 
 -- | Type schemes of primitive operations.
 -- @as@ is a list of types of arguments, @r@ is the resulting type.
--- E.g. @Text -> Bool -> Integer@ is encoded as @TypeScheme val [Text, Bool] Integer@.
-data TypeScheme val (args :: [GHC.Type]) res where
+-- E.g. @Text -> Bool -> Integer@ is encoded as @TypeScheme uni [Text, Bool] Integer@.
+data TypeScheme uni (args :: [GHC.Type]) res where
     TypeSchemeResult
-        :: (KnownTypeAst (UniOf val) res, MakeKnown val res)
-        => TypeScheme val '[] res
+        :: (KnownTypeAst uni res, MakeKnownIn uni res)
+        => TypeScheme uni '[] res
     TypeSchemeArrow
-        :: (KnownTypeAst (UniOf val) arg, ReadKnown val arg, MakeKnown val arg)
-        => TypeScheme val args res
-        -> TypeScheme val (arg ': args) res
+        :: (KnownTypeAst uni arg, ReadKnownIn uni arg, MakeKnownIn uni arg)
+        => TypeScheme uni args res
+        -> TypeScheme uni (arg ': args) res
     TypeSchemeAll
         :: (KnownSymbol text, KnownNat uniq, KnownKind kind)
            -- Here we require the user to manually provide the unique of a type variable.
            -- That's nothing but silly, but I do not see what else we can do with the current design.
         => Proxy '(text, uniq, kind)
-        -> TypeScheme val args res
-        -> TypeScheme val args res
+        -> TypeScheme uni args res
+        -> TypeScheme uni args res
 
-argProxy :: TypeScheme val (arg ': args) res -> Proxy arg
+argProxy :: TypeScheme uni (arg ': args) res -> Proxy arg
 argProxy _ = Proxy
 
 -- | Convert a 'TypeScheme' to the corresponding 'Type'.
 -- Basically, a map from the PHOAS representation to the FOAS one.
-typeSchemeToType :: TypeScheme val args res -> Type TyName (UniOf val) ()
+typeSchemeToType :: TypeScheme uni args res -> Type TyName uni ()
 typeSchemeToType sch@TypeSchemeResult = toTypeAst sch
 typeSchemeToType sch@(TypeSchemeArrow schB) =
     TyFun () (toTypeAst $ argProxy sch) $ typeSchemeToType schB