[Builtin] Make 'makeKnown' receive the term representation of the value (IntersectMBO#3957)

* [Builtin] Make 'makeKnown' receive the term representation of the value

* [Builtin] Make 'readKnown' receive the term representation of the value

Author: effectfully

plutus-core/generators/PlutusCore/Generators/Internal/TypeEvalCheck.hs

@@ -106,7 +106,7 @@ typeEvalCheckBy
     -> TypeEvalCheckM uni fun (TermOf (Term TyName Name uni fun ()) (TypeEvalCheckResult uni fun))
 typeEvalCheckBy eval (TermOf term (x :: a)) = TermOf term <$> do
     let tyExpected = runQuote . normalizeType $ toTypeAst (Proxy @a)
-        valExpected = makeKnownNoEmit x
+        valExpected = makeKnownOrFail x
     tyActual <- runQuoteT $ do
         config <- getDefTypeCheckConfig ()
         inferType config term

plutus-core/generators/PlutusCore/Generators/Internal/TypedBuiltinGen.hs

@@ -64,7 +64,7 @@ attachCoercedTerm
     => GenT m a -> GenT m (TermOf term a)
 attachCoercedTerm a = do
     x <- a
-    case makeKnownNoEmit x of
+    case makeKnownOrFail x of
         -- I've attempted to implement support for generating 'EvaluationFailure',
         -- but it turned out to be too much of a pain for something that we do not really need.
         EvaluationFailure -> fail $ concat

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

@@ -138,8 +138,8 @@ instance KnownTypeAst uni Void where
         a <- freshTyName "a"
         pure $ TyForall () a (Type ()) $ TyVar () a
 instance KnownType term Void where
-    makeKnown = absurd
-    readKnown = throwingWithCause _UnliftingError "Can't unlift a 'Void'" . Just
+    makeKnown _ = absurd
+    readKnown mayCause _ = throwingWithCause _UnliftingError "Can't unlift a 'Void'" mayCause
 type instance ToBinds Void = '[]
 
 data BuiltinErrorCall = BuiltinErrorCall

plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs

@@ -36,7 +36,8 @@ module PlutusCore.Constant.Typed
     , HasConstantIn
     , KnownTypeAst (..)
     , KnownType (..)
-    , makeKnownNoEmit
+    , readKnownSelf
+    , makeKnownOrFail
     , SomeConstant (..)
     , SomeConstantOf (..)
     ) where
@@ -408,24 +409,24 @@ newtype Opaque term (rep :: GHC.Type) = Opaque
 
 -- | Throw an 'UnliftingError' saying that the received argument is not a constant.
 throwNotAConstant
-    :: (MonadError (ErrorWithCause err term) m, AsUnliftingError err)
-    => term -> m r
-throwNotAConstant = throwingWithCause _UnliftingError "Not a constant" . Just
+    :: (MonadError (ErrorWithCause err cause) m, AsUnliftingError err)
+    => Maybe cause -> m r
+throwNotAConstant = throwingWithCause _UnliftingError "Not a constant"
 
 class AsConstant term where
     -- | Unlift from the 'Constant' constructor throwing an 'UnliftingError' if the provided @term@
     -- is not a 'Constant'.
     asConstant
-        :: (MonadError (ErrorWithCause err term) m, AsUnliftingError err)
-        => term -> m (Some (ValueOf (UniOf term)))
+        :: (MonadError (ErrorWithCause err cause) m, AsUnliftingError err)
+        => Maybe cause -> term -> m (Some (ValueOf (UniOf term)))
 
 class FromConstant term where
     -- | Wrap a Haskell value as a @term@.
     fromConstant :: Some (ValueOf (UniOf term)) -> term
 
 instance AsConstant (Term TyName Name uni fun ann) where
-    asConstant (Constant _ val) = pure val
-    asConstant term             = throwNotAConstant term
+    asConstant _        (Constant _ val) = pure val
+    asConstant mayCause _                = throwNotAConstant mayCause
 
 instance FromConstant (Term tyname name uni fun ()) where
     fromConstant = Constant ()
