[Builtins] Drop 'val' from 'KnownType' stuff

plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs

@@ -151,9 +151,11 @@ instance KnownTypeAst DefaultUni Void where
     toTypeAst _ = runQuote $ do
         a <- freshTyName "a"
         pure $ TyForall () a (Type ()) $ TyVar () a
-instance UniOf term ~ DefaultUni => MakeKnownIn DefaultUni term Void where
+instance MakeKnownIn DefaultUni Void where
+    type AssociateValueMake _ _ = Ignore
     makeKnown _ = absurd
-instance UniOf term ~ DefaultUni => ReadKnownIn DefaultUni term Void where
+instance ReadKnownIn DefaultUni Void where
+    type AssociateValueRead _ _ = Ignore
     readKnown mayCause _ = throwingWithCause _UnliftingError "Can't unlift a 'Void'" mayCause
 
 data BuiltinErrorCall = BuiltinErrorCall

plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs

@@ -1,17 +1,18 @@
-{-# LANGUAGE BlockArguments        #-}
-{-# LANGUAGE ConstraintKinds       #-}
-{-# LANGUAGE DataKinds             #-}
-{-# LANGUAGE DefaultSignatures     #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE KindSignatures        #-}
-{-# LANGUAGE LambdaCase            #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE OverloadedStrings     #-}
-{-# LANGUAGE TemplateHaskell       #-}
-{-# LANGUAGE TypeApplications      #-}
-{-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE BlockArguments           #-}
+{-# LANGUAGE ConstraintKinds          #-}
+{-# LANGUAGE DataKinds                #-}
+{-# LANGUAGE DefaultSignatures        #-}
+{-# LANGUAGE FlexibleInstances        #-}
+{-# LANGUAGE KindSignatures           #-}
+{-# LANGUAGE LambdaCase               #-}
+{-# LANGUAGE MultiParamTypeClasses    #-}
+{-# LANGUAGE OverloadedStrings        #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TemplateHaskell          #-}
+{-# LANGUAGE TypeApplications         #-}
+{-# LANGUAGE TypeFamilies             #-}
+{-# LANGUAGE TypeOperators            #-}
+{-# LANGUAGE UndecidableInstances     #-}
 
 module PlutusCore.Builtin.KnownType
     ( KnownTypeError
@@ -28,6 +29,7 @@ module PlutusCore.Builtin.KnownType
     , makeKnownRun
     , makeKnownOrFail
     , readKnownSelf
+    , Ignore
     ) where
 
 import PlutusPrelude (reoption)
@@ -44,6 +46,7 @@ import Control.Lens.TH (makeClassyPrisms)
 import Control.Monad.Except
 import Data.Coerce
 import Data.DList (DList)
+import Data.Kind qualified as GHC
 import Data.String
 import Data.Text (Text)
 import GHC.Exts (inline, oneShot)
@@ -52,7 +55,8 @@ import Universe
 
 -- | A constraint for \"@a@ is a 'ReadKnownIn' and 'MakeKnownIn' by means of being included
 -- in @uni@\".
-type KnownBuiltinTypeIn uni val a = (HasConstantIn uni val, GShow uni, GEq uni, uni `Contains` a)
+type KnownBuiltinTypeIn uni val a =
+    (uni ~ UniOf val, HasConstant val, GShow uni, GEq uni, uni `Contains` a)
 
 -- | A constraint for \"@a@ is a 'ReadKnownIn' and 'MakeKnownIn' by means of being included
 -- in @UniOf term@\".
@@ -245,41 +249,57 @@ the cause stored in it is not forced due to @Maybe@ being a lazy data type.
 -}
 
 -- See Note [Performance of ReadKnownIn and MakeKnownIn instances].
-class uni ~ UniOf val => MakeKnownIn uni val a where
+type MakeKnownIn :: (GHC.Type -> GHC.Type) -> GHC.Type -> GHC.Constraint
+class MakeKnownIn uni a where
+    type AssociateValueMake uni a :: GHC.Type -> GHC.Constraint
+    type AssociateValueMake uni a = HasConstant
+
     -- See Note [Cause of failure].
     -- | Convert a Haskell value to the corresponding PLC val.
     -- The inverse of 'readKnown'.
-    makeKnown :: Maybe cause -> a -> MakeKnownM cause val
-    default makeKnown :: KnownBuiltinType val a => Maybe cause -> a -> MakeKnownM cause val
+    makeKnown
+        :: (uni ~ UniOf val, AssociateValueMake uni a val)
+        => Maybe cause -> a -> MakeKnownM cause val
+    default makeKnown
+        :: KnownBuiltinTypeIn uni val a
+        => Maybe cause -> a -> MakeKnownM cause val
     -- Forcing the value to avoid space leaks. Note that the value is only forced to WHNF,
     -- so care must be taken to ensure that every value of a type from the universe gets forced
     -- to NF whenever it's forced to WHNF.
     makeKnown _ x = pure . fromConstant . someValue $! x
     {-# INLINE makeKnown #-}
 
-type MakeKnown val = MakeKnownIn (UniOf val) val
+type MakeKnown val a = (MakeKnownIn (UniOf val) a, AssociateValueMake (UniOf val) a val)
 
 -- See Note [Performance of ReadKnownIn and MakeKnownIn instances].
-class uni ~ UniOf val => ReadKnownIn uni val a where
+type ReadKnownIn :: (GHC.Type -> GHC.Type) -> GHC.Type -> GHC.Constraint
+class ReadKnownIn uni a where
+    type AssociateValueRead uni a :: GHC.Type -> GHC.Constraint
+    type AssociateValueRead uni a = HasConstant
+
     -- See Note [Cause of failure].
     -- | Convert a PLC val to the corresponding Haskell value.
     -- The inverse of 'makeKnown'.
-    readKnown :: Maybe cause -> val -> ReadKnownM cause a
-    default readKnown :: KnownBuiltinType val a => Maybe cause -> val -> ReadKnownM cause a
+    readKnown
+        :: (uni ~ UniOf val, AssociateValueRead uni a val)
+        => Maybe cause -> val -> ReadKnownM cause a
+    default readKnown
+        :: KnownBuiltinTypeIn uni val a
+        => Maybe cause -> val -> ReadKnownM cause a
     -- If 'inline' is not used, proper inlining does not happen for whatever reason.
     readKnown = inline readKnownConstant
     {-# INLINE readKnown #-}
 
-type ReadKnown val = ReadKnownIn (UniOf val) val
+type ReadKnown val a = (ReadKnownIn (UniOf val) a, AssociateValueRead (UniOf val) a val)
 
 makeKnownRun
-    :: MakeKnownIn uni val a
+    :: MakeKnown val a
     => Maybe cause -> a -> (ReadKnownM cause val, DList Text)
 makeKnownRun mayCause = runEmitter . runExceptT . makeKnown mayCause
 {-# INLINE makeKnownRun #-}
 
 -- | Same as 'makeKnown', but allows for neither emitting nor storing the cause of a failure.
-makeKnownOrFail :: MakeKnownIn uni val a => a -> EvaluationResult val
+makeKnownOrFail :: MakeKnown val a => a -> EvaluationResult val
 makeKnownOrFail = reoption . fst . makeKnownRun Nothing
 {-# INLINE makeKnownOrFail #-}
 
@@ -292,7 +312,8 @@ readKnownSelf
 readKnownSelf val = either throwKnownTypeErrorWithCause pure $ readKnown (Just val) val
 {-# INLINE readKnownSelf #-}
 
-instance MakeKnownIn uni val a => MakeKnownIn uni val (EvaluationResult a) where
+instance MakeKnownIn uni a => MakeKnownIn uni (EvaluationResult a) where
+    type AssociateValueMake uni (EvaluationResult a) = AssociateValueMake uni a
     makeKnown mayCause EvaluationFailure     = throwingWithCause _EvaluationFailure () mayCause
     makeKnown mayCause (EvaluationSuccess x) = makeKnown mayCause x
     {-# INLINE makeKnown #-}
@@ -303,42 +324,46 @@ instance MakeKnownIn uni val a => MakeKnownIn uni val (EvaluationResult a) where
 -- that when this value is 'EvaluationFailure', a PLC 'Error' was caught.
 -- I.e. it would essentially allow us to catch errors and handle them in a programmable way.
 -- We forbid this, because it complicates code and isn't supported by evaluation engines anyway.
-instance
-        ( TypeError ('Text "‘EvaluationResult’ cannot appear in the type of an argument")
-        , uni ~ UniOf val
-        ) => ReadKnownIn uni val (EvaluationResult a) where
+instance TypeError ('Text "‘EvaluationResult’ cannot appear in the type of an argument") =>
+            ReadKnownIn uni (EvaluationResult a) where
+    type AssociateValueRead _ _ = Ignore
     readKnown mayCause _ =
         throwingWithCause _UnliftingError "Panic: 'TypeError' was bypassed" mayCause
 
-instance MakeKnownIn uni val a => MakeKnownIn uni val (Emitter a) where
+instance MakeKnownIn uni a => MakeKnownIn uni (Emitter a) where
+    type AssociateValueMake uni (Emitter a) = AssociateValueMake uni a
     makeKnown mayCause a = lift a >>= makeKnown mayCause
     {-# INLINE makeKnown #-}
 
-instance
-        ( TypeError ('Text "‘Emitter’ cannot appear in the type of an argument")
-        , uni ~ UniOf val
-        ) => ReadKnownIn uni val (Emitter a) where
+instance TypeError ('Text "‘Emitter’ cannot appear in the type of an argument") =>
+            ReadKnownIn uni (Emitter a) where
+    type AssociateValueRead _ _ = Ignore
     readKnown mayCause _ =
         throwingWithCause _UnliftingError "Panic: 'TypeError' was bypassed" mayCause
 
-instance HasConstantIn uni val => MakeKnownIn uni val (SomeConstant uni rep) where
+instance MakeKnownIn uni (SomeConstant uni rep) where
     makeKnown _ = coerceArg $ pure . fromConstant
     {-# INLINE makeKnown #-}
 
-instance HasConstantIn uni val => ReadKnownIn uni val (SomeConstant uni rep) where
+instance ReadKnownIn uni (SomeConstant uni rep) where
     readKnown = coerceVia (\asC mayCause -> fmap SomeConstant . asC mayCause) asConstant
     {-# INLINE readKnown #-}
 
-instance uni ~ UniOf val => MakeKnownIn uni val (Opaque val rep) where
+instance uni ~ UniOf val => MakeKnownIn uni (Opaque val rep) where
+    type AssociateValueMake _ _ = (~) val
     makeKnown _ = coerceArg pure  -- A faster @pure . Opaque@.
     {-# INLINE makeKnown #-}
 
-instance uni ~ UniOf val => ReadKnownIn uni val (Opaque val rep) where
+instance uni ~ UniOf val => ReadKnownIn uni (Opaque val rep) where
+    type AssociateValueRead _ _ = (~) val
     readKnown _ = coerceArg pure  -- A faster @pure . Opaque@.
     {-# INLINE readKnown #-}
 
 -- Utils
 
+class    Ignore a
+instance Ignore a
+
 -- | Coerce the second argument to the result type of the first one. The motivation for this
 -- function is that it's often more annoying to explicitly specify a target type for 'coerce' than
 -- to construct an explicit coercion function, so this combinator can be used in cases like that.

plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs

@@ -168,12 +168,12 @@ instance (res ~ res', Typeable res, KnownTypeAst (UniOf val) res, MakeKnown val
     knownMonotype = TypeSchemeResult
     knownMonoruntime = RuntimeSchemeResult
 
-    toImmediateF = makeKnown (Just ())
+    toImmediateF = inline makeKnown (Just ())
     {-# INLINE toImmediateF #-}
 
     -- For deferred unlifting we need to lift the 'ReadKnownM' action into 'MakeKnownM',
     -- hence 'liftEither'.
-    toDeferredF getRes = liftEither getRes >>= makeKnown (Just ())
+    toDeferredF getRes = liftEither getRes >>= inline makeKnown (Just ())
     {-# INLINE toDeferredF #-}
 
 -- | Every term-level argument becomes as 'TypeSchemeArrow'.
@@ -185,7 +185,7 @@ instance
     knownMonoruntime = RuntimeSchemeArrow $ knownMonoruntime @val @args @res
 
     -- Unlift, then recurse.
-    toImmediateF f = fmap (toImmediateF @val @args @res . f) . readKnown (Just ())
+    toImmediateF f = fmap (toImmediateF @val @args @res . f) . inline readKnown (Just ())
     {-# INLINE toImmediateF #-}
 
     -- Grow the builtin application within the received action and recurse on the result.
@@ -201,7 +201,7 @@ instance
         -- of how unlifting is aligned.
         --
         -- 'pure' signifies that no failure can occur at this point.
-        pure . toDeferredF @val @args @res $! getF <*> readKnown (Just ()) arg
+        pure . toDeferredF @val @args @res $! getF <*> inline readKnown (Just ()) arg
     {-# INLINE toDeferredF #-}
 
 -- | A class that allows us to derive a polytype for a builtin.

plutus-core/plutus-core/src/PlutusCore/Builtin/TestKnown.hs

@@ -24,19 +24,15 @@ import Universe
 class    (KnownBuiltinTypeAst uni a => KnownTypeAst uni a) => ImplementedKnownTypeAst uni a
 instance (KnownBuiltinTypeAst uni a => KnownTypeAst uni a) => ImplementedKnownTypeAst uni a
 
--- | For providing a 'ReadKnownIn' instance for a built-in type it's enough for that type to satisfy
--- 'KnownBuiltinTypeIn'.
-class    (forall val. KnownBuiltinTypeIn uni val a => ReadKnownIn uni val a) =>
-    ImplementedReadKnownIn uni a
-instance (forall val. KnownBuiltinTypeIn uni val a => ReadKnownIn uni val a) =>
-    ImplementedReadKnownIn uni a
+-- | For providing a 'ReadKnownIn' instance for a built-in type it's enough for that type to be in
+-- the universe.
+class    (uni `Contains` a => ReadKnownIn uni a) => ImplementedReadKnownIn uni a
+instance (uni `Contains` a => ReadKnownIn uni a) => ImplementedReadKnownIn uni a
 
--- | For providing a 'MakeKnownIn' instance for a built-in type it's enough for that type to satisfy
--- 'KnownBuiltinTypeIn'.
-class    (forall val. KnownBuiltinTypeIn uni val a => MakeKnownIn uni val a) =>
-    ImplementedMakeKnownIn uni a
-instance (forall val. KnownBuiltinTypeIn uni val a => MakeKnownIn uni val a) =>
-    ImplementedMakeKnownIn uni a
+-- | For providing a 'MakeKnownIn' instance for a built-in type it's enough for that type to be in
+-- the univese.
+class    (uni `Contains` a => MakeKnownIn uni a) => ImplementedMakeKnownIn uni a
+instance (uni `Contains` a => MakeKnownIn uni a) => ImplementedMakeKnownIn uni a
 
 -- | An instance of this class not having any constraints ensures that every type (according to
 -- 'Everywhere') from the universe has 'KnownTypeAst, 'ReadKnownIn' and 'MakeKnownIn' instances.

plutus-core/plutus-core/src/PlutusCore/Builtin/TypeScheme.hs

@@ -5,6 +5,7 @@
 {-# LANGUAGE DataKinds        #-}
 {-# LANGUAGE GADTs            #-}
 {-# LANGUAGE KindSignatures   #-}
+{-# LANGUAGE RankNTypes       #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies     #-}
 {-# LANGUAGE TypeOperators    #-}
@@ -62,8 +63,9 @@ data TypeScheme val (args :: [GHC.Type]) res where
         :: (Typeable res, KnownTypeAst (UniOf val) res, MakeKnown val res)
         => TypeScheme val '[] res
     TypeSchemeArrow
-        :: (Typeable arg, KnownTypeAst (UniOf val) arg, MakeKnown val arg, ReadKnown val arg)
-        => TypeScheme val args res -> TypeScheme val (arg ': args) res
+        :: (Typeable arg, KnownTypeAst (UniOf val) arg, ReadKnown val arg, MakeKnown val arg)
+        => TypeScheme val args res
+        -> TypeScheme val (arg ': args) res
     TypeSchemeAll
         :: (KnownSymbol text, KnownNat uniq, KnownKind kind)
            -- Here we require the user to manually provide the unique of a type variable.
@@ -78,7 +80,7 @@ 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 sch@TypeSchemeResult       = toTypeAst sch
+typeSchemeToType sch@TypeSchemeResult = toTypeAst sch
 typeSchemeToType sch@(TypeSchemeArrow schB) =
     TyFun () (toTypeAst $ argProxy sch) $ typeSchemeToType schB
 typeSchemeToType (TypeSchemeAll proxy schK) = case proxy of

plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs

@@ -193,28 +193,24 @@ It's some pretty annoying boilerplate and for now we've decided it's not worth i
 -}
 
 -- See Note [Constraints of ReadKnownIn and MakeKnownIn instances].
-instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term Integer
-instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term BS.ByteString
-instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term Text.Text
-instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term ()
-instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term Bool
-instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term Data
-instance (HasConstantIn DefaultUni term, DefaultUni `Contains` [a]) =>
-    MakeKnownIn DefaultUni term [a]
-instance (HasConstantIn DefaultUni term, DefaultUni `Contains` (a, b)) =>
-    MakeKnownIn DefaultUni term (a, b)
+instance MakeKnownIn DefaultUni Integer
+instance MakeKnownIn DefaultUni BS.ByteString
+instance MakeKnownIn DefaultUni Text.Text
+instance MakeKnownIn DefaultUni ()
+instance MakeKnownIn DefaultUni Bool
+instance MakeKnownIn DefaultUni Data
+instance DefaultUni `Contains` [a] => MakeKnownIn DefaultUni [a]
+instance DefaultUni `Contains` (a, b) => MakeKnownIn DefaultUni (a, b)
 
 -- See Note [Constraints of ReadKnownIn and MakeKnownIn instances].
-instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term Integer
-instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term BS.ByteString
-instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term Text.Text
-instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term ()
-instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term Bool
-instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term Data
-instance (HasConstantIn DefaultUni term, DefaultUni `Contains` [a]) =>
-    ReadKnownIn DefaultUni term [a]
-instance (HasConstantIn DefaultUni term, DefaultUni `Contains` (a, b)) =>
-    ReadKnownIn DefaultUni term (a, b)
+instance ReadKnownIn DefaultUni Integer
+instance ReadKnownIn DefaultUni BS.ByteString
+instance ReadKnownIn DefaultUni Text.Text
+instance ReadKnownIn DefaultUni ()
+instance ReadKnownIn DefaultUni Bool
+instance ReadKnownIn DefaultUni Data
+instance DefaultUni `Contains` [a] => ReadKnownIn DefaultUni [a]
+instance DefaultUni `Contains` (a, b) => ReadKnownIn DefaultUni (a, b)
 
 -- If this tells you an instance is missing, add it right above, following the pattern.
 instance TestTypesFromTheUniverseAreAllKnown DefaultUni
@@ -253,11 +249,11 @@ instance KnownTypeAst DefaultUni Int64 where
     toTypeAst _ = toTypeAst $ Proxy @Integer
 
 -- See Note [Int as Integer].
-instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term Int64 where
+instance MakeKnownIn DefaultUni Int64 where
     makeKnown mayCause = makeKnown mayCause . toInteger
     {-# INLINE makeKnown #-}
 
-instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term Int64 where
+instance ReadKnownIn DefaultUni Int64 where
     readKnown mayCause term =
         -- See Note [Performance of KnownTypeIn instances].
         -- Funnily, we don't need 'inline' here, unlike in the default implementation of 'readKnown'
@@ -272,13 +268,13 @@ instance KnownTypeAst DefaultUni Int where
     toTypeAst _ = toTypeAst $ Proxy @Integer
 
 -- See Note [Int as Integer].
-instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term Int where
+instance MakeKnownIn DefaultUni Int where
     -- This could safely just be toInteger, but this way is more explicit and it'll
     -- turn into the same thing anyway.
     makeKnown mayCause = makeKnown mayCause . intCastEq @Int @Int64
     {-# INLINE makeKnown #-}
 
-instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term Int where
+instance ReadKnownIn DefaultUni Int where
     readKnown mayCause term = intCastEq @Int64 @Int <$> readKnown mayCause term
     {-# INLINE readKnown #-}
 

plutus-core/testlib/PlutusCore/Generators/Internal/Denotation.hs

@@ -1,9 +1,10 @@
 -- | This module defines tools for associating PLC terms with their corresponding
 -- Haskell values.
 
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE GADTs           #-}
-{-# LANGUAGE RankNTypes      #-}
+{-# LANGUAGE ConstraintKinds  #-}
+{-# LANGUAGE GADTs            #-}
+{-# LANGUAGE RankNTypes       #-}
+{-# LANGUAGE TypeApplications #-}
 
 module PlutusCore.Generators.Internal.Denotation
     ( KnownType
@@ -109,7 +110,7 @@ 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 _ ->
             withTypeSchemeResult sch $ \tr ->
                 insertDenotation tr $ Denotation fun (Builtin ()) meta sch