More despair

plutus-benchmark/validation/Common.hs

@@ -141,7 +141,7 @@ type Term = UPLC.Term UPLC.DeBruijn UPLC.DefaultUni UPLC.DefaultFun ()
 peelDataArguments :: Term -> (Term, [PLC.Data])
 peelDataArguments = go []
     where
-        go acc t@(UPLC.Apply () t' arg) = case PLC.readKnown Nothing arg of
+        go acc t@(UPLC.Apply () t' arg) = case PLC.readKnown @UPLC.DefaultUni Nothing arg of
             Left _  -> (t, acc)
             Right d -> go (d:acc) t'
         go acc t = (t, acc)

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

@@ -1,3 +1,4 @@
+{-# LANGUAGE AllowAmbiguousTypes      #-}
 {-# LANGUAGE BlockArguments           #-}
 {-# LANGUAGE ConstraintKinds          #-}
 {-# LANGUAGE DataKinds                #-}
@@ -53,10 +54,13 @@ import GHC.Exts (inline, oneShot)
 import GHC.TypeLits
 import Universe
 
+class    (UniOf term ~ uni, HasConstant term) => HasConstantIn' uni term
+instance (UniOf term ~ uni, HasConstant term) => HasConstantIn' uni term
+
 -- | A constraint for \"@a@ is a 'ReadKnownIn' and 'MakeKnownIn' by means of being included
 -- in @uni@\".
 type KnownBuiltinTypeIn uni val a =
-    (uni ~ UniOf val, HasConstant val, GShow uni, GEq uni, uni `Contains` a)
+    (HasConstantIn' uni 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@\".
@@ -252,13 +256,13 @@ the cause stored in it is not forced due to @Maybe@ being a lazy data type.
 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
+    type AssociateValueMake uni a = HasConstantIn' uni
 
     -- See Note [Cause of failure].
     -- | Convert a Haskell value to the corresponding PLC val.
     -- The inverse of 'readKnown'.
     makeKnown
-        :: (uni ~ UniOf val, AssociateValueMake uni a val)
+        :: AssociateValueMake uni a val
         => Maybe cause -> a -> MakeKnownM cause val
     default makeKnown
         :: KnownBuiltinTypeIn uni val a
@@ -275,13 +279,13 @@ type MakeKnown val a = (MakeKnownIn (UniOf val) a, AssociateValueMake (UniOf val
 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
+    type AssociateValueRead uni a = HasConstantIn' uni
 
     -- See Note [Cause of failure].
     -- | Convert a PLC val to the corresponding Haskell value.
     -- The inverse of 'makeKnown'.
     readKnown
-        :: (uni ~ UniOf val, AssociateValueRead uni a val)
+        :: AssociateValueRead uni a val
         => Maybe cause -> val -> ReadKnownM cause a
     default readKnown
         :: KnownBuiltinTypeIn uni val a
@@ -293,9 +297,9 @@ class ReadKnownIn uni a where
 type ReadKnown val a = (ReadKnownIn (UniOf val) a, AssociateValueRead (UniOf val) a val)
 
 makeKnownRun
-    :: MakeKnown val a
+    :: forall val a cause. MakeKnown val a
     => Maybe cause -> a -> (ReadKnownM cause val, DList Text)
-makeKnownRun mayCause = runEmitter . runExceptT . makeKnown mayCause
+makeKnownRun mayCause = runEmitter . runExceptT . makeKnown @(UniOf val) mayCause
 {-# INLINE makeKnownRun #-}
 
 -- | Same as 'makeKnown', but allows for neither emitting nor storing the cause of a failure.
@@ -305,17 +309,18 @@ makeKnownOrFail = reoption . fst . makeKnownRun Nothing
 
 -- | Same as 'readKnown', but the cause of a potential failure is the provided term itself.
 readKnownSelf
-    :: ( ReadKnown val a
+    :: forall val a err.
+       ( ReadKnown val a
        , AsUnliftingError err, AsEvaluationFailure err
        )
     => val -> Either (ErrorWithCause err val) a
-readKnownSelf val = either throwKnownTypeErrorWithCause pure $ readKnown (Just val) val
+readKnownSelf val = either throwKnownTypeErrorWithCause pure $ readKnown @(UniOf val) (Just val) val
 {-# INLINE readKnownSelf #-}
 
 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
+    makeKnown mayCause (EvaluationSuccess x) = makeKnown @uni mayCause x
     {-# INLINE makeKnown #-}
 
 -- Catching 'EvaluationFailure' here would allow *not* to short-circuit when 'readKnown' fails
@@ -332,7 +337,7 @@ instance TypeError ('Text "‘EvaluationResult’ cannot appear in the type of a
 
 instance MakeKnownIn uni a => MakeKnownIn uni (Emitter a) where
     type AssociateValueMake uni (Emitter a) = AssociateValueMake uni a
-    makeKnown mayCause a = lift a >>= makeKnown mayCause
+    makeKnown mayCause a = lift a >>= makeKnown @uni mayCause
     {-# INLINE makeKnown #-}
 
 instance TypeError ('Text "‘Emitter’ cannot appear in the type of an argument") =>
@@ -349,12 +354,12 @@ instance ReadKnownIn uni (SomeConstant uni rep) where
     readKnown = coerceVia (\asC mayCause -> fmap SomeConstant . asC mayCause) asConstant
     {-# INLINE readKnown #-}
 
-instance uni ~ UniOf val => MakeKnownIn uni (Opaque val rep) where
+instance MakeKnownIn uni (Opaque val rep) where
     type AssociateValueMake _ _ = (~) val
     makeKnown _ = coerceArg pure  -- A faster @pure . Opaque@.
     {-# INLINE makeKnown #-}
 
-instance uni ~ UniOf val => ReadKnownIn uni (Opaque val rep) where
+instance ReadKnownIn uni (Opaque val rep) where
     type AssociateValueRead _ _ = (~) val
     readKnown _ = coerceArg pure  -- A faster @pure . Opaque@.
     {-# INLINE readKnown #-}

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 = inline makeKnown (Just ())
+    toImmediateF = inline (makeKnown @(UniOf val)) (Just ())
     {-# INLINE toImmediateF #-}
 
     -- For deferred unlifting we need to lift the 'ReadKnownM' action into 'MakeKnownM',
     -- hence 'liftEither'.
-    toDeferredF getRes = liftEither getRes >>= inline makeKnown (Just ())
+    toDeferredF getRes = liftEither getRes >>= inline (makeKnown @(UniOf val)) (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) . inline readKnown (Just ())
+    toImmediateF f = fmap (toImmediateF @val @args @res . f) . inline (readKnown @(UniOf val)) (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 <*> inline readKnown (Just ()) arg
+        pure . toDeferredF @val @args @res $! getF <*> inline (readKnown @(UniOf val)) (Just ()) arg
     {-# INLINE toDeferredF #-}
 
 -- | A class that allows us to derive a polytype for a builtin.

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

@@ -250,7 +250,7 @@ instance KnownTypeAst DefaultUni Int64 where
 
 -- See Note [Int as Integer].
 instance MakeKnownIn DefaultUni Int64 where
-    makeKnown mayCause = makeKnown mayCause . toInteger
+    makeKnown mayCause = makeKnown @DefaultUni mayCause . toInteger
     {-# INLINE makeKnown #-}
 
 instance ReadKnownIn DefaultUni Int64 where
@@ -271,11 +271,11 @@ instance KnownTypeAst DefaultUni 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
+    makeKnown mayCause = makeKnown @DefaultUni mayCause . intCastEq @Int @Int64
     {-# INLINE makeKnown #-}
 
 instance ReadKnownIn DefaultUni Int where
-    readKnown mayCause term = intCastEq @Int64 @Int <$> readKnown mayCause term
+    readKnown mayCause term = intCastEq @Int64 @Int <$> readKnown @DefaultUni mayCause term
     {-# INLINE readKnown #-}
 
 {- Note [Stable encoding of tags]