@@ -461,35 +462,41 @@ latter breaks on @m a@
 
 -- See Note [KnownType's defaults].
 -- | Haskell types known to exist on the PLC side.
+-- Both the methods take a @Maybe cause@ argument to report the cause of a potential failure.
+-- @cause@ is different to @term@ to support evaluators that distinguish between terms and values
+-- (@makeKnown@ normally constructs a value, but it's convenient to report the cause of a failure
+-- as a term). Note that an evaluator might require the cause to be computed lazily for best
+-- performance on the happy path and @Maybe@ ensures that even if we somehow force the argument,
+-- the cause stored in it is not forced due to @Maybe@ being a lazy data type.
 class KnownTypeAst (UniOf term) a => KnownType term a where
     -- | Convert a Haskell value to the corresponding PLC term.
     -- The inverse of 'readKnown'.
     makeKnown
-        :: ( MonadEmitter m, MonadError err m, AsEvaluationFailure err
+        :: ( MonadEmitter m, MonadError (ErrorWithCause err cause) m, AsEvaluationFailure err
            )
-        => a -> m term
+        => Maybe cause -> a -> m term
     default makeKnown
-        :: ( MonadError err m
+        :: ( MonadError (ErrorWithCause err cause) m
            , KnownBuiltinType term a
            )
-        => a -> m term
+        => Maybe cause -> a -> m term
     -- 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
+    makeKnown _ x = pure . fromConstant . someValue $! x
 
     -- | Convert a PLC term to the corresponding Haskell value.
     -- The inverse of 'makeKnown'.
     readKnown
-        :: ( MonadError (ErrorWithCause err term) m, AsUnliftingError err, AsEvaluationFailure err
+        :: ( MonadError (ErrorWithCause err cause) m, AsUnliftingError err, AsEvaluationFailure err
            )
-        => term -> m a
+        => Maybe cause -> term -> m a
     default readKnown
-        :: ( MonadError (ErrorWithCause err term) m, AsUnliftingError err
+        :: ( MonadError (ErrorWithCause err cause) m, AsUnliftingError err
            , KnownBuiltinType term a
            )
-        => term -> m a
-    readKnown term = asConstant term >>= \case
+        => Maybe cause -> term -> m a
+    readKnown mayCause term = asConstant mayCause term >>= \case
         Some (ValueOf uniAct x) -> do
             let uniExp = knownUni @_ @(UniOf term) @a
             case uniAct `geq` uniExp of
@@ -500,34 +507,57 @@ class KnownTypeAst (UniOf term) a => KnownType term a where
                             , "expected: " ++ gshow uniExp
                             , "; actual: " ++ gshow uniAct
                             ]
-                    throwingWithCause _UnliftingError err $ Just term
-
-makeKnownNoEmit :: (KnownType term a, MonadError err m, AsEvaluationFailure err) => a -> m term
-makeKnownNoEmit = unNoEmitterT . makeKnown
+                    throwingWithCause _UnliftingError err mayCause
+
+-- | Same as 'readKnown', but the cause of a potential failure is the provided term itself.
+readKnownSelf
+    :: ( KnownType term a
+       , MonadError (ErrorWithCause err term) m, AsUnliftingError err, AsEvaluationFailure err
+       )
+    => term -> m a
+readKnownSelf term = readKnown (Just term) term
+
+-- | A transformer for fitting a monad not carrying the cause of a failure into 'makeKnown'.
+newtype NoCauseT (term :: GHC.Type) m a = NoCauseT
+    { unNoCauseT :: m a
+    } deriving newtype (Functor, Applicative, Monad)
+
+instance (MonadError err m, AsEvaluationFailure err) =>
+            MonadError (ErrorWithCause err term) (NoCauseT term m) where
+    throwError _ = NoCauseT $ throwError evaluationFailure
+    NoCauseT a `catchError` h =
+        NoCauseT $ a `catchError` \err ->
+            unNoCauseT . h $ ErrorWithCause err Nothing
+
+-- | Same as 'makeKnown', but allows for neither emitting nor storing the cause of a failure.
+-- For example the monad can be simply 'EvaluationResult'.
+makeKnownOrFail :: (KnownType term a, MonadError err m, AsEvaluationFailure err) => a -> m term
+makeKnownOrFail = unNoCauseT . unNoEmitterT . makeKnown Nothing
 
 instance KnownTypeAst uni a => KnownTypeAst uni (EvaluationResult a) where
     toTypeAst _ = toTypeAst $ Proxy @a
 
 instance (KnownTypeAst (UniOf term) a, KnownType term a) =>
             KnownType term (EvaluationResult a) where
-    makeKnown EvaluationFailure     = throwError evaluationFailure
-    makeKnown (EvaluationSuccess x) = makeKnown x
+    makeKnown mayCause EvaluationFailure     = throwingWithCause _EvaluationFailure () mayCause
+    makeKnown mayCause (EvaluationSuccess x) = makeKnown mayCause x
 
     -- Catching 'EvaluationFailure' here would allow *not* to short-circuit when 'readKnown' fails
     -- to read a Haskell value of type @a@. Instead, in the denotation of the builtin function
     -- the programmer would be given an explicit 'EvaluationResult' value to handle, which means
     -- 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.
-    readKnown = throwingWithCause _UnliftingError "Error catching is not supported" . Just
+    readKnown mayCause _ =
+        throwingWithCause _UnliftingError "Error catching is not supported" mayCause
 
 instance KnownTypeAst uni a => KnownTypeAst uni (Emitter a) where
     toTypeAst _ = toTypeAst $ Proxy @a
 
 instance KnownType term a => KnownType term (Emitter a) where
-    makeKnown = unEmitter >=> makeKnown
+    makeKnown mayCause = unEmitter >=> makeKnown mayCause
     -- TODO: we really should tear 'KnownType' apart into two separate type classes.
-    readKnown = throwingWithCause _UnliftingError "Can't unlift an 'Emitter'" . Just
+    readKnown mayCause _ = throwingWithCause _UnliftingError "Can't unlift an 'Emitter'" mayCause
 
 -- | For unlifting from the 'Constant' constructor. For cases where we care about having a type tag
 -- in the denotation of a builtin rather than full unlifting to a specific built-in type.
@@ -543,8 +573,8 @@ instance (uni ~ uni', KnownTypeAst uni rep) => KnownTypeAst uni (SomeConstant un
 
 instance (HasConstantIn uni term, KnownTypeAst uni rep) =>
             KnownType term (SomeConstant uni rep) where
-    makeKnown = pure . fromConstant . unSomeConstant
-    readKnown = fmap SomeConstant . asConstant
+    makeKnown _ = pure . fromConstant . unSomeConstant
+    readKnown mayCause = fmap SomeConstant . asConstant mayCause
 
 {- | 'SomeConstantOf' is similar to 'SomeConstant': while the latter is for unlifting any
 constants, the former is for unlifting constants of a specific polymorphic built-in type
@@ -606,18 +636,18 @@ data ReadSomeConstantOf m uni f reps =
 
 instance (KnownBuiltinTypeIn uni term f, All (KnownTypeAst uni) reps, HasUniApply uni) =>
             KnownType term (SomeConstantOf uni f reps) where
-    makeKnown = pure . fromConstant . runSomeConstantOf
+    makeKnown _ = pure . fromConstant . runSomeConstantOf
 
-    readKnown term = asConstant term >>= \case
+    readKnown (mayCause :: Maybe cause) term = asConstant mayCause term >>= \case
         Some (ValueOf uni xs) -> do
             let uniF = knownUni @_ @_ @f
                 err = fromString $ concat
                     [ "Type mismatch: "
                     , "expected an application of: " ++ gshow uniF
                     , "; but got the following type: " ++ gshow uni
                     ]
-                wrongType :: (MonadError (ErrorWithCause err term) m, AsUnliftingError err) => m a
-                wrongType = throwingWithCause _UnliftingError err $ Just term
+                wrongType :: (MonadError (ErrorWithCause err cause) m, AsUnliftingError err) => m a
+                wrongType = throwingWithCause _UnliftingError err mayCause
             -- In order to prove that the type of @xs@ is an application of @f@ we need to
             -- peel all type applications off in the type of @xs@ until we get to the head and then
             -- check that the head is indeed @f@. Each peeled type application becomes a
@@ -663,12 +693,12 @@ instance KnownTypeAst uni rep => KnownTypeAst uni (Opaque term rep) where
     toTypeAst _ = toTypeAst $ Proxy @rep
 
 instance (term ~ term', KnownTypeAst (UniOf term) rep) => KnownType term (Opaque term' rep) where
-    makeKnown = pure . unOpaque
-    readKnown = pure . Opaque
+    makeKnown _ = pure . unOpaque
+    readKnown _ = pure . Opaque
 
 instance uni `Contains` Integer       => KnownTypeAst uni Integer
 instance uni `Contains` BS.ByteString => KnownTypeAst uni BS.ByteString
-instance uni `Contains` Text.Text          => KnownTypeAst uni Text.Text
+instance uni `Contains` Text.Text     => KnownTypeAst uni Text.Text
 instance uni `Contains` ()            => KnownTypeAst uni ()
 instance uni `Contains` Bool          => KnownTypeAst uni Bool
 instance uni `Contains` [a]           => KnownTypeAst uni [a]
@@ -677,7 +707,7 @@ instance uni `Contains` Data          => KnownTypeAst uni Data
 
 instance KnownBuiltinType term Integer       => KnownType term Integer
 instance KnownBuiltinType term BS.ByteString => KnownType term BS.ByteString
-instance KnownBuiltinType term Text.Text          => KnownType term Text.Text
+instance KnownBuiltinType term Text.Text     => KnownType term Text.Text
 instance KnownBuiltinType term ()            => KnownType term ()
 instance KnownBuiltinType term Bool          => KnownType term Bool
 instance KnownBuiltinType term [a]           => KnownType term [a]
@@ -697,11 +727,11 @@ instance uni `Includes` Integer => KnownTypeAst uni Int where
 
 -- See Note [Int as Integer].
 instance KnownBuiltinType term Integer => KnownType term Int where
-    makeKnown = makeKnown . toInteger
-    readKnown term = do
-        i :: Integer <- readKnown term
+    makeKnown mayCause = makeKnown mayCause . toInteger
+    readKnown mayCause term = do
+        i :: Integer <- readKnown mayCause term
         unless (fromIntegral (minBound :: Int) <= i && i <= fromIntegral (maxBound :: Int)) $
-            throwingWithCause _EvaluationFailure () $ Just term
+            throwingWithCause _EvaluationFailure () mayCause
         pure $ fromIntegral i
 
 -- Utils

plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs

@@ -36,7 +36,6 @@ import           PlutusCore.Name
 import           PlutusCore.Pretty                       (PrettyConfigPlc, PrettyConst)
 
 import           Control.Monad.Except
-import           Control.Monad.Morph
 import           Control.Monad.Reader
 import           Control.Monad.ST
 import           Data.Array
@@ -69,7 +68,7 @@ evalBuiltinApp
     -> BuiltinRuntime (CkValue uni fun)
     -> CkM uni fun s (CkValue uni fun)
 evalBuiltinApp term runtime@(BuiltinRuntime sch x _) = case sch of
-    TypeSchemeResult _ -> makeKnown x
+    TypeSchemeResult _ -> makeKnown (Just term) x
     _                  -> pure $ VBuiltin term runtime
 
 ckValueToTerm :: CkValue uni fun -> Term TyName Name uni fun ()
@@ -95,29 +94,22 @@ data CkUserError =
     CkEvaluationFailure -- Error has been called or a builtin application has failed
     deriving (Show, Eq, Generic, NFData)
 
--- | The CK machine-specific 'EvaluationException' parameterized over @term@.
-type CkEvaluationExceptionCarrying term fun =
-    EvaluationException CkUserError (MachineError fun) term
+-- | The CK machine-specific 'EvaluationException'.
+type CkEvaluationException uni fun =
+    EvaluationException CkUserError (MachineError fun) (Term TyName Name uni fun ())
 
--- See Note [Being generic over @term@ in 'CekM']
-type CkCarryingM term uni fun s =
+type CkM uni fun s =
     ReaderT (CkEnv uni fun s)
-        (ExceptT (CkEvaluationExceptionCarrying term fun)
+        (ExceptT (CkEvaluationException uni fun)
             (ST s))
 
--- | The CK machine-specific 'EvaluationException'.
-type CkEvaluationException uni fun =
-    CkEvaluationExceptionCarrying (Term TyName Name uni fun ()) fun
-
 instance AsEvaluationFailure CkUserError where
     _EvaluationFailure = _EvaluationFailureVia CkEvaluationFailure
 
 instance Pretty CkUserError where
     pretty CkEvaluationFailure = "The provided Plutus code called 'error'."
 
-type CkM uni fun s = CkCarryingM (Term TyName Name uni fun ()) uni fun s
-
-instance MonadEmitter (CkCarryingM term uni fun s) where
+instance MonadEmitter (CkM uni fun s) where
     emit str = do
         mayLogsRef <- asks ckEnvMayEmitRef
         case mayLogsRef of
@@ -130,8 +122,8 @@ instance FromConstant (CkValue uni fun) where
     fromConstant = VCon
 
 instance AsConstant (CkValue uni fun) where
-    asConstant (VCon val) = pure val
-    asConstant term       = throwNotAConstant term
+    asConstant _        (VCon val) = pure val
+    asConstant mayCause _          = throwNotAConstant mayCause
 
 data Frame uni fun
     = FrameApplyFun (CkValue uni fun)                       -- ^ @[V _]@
@@ -304,15 +296,13 @@ applyEvaluate
     -> CkM uni fun s (Term TyName Name uni fun ())
 applyEvaluate stack (VLamAbs name _ body) arg = stack |> substituteDb name (ckValueToTerm arg) body
 applyEvaluate stack (VBuiltin term (BuiltinRuntime sch f _)) arg = do
-    let term' = Apply () term $ ckValueToTerm arg
+    let argTerm = ckValueToTerm arg
+        term' = Apply () term argTerm
     case sch of
         -- It's only possible to apply a builtin application if the builtin expects a term
         -- argument next.
         TypeSchemeArrow _ schB -> do
-            -- The builtin application machinery wants to be able to throw a 'CekValue' rather
-            -- than a 'Term', hence 'withErrorDischarging'.
-            let dischargeError = hoist $ withExceptT $ mapCauseInMachineException ckValueToTerm
-            x <- dischargeError $ readKnown arg
+            x <- readKnown (Just argTerm) arg
             let noCosting = error "The CK machine does not support costing"
                 runtime' = BuiltinRuntime schB (f x) noCosting
             res <- evalBuiltinApp term' runtime'
@@ -374,4 +364,4 @@ readKnownCk
     => BuiltinsRuntime fun (CkValue uni fun)
     -> Term TyName Name uni fun ()
     -> Either (CkEvaluationException uni fun) a
-readKnownCk runtime = evaluateCkNoEmit runtime >=> readKnown
+readKnownCk runtime = evaluateCkNoEmit runtime >=> readKnownSelf

plutus-core/plutus-ir/src/PlutusIR/Core/Type.hs

@@ -125,8 +125,8 @@ data Term tyname name uni fun a =
 type instance UniOf (Term tyname name uni fun ann) = uni
 
 instance AsConstant (Term tyname name uni fun ann) where
-    asConstant (Constant _ val) = pure val
-    asConstant term             = throwNotAConstant term
+    asConstant _        (Constant _ val) = pure val
+    asConstant mayCause _                = throwNotAConstant mayCause
 
 instance FromConstant (Term tyname name uni fun ()) where
     fromConstant = Constant ()

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs

@@ -96,8 +96,8 @@ instance TermLike (Term name uni fun) TPLC.TyName name uni fun where
     error    = \ann _ -> Error ann
 
 instance TPLC.AsConstant (Term name uni fun ann) where
-    asConstant (Constant _ val) = pure val
-    asConstant term             = TPLC.throwNotAConstant term
+    asConstant _        (Constant _ val) = pure val
+    asConstant mayCause _                = TPLC.throwNotAConstant mayCause
 
 instance TPLC.FromConstant (Term name uni fun ()) where
     fromConstant = Constant ()