From c1030ccd920ef39f108a7d7899cc3f39901f4fbc Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Sat, 26 Feb 2022 16:56:48 +0300
Subject: [PATCH 01/17] [Builtins] Defer 'readKnown' until full saturation

---
 .../src/PlutusCore/Builtin/KnownType.hs       | 26 +-----
 .../src/PlutusCore/Builtin/Runtime.hs         | 92 +++++++++++++------
 .../src/PlutusCore/Evaluation/Machine/Ck.hs   | 18 ++--
 .../Evaluation/Machine/Cek/Internal.hs        | 16 ++--
 .../iteAtIntegerWrongCondType.plc.golden      |  2 +-
 .../iteAtIntegerWrongCondType.uplc.golden     |  2 +-
 6 files changed, 87 insertions(+), 69 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs
index 2e937472fd0..e8d40183b2e 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs
@@ -15,10 +15,8 @@
 {-# LANGUAGE UndecidableSuperClasses #-}
 
 module PlutusCore.Builtin.KnownType
-    ( MakeKnownError
-    , ReadKnownError
+    ( ReadKnownError
     , throwReadKnownErrorWithCause
-    , throwMakeKnownErrorWithCause
     , KnownBuiltinTypeIn
     , KnownBuiltinType
     , readKnownConstant
@@ -154,36 +152,20 @@ Overall, asking the user to manually unlift from @SomeConstant uni [a]@ is just
 faster than any kind of fancy encoding.
 -}
 
--- | The type of errors that 'makeKnown' can return.
-data MakeKnownError
-    = MakeKnownEvaluationFailure
-    deriving stock (Eq)
-
 -- | The type of errors that 'readKnown' can return.
 data ReadKnownError
     = ReadKnownUnliftingError UnliftingError
     | ReadKnownEvaluationFailure
     deriving stock (Eq)
 
-makeClassyPrisms ''MakeKnownError
 makeClassyPrisms ''ReadKnownError
 
-instance AsEvaluationFailure MakeKnownError where
-    _EvaluationFailure = _EvaluationFailureVia MakeKnownEvaluationFailure
-
 instance AsUnliftingError ReadKnownError where
     _UnliftingError = _ReadKnownUnliftingError
 
 instance AsEvaluationFailure ReadKnownError where
     _EvaluationFailure = _EvaluationFailureVia ReadKnownEvaluationFailure
 
--- | Throw a @ErrorWithCause ReadKnownError cause@.
-throwMakeKnownErrorWithCause
-    :: (MonadError (ErrorWithCause err cause) m, AsEvaluationFailure err)
-    => ErrorWithCause MakeKnownError cause -> m void
-throwMakeKnownErrorWithCause (ErrorWithCause rkErr cause) = case rkErr of
-    MakeKnownEvaluationFailure -> throwingWithCause _EvaluationFailure () cause
-
 -- | Throw a @ErrorWithCause ReadKnownError cause@.
 throwReadKnownErrorWithCause
     :: (MonadError (ErrorWithCause err cause) m, AsUnliftingError err, AsEvaluationFailure err)
@@ -232,10 +214,10 @@ readKnownConstant mayCause val = asConstant mayCause val >>= oneShot \case
 class uni ~ UniOf val => KnownTypeIn uni val a where
     -- | Convert a Haskell value to the corresponding PLC val.
     -- The inverse of 'readKnown'.
-    makeKnown :: Maybe cause -> a -> ExceptT (ErrorWithCause MakeKnownError cause) Emitter val
+    makeKnown :: Maybe cause -> a -> ExceptT (ErrorWithCause ReadKnownError cause) Emitter val
     default makeKnown
         :: KnownBuiltinType val a
-        => Maybe cause -> a -> ExceptT (ErrorWithCause MakeKnownError cause) Emitter val
+        => Maybe cause -> a -> ExceptT (ErrorWithCause ReadKnownError cause) Emitter 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.
@@ -257,7 +239,7 @@ type KnownType val a = (KnownTypeAst (UniOf val) a, KnownTypeIn (UniOf val) val
 
 makeKnownRun
     :: KnownTypeIn uni val a
-    => Maybe cause -> a -> (Either (ErrorWithCause MakeKnownError cause) val, DList Text)
+    => Maybe cause -> a -> (Either (ErrorWithCause ReadKnownError cause) val, DList Text)
 makeKnownRun mayCause = runEmitter . runExceptT . makeKnown mayCause
 {-# INLINE makeKnownRun #-}
 
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index 8adae67b535..69803f01d8a 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -1,3 +1,6 @@
+{-# LANGUAGE RankNTypes     #-}
+{-# LANGUAGE TypeFamilies   #-}
+
 {-# LANGUAGE DataKinds      #-}
 {-# LANGUAGE GADTs          #-}
 {-# LANGUAGE KindSignatures #-}
@@ -12,7 +15,6 @@ import PlutusPrelude
 import PlutusCore.Builtin.HasConstant
 import PlutusCore.Builtin.Meaning
 import PlutusCore.Builtin.TypeScheme
-import PlutusCore.Core
 import PlutusCore.Evaluation.Machine.Exception
 
 import Control.DeepSeq
@@ -23,21 +25,31 @@ import Data.Kind qualified as GHC (Type)
 import GHC.Exts (inline)
 import PlutusCore.Builtin.KnownType
 
+import PlutusCore.Builtin.Emitter
+import PlutusCore.Evaluation.Machine.ExBudget
+import PlutusCore.Evaluation.Machine.ExMemory
+
+data Nat = Z | S Nat
+
 -- | Same as 'TypeScheme' except this one doesn't contain any evaluation-irrelevant types stuff.
-data RuntimeScheme val (args :: [GHC.Type]) res where
-    RuntimeSchemeResult
-        :: KnownTypeIn (UniOf val) val res
-        => RuntimeScheme val '[] res
-    RuntimeSchemeArrow
-        :: KnownTypeIn (UniOf val) val arg
-        => RuntimeScheme val args res
-        -> RuntimeScheme val (arg ': args) res
-    RuntimeSchemeAll
-        :: RuntimeScheme val args res
-        -> RuntimeScheme val args res
+data RuntimeScheme n where
+    RuntimeSchemeResult :: RuntimeScheme 'Z
+    RuntimeSchemeArrow :: RuntimeScheme n -> RuntimeScheme ('S n)
+    RuntimeSchemeAll :: RuntimeScheme n -> RuntimeScheme n
+
+type MakeKnownM = ExceptT (ErrorWithCause ReadKnownError ()) Emitter
+type ReadKnownM = Either (ErrorWithCause ReadKnownError ())
+
+type family ToDenotationType val (n :: Nat) :: GHC.Type where
+    ToDenotationType val 'Z     = MakeKnownM val
+    ToDenotationType val ('S n) = val -> ReadKnownM (ToDenotationType val n)
+
+type family ToCostingType (n :: Nat) :: GHC.Type where
+    ToCostingType 'Z     = ExBudget
+    ToCostingType ('S n) = ExMemory -> ToCostingType n
 
 -- we use strictdata, so this is just for the purpose of completeness
-instance NFData (RuntimeScheme val args res) where
+instance NFData (RuntimeScheme n) where
     rnf r = case r of
         RuntimeSchemeResult    -> rwhnf r
         RuntimeSchemeArrow arg -> rnf arg
@@ -60,13 +72,15 @@ instance NFData (RuntimeScheme val args res) where
 -- All the three are in sync in terms of partial instantiatedness due to 'TypeScheme' being a
 -- GADT and 'FoldArgs' and 'FoldArgsEx' operating on the index of that GADT.
 data BuiltinRuntime val =
-    forall args res. BuiltinRuntime
-        (RuntimeScheme val args res)
-        ~(FoldArgs args res)  -- Must be lazy, because we don't want to compute the denotation when
-                              -- it's fully saturated before figuring out what it's going to cost.
-        ~(FoldArgsEx args)    -- We make this lazy, so that evaluators that don't care about costing
-                              -- can put @undefined@ here. TODO: we should test if making this
-                              -- strict introduces any measurable speedup.
+    forall n. BuiltinRuntime
+        (RuntimeScheme n)
+        ~(ToDenotationType val n)  -- Must be lazy, because we don't want to compute the denotation
+                                   -- when it's fully saturated before figuring out what it's going
+                                   -- to cost.
+        ~(ToCostingType n)         -- We make this lazy, so that evaluators that don't care about
+                                   -- costing can put @undefined@ here.
+                                   -- TODO: we should test if making this strict introduces any
+                                   -- measurable speedup.
 
 instance NFData (BuiltinRuntime val) where
     rnf (BuiltinRuntime rs f exF) = rnf rs `seq` f `seq` rwhnf exF
@@ -78,18 +92,40 @@ newtype BuiltinsRuntime fun val = BuiltinsRuntime
 
 deriving newtype instance (NFData fun) => NFData (BuiltinsRuntime fun val)
 
--- | Convert a 'TypeScheme' to a 'RuntimeScheme'.
-typeSchemeToRuntimeScheme :: TypeScheme val args res -> RuntimeScheme val args res
-typeSchemeToRuntimeScheme TypeSchemeResult       = RuntimeSchemeResult
-typeSchemeToRuntimeScheme (TypeSchemeArrow schB) =
-    RuntimeSchemeArrow $ typeSchemeToRuntimeScheme schB
-typeSchemeToRuntimeScheme (TypeSchemeAll _ schK) =
-    RuntimeSchemeAll $ typeSchemeToRuntimeScheme schK
+data UnliftMode
+    = UnliftImmediately
+    | UnliftWhenSaturated
+
+unliftMode :: UnliftMode
+unliftMode = UnliftImmediately
 
 -- | Instantiate a 'BuiltinMeaning' given denotations of built-in functions and a cost model.
 toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
 toBuiltinRuntime cost (BuiltinMeaning sch f exF) =
-    BuiltinRuntime (typeSchemeToRuntimeScheme sch) f (exF cost)
+    go sch $ \sch' toF' toExF' -> (BuiltinRuntime sch' $! (toF' $ pure f)) $! (toExF' $ exF cost) where
+        go
+            :: TypeScheme val args res
+            -> (forall n.
+                    RuntimeScheme n
+                -> (ReadKnownM (FoldArgs args res) -> ToDenotationType val n)
+                -> (FoldArgsEx args -> ToCostingType n)
+                -> BuiltinRuntime val)
+            -> BuiltinRuntime val
+        go TypeSchemeResult       k =
+            k
+                RuntimeSchemeResult
+                (\getRes -> liftEither getRes >>= makeKnown (Just ()))
+                id
+        go (TypeSchemeArrow schB) k =
+            go schB $ \sch' toF' toExF' -> k
+                (RuntimeSchemeArrow sch')
+                (\getF x -> do
+                    let getVal = readKnown (Just ()) x
+                    case unliftMode of
+                        UnliftImmediately   -> getVal <&> \val -> toF' (($ val) <$> getF)
+                        UnliftWhenSaturated -> pure . toF' $ getF <*> getVal)
+                (toExF' .)
+        go (TypeSchemeAll _ schK) k = go schK $ k . RuntimeSchemeAll
 
 -- See Note [Inlining meanings of builtins].
 -- | Calculate runtime info for all built-in functions given denotations of builtins
diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
index 6363d5843ea..bc4446d0b1b 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
@@ -66,14 +66,14 @@ evalBuiltinApp
     :: Term TyName Name uni fun ()
     -> BuiltinRuntime (CkValue uni fun)
     -> CkM uni fun s (CkValue uni fun)
-evalBuiltinApp term runtime@(BuiltinRuntime sch x _) = case sch of
+evalBuiltinApp term runtime@(BuiltinRuntime sch getX _) = case sch of
     RuntimeSchemeResult -> do
-        let (errOrRes, logs) = makeKnownRun (Just term) x
+        let (errOrRes, logs) = runEmitter $ runExceptT getX
         emitCkM logs
         case errOrRes of
-            Left err  -> throwMakeKnownErrorWithCause err
-            Right res -> pure res
-    _ -> pure $ VBuiltin term runtime
+            Left err -> throwReadKnownErrorWithCause $ term <$ err
+            Right x  -> pure x
+    _                   -> pure $ VBuiltin term runtime
 
 ckValueToTerm :: CkValue uni fun -> Term TyName Name uni fun ()
 ckValueToTerm = \case
@@ -306,11 +306,11 @@ applyEvaluate stack (VBuiltin term (BuiltinRuntime sch f _)) arg = do
     case sch of
         -- It's only possible to apply a builtin application if the builtin expects a term
         -- argument next.
-        RuntimeSchemeArrow schB -> case readKnown (Just argTerm) arg  of
-            Left err -> throwReadKnownErrorWithCause err
-            Right x  -> do
+        RuntimeSchemeArrow schB -> case f arg of
+            Left err  -> throwReadKnownErrorWithCause $ term' <$ err
+            Right app -> do
                 let noCosting = error "The CK machine does not support costing"
-                    runtime' = BuiltinRuntime schB (f x) noCosting
+                    runtime' = BuiltinRuntime schB app noCosting
                 res <- evalBuiltinApp term' runtime'
                 stack <| res
         _ ->
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
index d2ed340a4dc..2aadbc12ecd 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
@@ -561,14 +561,14 @@ evalBuiltinApp
     -> CekValEnv uni fun
     -> BuiltinRuntime (CekValue uni fun)
     -> CekM uni fun s (CekValue uni fun)
-evalBuiltinApp fun term env runtime@(BuiltinRuntime sch x cost) = case sch of
+evalBuiltinApp fun term env runtime@(BuiltinRuntime sch getX cost) = case sch of
     RuntimeSchemeResult -> do
         spendBudgetCek (BBuiltinApp fun) cost
-        let !(errOrRes, logs) = makeKnownRun (Just term) x
+        let !(errOrRes, logs) = runEmitter $ runExceptT getX
         ?cekEmitter logs
         case errOrRes of
-            Left err  -> throwMakeKnownErrorWithCause err
-            Right res -> pure res
+            Left err -> throwReadKnownErrorWithCause $ term <$ err
+            Right x  -> pure x
     _ -> pure $ VBuiltin fun term env runtime
 {-# INLINE evalBuiltinApp #-}
 
@@ -708,13 +708,13 @@ enterComputeCek = computeCek (toWordArray 0) where
         case sch of
             -- It's only possible to apply a builtin application if the builtin expects a term
             -- argument next.
-            RuntimeSchemeArrow schB -> case readKnown (Just argTerm) arg of
-                Left err -> throwReadKnownErrorWithCause err
-                Right x  -> do
+            RuntimeSchemeArrow schB -> case f arg of
+                Left err  -> throwReadKnownErrorWithCause $ term' <$ err
+                Right app -> do
                     -- TODO: should we bother computing that 'ExMemory' eagerly? We may not need it.
                     -- We pattern match on @arg@ twice: in 'readKnown' and in 'toExMemory'.
                     -- Maybe we could fuse the two?
-                    let runtime' = BuiltinRuntime schB (f x) . exF $ toExMemory arg
+                    let runtime' = BuiltinRuntime schB app . exF $ toExMemory arg
                     res <- evalBuiltinApp fun term' env runtime'
                     returnCek unbudgetedSteps ctx res
             _ ->
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
index 9b591585958..6f68e70e866 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
@@ -1,4 +1,4 @@
 (Left An error has occurred:  error:
 Could not unlift a builtin:
 Type mismatch: expected: bool; actual: string
-Caused by: (con string "11 <= 22"))
\ No newline at end of file
+Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
index 9b591585958..6f68e70e866 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
@@ -1,4 +1,4 @@
 (Left An error has occurred:  error:
 Could not unlift a builtin:
 Type mismatch: expected: bool; actual: string
-Caused by: (con string "11 <= 22"))
\ No newline at end of file
+Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file

From ae0a821f5420c9f023319c670aded5b2756cbd43 Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Wed, 2 Mar 2022 16:05:56 +0300
Subject: [PATCH 02/17] Use 'UnliftWhenSaturated' instead of
 'UnliftImmediately'

---
 plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs | 2 +-
 .../Golden/iteAtIntegerWrongCondType.plc.golden           | 8 ++++----
 .../Golden/iteAtIntegerWrongCondType.uplc.golden          | 8 ++++----
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index 69803f01d8a..d54bf6ac703 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -97,7 +97,7 @@ data UnliftMode
     | UnliftWhenSaturated
 
 unliftMode :: UnliftMode
-unliftMode = UnliftImmediately
+unliftMode = UnliftWhenSaturated
 
 -- | Instantiate a 'BuiltinMeaning' given denotations of built-in functions and a cost model.
 toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
index 6f68e70e866..17e15ddf9b2 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
@@ -1,4 +1,4 @@
-(Left An error has occurred:  error:
-Could not unlift a builtin:
-Type mismatch: expected: bool; actual: string
-Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file
+(Right [
+  [ (force (builtin ifThenElse)) (con string "11 <= 22") ]
+  (con string "\172(11 <= 22)")
+])
\ No newline at end of file
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
index 6f68e70e866..17e15ddf9b2 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
@@ -1,4 +1,4 @@
-(Left An error has occurred:  error:
-Could not unlift a builtin:
-Type mismatch: expected: bool; actual: string
-Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file
+(Right [
+  [ (force (builtin ifThenElse)) (con string "11 <= 22") ]
+  (con string "\172(11 <= 22)")
+])
\ No newline at end of file

From 4388d6c64c5784d06d9c9e3acf2e27ee017f7ccf Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Thu, 3 Mar 2022 00:11:30 +0300
Subject: [PATCH 03/17] Revert "Use 'UnliftWhenSaturated' instead of
 'UnliftImmediately'"

This reverts commit 19656b670030d30e8825a0e8b4fa589ab8626cb2.
---
 plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs | 2 +-
 .../Golden/iteAtIntegerWrongCondType.plc.golden           | 8 ++++----
 .../Golden/iteAtIntegerWrongCondType.uplc.golden          | 8 ++++----
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index d54bf6ac703..69803f01d8a 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -97,7 +97,7 @@ data UnliftMode
     | UnliftWhenSaturated
 
 unliftMode :: UnliftMode
-unliftMode = UnliftWhenSaturated
+unliftMode = UnliftImmediately
 
 -- | Instantiate a 'BuiltinMeaning' given denotations of built-in functions and a cost model.
 toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
index 17e15ddf9b2..6f68e70e866 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
@@ -1,4 +1,4 @@
-(Right [
-  [ (force (builtin ifThenElse)) (con string "11 <= 22") ]
-  (con string "\172(11 <= 22)")
-])
\ No newline at end of file
+(Left An error has occurred:  error:
+Could not unlift a builtin:
+Type mismatch: expected: bool; actual: string
+Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
index 17e15ddf9b2..6f68e70e866 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
@@ -1,4 +1,4 @@
-(Right [
-  [ (force (builtin ifThenElse)) (con string "11 <= 22") ]
-  (con string "\172(11 <= 22)")
-])
\ No newline at end of file
+(Left An error has occurred:  error:
+Could not unlift a builtin:
+Type mismatch: expected: bool; actual: string
+Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file

From 932756a8a6d5d96a156e1c5e4fca6b69d374d59c Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Wed, 9 Mar 2022 14:57:27 +0300
Subject: [PATCH 04/17] Correct causes for unlifting errors

---
 plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs | 2 +-
 .../src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs    | 2 +-
 .../test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden | 2 +-
 .../Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden     | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
index bc4446d0b1b..40766687e91 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
@@ -307,7 +307,7 @@ applyEvaluate stack (VBuiltin term (BuiltinRuntime sch f _)) arg = do
         -- It's only possible to apply a builtin application if the builtin expects a term
         -- argument next.
         RuntimeSchemeArrow schB -> case f arg of
-            Left err  -> throwReadKnownErrorWithCause $ term' <$ err
+            Left err  -> throwReadKnownErrorWithCause $ argTerm <$ err
             Right app -> do
                 let noCosting = error "The CK machine does not support costing"
                     runtime' = BuiltinRuntime schB app noCosting
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
index 2aadbc12ecd..077ff541096 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
@@ -709,7 +709,7 @@ enterComputeCek = computeCek (toWordArray 0) where
             -- It's only possible to apply a builtin application if the builtin expects a term
             -- argument next.
             RuntimeSchemeArrow schB -> case f arg of
-                Left err  -> throwReadKnownErrorWithCause $ term' <$ err
+                Left err  -> throwReadKnownErrorWithCause $ argTerm <$ err
                 Right app -> do
                     -- TODO: should we bother computing that 'ExMemory' eagerly? We may not need it.
                     -- We pattern match on @arg@ twice: in 'readKnown' and in 'toExMemory'.
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
index 6f68e70e866..9b591585958 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
@@ -1,4 +1,4 @@
 (Left An error has occurred:  error:
 Could not unlift a builtin:
 Type mismatch: expected: bool; actual: string
-Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file
+Caused by: (con string "11 <= 22"))
\ No newline at end of file
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
index 6f68e70e866..9b591585958 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
@@ -1,4 +1,4 @@
 (Left An error has occurred:  error:
 Could not unlift a builtin:
 Type mismatch: expected: bool; actual: string
-Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file
+Caused by: (con string "11 <= 22"))
\ No newline at end of file

From 6c9a09ac889354e24315f302955bb8002934fbf7 Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Wed, 9 Mar 2022 22:37:05 +0300
Subject: [PATCH 05/17] Use 'UnliftWhenSaturated' instead of
 'UnliftImmediately'

---
 plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs | 2 +-
 .../Golden/iteAtIntegerWrongCondType.plc.golden           | 8 ++++----
 .../Golden/iteAtIntegerWrongCondType.uplc.golden          | 8 ++++----
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index 69803f01d8a..d54bf6ac703 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -97,7 +97,7 @@ data UnliftMode
     | UnliftWhenSaturated
 
 unliftMode :: UnliftMode
-unliftMode = UnliftImmediately
+unliftMode = UnliftWhenSaturated
 
 -- | Instantiate a 'BuiltinMeaning' given denotations of built-in functions and a cost model.
 toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
index 9b591585958..17e15ddf9b2 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
@@ -1,4 +1,4 @@
-(Left An error has occurred:  error:
-Could not unlift a builtin:
-Type mismatch: expected: bool; actual: string
-Caused by: (con string "11 <= 22"))
\ No newline at end of file
+(Right [
+  [ (force (builtin ifThenElse)) (con string "11 <= 22") ]
+  (con string "\172(11 <= 22)")
+])
\ No newline at end of file
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
index 9b591585958..17e15ddf9b2 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
@@ -1,4 +1,4 @@
-(Left An error has occurred:  error:
-Could not unlift a builtin:
-Type mismatch: expected: bool; actual: string
-Caused by: (con string "11 <= 22"))
\ No newline at end of file
+(Right [
+  [ (force (builtin ifThenElse)) (con string "11 <= 22") ]
+  (con string "\172(11 <= 22)")
+])
\ No newline at end of file

From f4a237ce31e93d78ae86b61d79ce0f9cf0ebcfeb Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Wed, 9 Mar 2022 23:03:59 +0300
Subject: [PATCH 06/17] Playing with bangs

---
 plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index d54bf6ac703..266b046bfb4 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE BangPatterns   #-}
 {-# LANGUAGE RankNTypes     #-}
 {-# LANGUAGE TypeFamilies   #-}
 
@@ -102,7 +103,7 @@ unliftMode = UnliftWhenSaturated
 -- | Instantiate a 'BuiltinMeaning' given denotations of built-in functions and a cost model.
 toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
 toBuiltinRuntime cost (BuiltinMeaning sch f exF) =
-    go sch $ \sch' toF' toExF' -> (BuiltinRuntime sch' $! (toF' $ pure f)) $! (toExF' $ exF cost) where
+    go sch $ \sch' toF' toExF' -> BuiltinRuntime sch' (toF' $ pure f) (toExF' $ exF cost) where
         go
             :: TypeScheme val args res
             -> (forall n.
@@ -120,7 +121,7 @@ toBuiltinRuntime cost (BuiltinMeaning sch f exF) =
             go schB $ \sch' toF' toExF' -> k
                 (RuntimeSchemeArrow sch')
                 (\getF x -> do
-                    let getVal = readKnown (Just ()) x
+                    let !getVal = readKnown (Just ()) x
                     case unliftMode of
                         UnliftImmediately   -> getVal <&> \val -> toF' (($ val) <$> getF)
                         UnliftWhenSaturated -> pure . toF' $ getF <*> getVal)

From e3073ec34ef02e8fbe74c5816d001f0797674a47 Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Thu, 10 Mar 2022 01:12:20 +0300
Subject: [PATCH 07/17] Remove a bang

---
 plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index 266b046bfb4..492fea63ada 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE BangPatterns   #-}
 {-# LANGUAGE RankNTypes     #-}
 {-# LANGUAGE TypeFamilies   #-}
 
@@ -121,7 +120,7 @@ toBuiltinRuntime cost (BuiltinMeaning sch f exF) =
             go schB $ \sch' toF' toExF' -> k
                 (RuntimeSchemeArrow sch')
                 (\getF x -> do
-                    let !getVal = readKnown (Just ()) x
+                    let getVal = readKnown (Just ()) x
                     case unliftMode of
                         UnliftImmediately   -> getVal <&> \val -> toF' (($ val) <$> getF)
                         UnliftWhenSaturated -> pure . toF' $ getF <*> getVal)

From b6743db2a5c1eb171b6c685eed868fbc695cf588 Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Wed, 30 Mar 2022 11:45:03 +0300
Subject: [PATCH 08/17] Parallel 'TypeScheme' and 'RuntimeScheme'

---
 .../examples/PlutusCore/Examples/Builtins.hs  |  6 +-
 .../src/PlutusCore/Builtin/Meaning.hs         | 70 +++++++++++++++----
 .../src/PlutusCore/Builtin/Runtime.hs         | 69 ++++++------------
 .../src/PlutusCore/Builtin/TypeScheme.hs      | 19 -----
 4 files changed, 82 insertions(+), 82 deletions(-)

diff --git a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
index 0bd74f4351c..aa469ac487c 100644
--- a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
+++ b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
@@ -129,9 +129,11 @@ instance (ToBuiltinMeaning uni fun1, ToBuiltinMeaning uni fun2) =>
     type CostingPart uni (Either fun1 fun2) = (CostingPart uni fun1, CostingPart uni fun2)
 
     toBuiltinMeaning (Left  fun) = case toBuiltinMeaning fun of
-        BuiltinMeaning sch toF toExF -> BuiltinMeaning sch toF (toExF . fst)
+        BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch fImm fDef toExF) ->
+            BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch fImm fDef (toExF . fst))
     toBuiltinMeaning (Right fun) = case toBuiltinMeaning fun of
-        BuiltinMeaning sch toF toExF -> BuiltinMeaning sch toF (toExF . snd)
+        BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch fImm fDef toExF) ->
+            BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch fImm fDef (toExF . snd))
 
 defBuiltinsRuntimeExt
     :: HasConstantIn DefaultUni term
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
index e6383997b3a..045baf2cfff 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
@@ -17,21 +17,36 @@
 
 module PlutusCore.Builtin.Meaning where
 
+import PlutusPrelude
+
 import PlutusCore.Builtin.Elaborate
 import PlutusCore.Builtin.HasConstant
 import PlutusCore.Builtin.KnownKind
 import PlutusCore.Builtin.KnownType
 import PlutusCore.Builtin.KnownTypeAst
+import PlutusCore.Builtin.Runtime
 import PlutusCore.Builtin.TypeScheme
 import PlutusCore.Core
 import PlutusCore.Name
 
+import Control.Monad.Except
 import Data.Array
 import Data.Kind qualified as GHC
 import Data.Proxy
 import Data.Some.GADT
+import GHC.Exts (inline)
 import GHC.TypeLits
 
+-- | Turn a list of Haskell types @args@ into a functional type ending in @res@.
+--
+-- >>> :set -XDataKinds
+-- >>> :kind! FoldArgs [Text, Bool] Integer
+-- FoldArgs [Text, Bool] Integer :: *
+-- = Text -> Bool -> Integer
+type family FoldArgs args res where
+    FoldArgs '[]           res = res
+    FoldArgs (arg ': args) res = arg -> FoldArgs args res
+
 -- | The meaning of a built-in function consists of its type represented as a 'TypeScheme',
 -- its Haskell denotation and a costing function (both in uninstantiated form).
 --
@@ -47,22 +62,13 @@ data BuiltinMeaning val cost =
     forall args res. BuiltinMeaning
         (TypeScheme val args res)
         (FoldArgs args res)
-        (cost -> FoldArgsEx args)
--- I tried making it @(forall val. HasConstantIn uni val => TypeScheme val args res)@ instead of
--- @TypeScheme val args res@, but 'makeBuiltinMeaning' has to talk about
--- @KnownPolytype binds val args res a@ (note the @val@), because instances of 'KnownMonotype'
--- are constrained with @KnownType val arg@ and @KnownType val res@, and so the earliest we can
--- generalize from @val@ to @UniOf val@ is in 'toBuiltinMeaning'.
--- Besides, for 'BuiltinRuntime' we want to have a concrete 'TypeScheme' anyway for performance
--- reasons (there isn't much point in caching a value of a type with a constraint as it becomes a
--- function at runtime anyway, due to constraints being compiled as dictionaries).
+        (BuiltinRuntimeOptions (Length args) val cost)
 
 -- | A type class for \"each function from a set of built-in functions has a 'BuiltinMeaning'\".
 class (Bounded fun, Enum fun, Ix fun) => ToBuiltinMeaning uni fun where
     -- | The @cost@ part of 'BuiltinMeaning'.
     type CostingPart uni fun
 
-    -- | Get the 'BuiltinMeaning' of a built-in function.
     toBuiltinMeaning :: HasConstantIn uni val => fun -> BuiltinMeaning val (CostingPart uni fun)
 
 -- | Get the type of a built-in function.
@@ -116,6 +122,10 @@ function and the 'TypeScheme' of the built-in function will be derived automatic
 monomorphic and simply-polymorphic cases no types need to be specified at all.
 -}
 
+type family Length xs where
+    Length '[]       = 'Z
+    Length (_ ': xs) = 'S (Length xs)
+
 type family GetArgs a :: [GHC.Type] where
     GetArgs (a -> b) = a ': GetArgs b
     GetArgs _        = '[]
@@ -123,11 +133,17 @@ type family GetArgs a :: [GHC.Type] where
 -- | A class that allows us to derive a monotype for a builtin.
 class KnownMonotype val args res a | args res -> a, a -> res where
     knownMonotype :: TypeScheme val args res
+    knownMonoruntime :: RuntimeScheme (Length args)
+    toImmediateF :: FoldArgs args res -> ToDenotationType val (Length args)
+    toDeferredF :: ReadKnownM (FoldArgs args res) -> ToDenotationType val (Length args)
 
 -- | Once we've run out of term-level arguments, we return a 'TypeSchemeResult'.
 instance (res ~ res', KnownTypeAst (UniOf val) res, MakeKnown val res) =>
             KnownMonotype val '[] res res' where
     knownMonotype = TypeSchemeResult
+    knownMonoruntime = RuntimeSchemeResult
+    toImmediateF = makeKnown (Just ())
+    toDeferredF getRes = liftEither getRes >>= makeKnown (Just ())
 
 -- | Every term-level argument becomes as 'TypeSchemeArrow'.
 instance
@@ -135,14 +151,20 @@ instance
         , KnownMonotype val args res a
         ) => KnownMonotype val (arg ': args) res (arg -> a) where
     knownMonotype = TypeSchemeArrow knownMonotype
+    knownMonoruntime = RuntimeSchemeArrow $ knownMonoruntime @val @args @res
+    toImmediateF f val = toImmediateF @val @args @res . f <$> readKnown (Just ()) val
+    toDeferredF getF val = pure . toDeferredF @val @args @res $ getF <*> readKnown (Just ()) val
 
 -- | A class that allows us to derive a polytype for a builtin.
-class KnownPolytype (binds :: [Some TyNameRep]) val args res a | args res -> a, a -> res where
+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
+    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
+    knownPolyruntime = knownMonoruntime @val @args @res
 
 -- Here we unpack an existentially packed @kind@ and constrain it afterwards!
 -- So promoted existentials are true sigmas! If we were at the term level, we'd have to pack
@@ -152,6 +174,7 @@ instance KnownMonotype val args res a => KnownPolytype '[] val args res a where
 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
+    knownPolyruntime = RuntimeSchemeAll $ knownPolyruntime @binds @val @args @res
 
 -- See Note [Automatic derivation of type schemes]
 -- | Construct the meaning for a built-in function by automatically deriving its
@@ -164,5 +187,26 @@ makeBuiltinMeaning
        ( binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res
        , ElaborateFromTo 0 j val a, KnownPolytype binds val args res a
        )
-    => a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
-makeBuiltinMeaning = BuiltinMeaning $ knownPolytype @binds @val @args @res
+    => a -> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
+makeBuiltinMeaning f
+    = BuiltinMeaning (knownPolytype @binds @val @args @res) f
+    . BuiltinRuntimeOptions
+        (knownPolyruntime @binds @val @args @res)
+        (toImmediateF @val @args @res f)
+        (toDeferredF @val @args @res $ pure f)
+
+toBuiltinRuntime
+    :: UnliftingMode -> cost -> BuiltinMeaning val cost -> BuiltinRuntime val
+toBuiltinRuntime unlMode cost (BuiltinMeaning _ _ runtimeOpts) =
+    fromBuiltinRuntimeOptions unlMode cost runtimeOpts
+
+-- See Note [Inlining meanings of builtins].
+-- | Calculate runtime info for all built-in functions given denotations of builtins
+-- and a cost model.
+toBuiltinsRuntime
+    :: (cost ~ CostingPart uni fun, HasConstantIn uni val, ToBuiltinMeaning uni fun)
+    => cost -> BuiltinsRuntime fun val
+toBuiltinsRuntime cost =
+    BuiltinsRuntime . tabulateArray $
+        toBuiltinRuntime UnliftingDeferred cost . inline toBuiltinMeaning
+{-# INLINE toBuiltinsRuntime #-}
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index 5d45f6252b9..e259ecd8ca3 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -12,9 +12,6 @@ module PlutusCore.Builtin.Runtime where
 
 import PlutusPrelude
 
-import PlutusCore.Builtin.HasConstant
-import PlutusCore.Builtin.Meaning
-import PlutusCore.Builtin.TypeScheme
 import PlutusCore.Evaluation.Machine.Exception
 
 import Control.DeepSeq
@@ -22,7 +19,6 @@ import Control.Lens (ix, (^?))
 import Control.Monad.Except
 import Data.Array
 import Data.Kind qualified as GHC (Type)
-import GHC.Exts (inline)
 import PlutusCore.Builtin.KnownType
 
 import PlutusCore.Builtin.Emitter
@@ -79,6 +75,21 @@ data BuiltinRuntime val =
                                    -- to cost.
         (ToCostingType n)
 
+data BuiltinRuntimeOptions n val cost =
+    BuiltinRuntimeOptions
+        (RuntimeScheme n)
+        (ToDenotationType val n)
+        (ToDenotationType val n)
+        (cost -> ToCostingType n)
+
+fromBuiltinRuntimeOptions
+    :: UnliftingMode -> cost -> BuiltinRuntimeOptions n val cost -> BuiltinRuntime val
+fromBuiltinRuntimeOptions unlMode cost (BuiltinRuntimeOptions sch fImm fDef exF) =
+    BuiltinRuntime sch f $ exF cost where
+        f = case unlMode of
+                UnliftingImmediate -> fImm
+                UnliftingDeferred  -> fDef
+
 instance NFData (BuiltinRuntime val) where
     rnf (BuiltinRuntime rs f exF) = rnf rs `seq` f `seq` rwhnf exF
 
@@ -89,50 +100,12 @@ newtype BuiltinsRuntime fun val = BuiltinsRuntime
 
 deriving newtype instance (NFData fun) => NFData (BuiltinsRuntime fun val)
 
-data UnliftMode
-    = UnliftImmediately
-    | UnliftWhenSaturated
-
-unliftMode :: UnliftMode
-unliftMode = UnliftWhenSaturated
-
--- | Instantiate a 'BuiltinMeaning' given denotations of built-in functions and a cost model.
-toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
-toBuiltinRuntime cost (BuiltinMeaning sch f exF) =
-    go sch $ \sch' toF' toExF' -> BuiltinRuntime sch' (toF' $ pure f) (toExF' $ exF cost) where
-        go
-            :: TypeScheme val args res
-            -> (forall n.
-                    RuntimeScheme n
-                -> (ReadKnownM (FoldArgs args res) -> ToDenotationType val n)
-                -> (FoldArgsEx args -> ToCostingType n)
-                -> BuiltinRuntime val)
-            -> BuiltinRuntime val
-        go TypeSchemeResult       k =
-            k
-                RuntimeSchemeResult
-                (\getRes -> liftEither getRes >>= makeKnown (Just ()))
-                id
-        go (TypeSchemeArrow schB) k =
-            go schB $ \sch' toF' toExF' -> k
-                (RuntimeSchemeArrow sch')
-                (\getF x -> do
-                    let getVal = readKnown (Just ()) x
-                    case unliftMode of
-                        UnliftImmediately   -> getVal <&> \val -> toF' (($ val) <$> getF)
-                        UnliftWhenSaturated -> pure . toF' $ getF <*> getVal)
-                (toExF' .)
-        go (TypeSchemeAll _ schK) k = go schK $ k . RuntimeSchemeAll
-
--- See Note [Inlining meanings of builtins].
--- | Calculate runtime info for all built-in functions given denotations of builtins
--- and a cost model.
-toBuiltinsRuntime
-    :: (cost ~ CostingPart uni fun, HasConstantIn uni val, ToBuiltinMeaning uni fun)
-    => cost -> BuiltinsRuntime fun val
-toBuiltinsRuntime cost =
-    BuiltinsRuntime . tabulateArray $ toBuiltinRuntime cost . inline toBuiltinMeaning
-{-# INLINE toBuiltinsRuntime #-}
+data UnliftingMode
+    = UnliftingImmediate
+    | UnliftingDeferred
+
+unliftingMode :: UnliftingMode
+unliftingMode = UnliftingDeferred
 
 -- | Look up the runtime info of a built-in function during evaluation.
 lookupBuiltin
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/TypeScheme.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/TypeScheme.hs
index 62c5e920446..b9e7e56e0a0 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/TypeScheme.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/TypeScheme.hs
@@ -14,8 +14,6 @@
 module PlutusCore.Builtin.TypeScheme
     ( TypeScheme (..)
     , argProxy
-    , FoldArgs
-    , FoldArgsEx
     , typeSchemeToType
     ) where
 
@@ -23,8 +21,6 @@ import PlutusCore.Builtin.KnownKind
 import PlutusCore.Builtin.KnownType
 import PlutusCore.Builtin.KnownTypeAst
 import PlutusCore.Core
-import PlutusCore.Evaluation.Machine.ExBudget
-import PlutusCore.Evaluation.Machine.ExMemory
 import PlutusCore.Name
 
 import Data.Kind qualified as GHC (Type)
@@ -75,21 +71,6 @@ data TypeScheme val (args :: [GHC.Type]) res where
 argProxy :: TypeScheme val (arg ': args) res -> Proxy arg
 argProxy _ = Proxy
 
--- | Turn a list of Haskell types @args@ into a functional type ending in @res@.
---
--- >>> :set -XDataKinds
--- >>> :kind! FoldArgs [Text, Bool] Integer
--- FoldArgs [Text, Bool] Integer :: *
--- = Text -> Bool -> Integer
-type family FoldArgs args res where
-    FoldArgs '[]           res = res
-    FoldArgs (arg ': args) res = arg -> FoldArgs args res
-
--- | Calculates the parameters of the costing function for a builtin.
-type family FoldArgsEx args where
-    FoldArgsEx '[]           = ExBudget
-    FoldArgsEx (arg ': args) = ExMemory -> FoldArgsEx args
-
 -- | 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) ()

From 5d3fb5abe5ff34ee07d2560c91ae994f3b24d8c9 Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Wed, 30 Mar 2022 16:37:08 +0300
Subject: [PATCH 09/17] Drop immediate unlifting

---
 .../.plan.nix/plutus-core.nix                 |  1 +
 .../.plan.nix/plutus-core.nix                 |  1 +
 .../.plan.nix/plutus-core.nix                 |  1 +
 plutus-core/plutus-core.cabal                 |  1 +
 .../examples/PlutusCore/Examples/Builtins.hs  |  8 +++----
 .../src/PlutusCore/Builtin/Meaning.hs         | 20 ++++++++---------
 .../src/PlutusCore/Builtin/Runtime.hs         | 22 +++++--------------
 .../src/PlutusCore/Evaluation/Machine/Ck.hs   | 14 +++++-------
 .../Evaluation/Machine/Cek/Debug.hs           | 17 ++++++++++++++
 .../Evaluation/Machine/Cek/Internal.hs        | 16 ++++++--------
 10 files changed, 53 insertions(+), 48 deletions(-)
 create mode 100644 plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Debug.hs

diff --git a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix
index 0cf968f2475..38c767c1bdd 100644
--- a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix
+++ b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix
@@ -277,6 +277,7 @@
           "UntypedPlutusCore/DeBruijn"
           "UntypedPlutusCore/Evaluation/Machine/Cek"
           "UntypedPlutusCore/Evaluation/Machine/Cek/Internal"
+          "UntypedPlutusCore/Evaluation/Machine/Cek/Debug"
           "UntypedPlutusCore/Parser"
           "UntypedPlutusCore/Rename"
           "UntypedPlutusCore/MkUPlc"
diff --git a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix
index 0cf968f2475..38c767c1bdd 100644
--- a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix
+++ b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix
@@ -277,6 +277,7 @@
           "UntypedPlutusCore/DeBruijn"
           "UntypedPlutusCore/Evaluation/Machine/Cek"
           "UntypedPlutusCore/Evaluation/Machine/Cek/Internal"
+          "UntypedPlutusCore/Evaluation/Machine/Cek/Debug"
           "UntypedPlutusCore/Parser"
           "UntypedPlutusCore/Rename"
           "UntypedPlutusCore/MkUPlc"
diff --git a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix
index 0cf968f2475..38c767c1bdd 100644
--- a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix
+++ b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix
@@ -277,6 +277,7 @@
           "UntypedPlutusCore/DeBruijn"
           "UntypedPlutusCore/Evaluation/Machine/Cek"
           "UntypedPlutusCore/Evaluation/Machine/Cek/Internal"
+          "UntypedPlutusCore/Evaluation/Machine/Cek/Debug"
           "UntypedPlutusCore/Parser"
           "UntypedPlutusCore/Rename"
           "UntypedPlutusCore/MkUPlc"
diff --git a/plutus-core/plutus-core.cabal b/plutus-core/plutus-core.cabal
index 4adcd98c6ff..909c846ee47 100644
--- a/plutus-core/plutus-core.cabal
+++ b/plutus-core/plutus-core.cabal
@@ -140,6 +140,7 @@ library
         UntypedPlutusCore.DeBruijn
         UntypedPlutusCore.Evaluation.Machine.Cek
         UntypedPlutusCore.Evaluation.Machine.Cek.Internal
+        UntypedPlutusCore.Evaluation.Machine.Cek.Debug
         UntypedPlutusCore.Parser
         UntypedPlutusCore.Rename
         UntypedPlutusCore.MkUPlc
diff --git a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
index aa469ac487c..df49442208b 100644
--- a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
+++ b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
@@ -129,11 +129,11 @@ instance (ToBuiltinMeaning uni fun1, ToBuiltinMeaning uni fun2) =>
     type CostingPart uni (Either fun1 fun2) = (CostingPart uni fun1, CostingPart uni fun2)
 
     toBuiltinMeaning (Left  fun) = case toBuiltinMeaning fun of
-        BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch fImm fDef toExF) ->
-            BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch fImm fDef (toExF . fst))
+        BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch f toExF) ->
+            BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch f (toExF . fst))
     toBuiltinMeaning (Right fun) = case toBuiltinMeaning fun of
-        BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch fImm fDef toExF) ->
-            BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch fImm fDef (toExF . snd))
+        BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch f toExF) ->
+            BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch f (toExF . snd))
 
 defBuiltinsRuntimeExt
     :: HasConstantIn DefaultUni term
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
index 045baf2cfff..7adc7fcbea5 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
@@ -134,7 +134,6 @@ type family GetArgs a :: [GHC.Type] where
 class KnownMonotype val args res a | args res -> a, a -> res where
     knownMonotype :: TypeScheme val args res
     knownMonoruntime :: RuntimeScheme (Length args)
-    toImmediateF :: FoldArgs args res -> ToDenotationType val (Length args)
     toDeferredF :: ReadKnownM (FoldArgs args res) -> ToDenotationType val (Length args)
 
 -- | Once we've run out of term-level arguments, we return a 'TypeSchemeResult'.
@@ -142,8 +141,8 @@ instance (res ~ res', KnownTypeAst (UniOf val) res, MakeKnown val res) =>
             KnownMonotype val '[] res res' where
     knownMonotype = TypeSchemeResult
     knownMonoruntime = RuntimeSchemeResult
-    toImmediateF = makeKnown (Just ())
     toDeferredF getRes = liftEither getRes >>= makeKnown (Just ())
+    {-# INLINE toDeferredF #-}
 
 -- | Every term-level argument becomes as 'TypeSchemeArrow'.
 instance
@@ -152,8 +151,8 @@ instance
         ) => KnownMonotype val (arg ': args) res (arg -> a) where
     knownMonotype = TypeSchemeArrow knownMonotype
     knownMonoruntime = RuntimeSchemeArrow $ knownMonoruntime @val @args @res
-    toImmediateF f val = toImmediateF @val @args @res . f <$> readKnown (Just ()) val
-    toDeferredF getF val = pure . toDeferredF @val @args @res $ getF <*> readKnown (Just ()) val
+    toDeferredF getF = \arg -> toDeferredF @val @args @res $! getF <*> readKnown (Just ()) arg
+    {-# INLINE toDeferredF #-}
 
 -- | A class that allows us to derive a polytype for a builtin.
 class KnownMonotype val args res a =>
@@ -192,13 +191,13 @@ makeBuiltinMeaning f
     = BuiltinMeaning (knownPolytype @binds @val @args @res) f
     . BuiltinRuntimeOptions
         (knownPolyruntime @binds @val @args @res)
-        (toImmediateF @val @args @res f)
         (toDeferredF @val @args @res $ pure f)
+{-# INLINE makeBuiltinMeaning #-}
 
-toBuiltinRuntime
-    :: UnliftingMode -> cost -> BuiltinMeaning val cost -> BuiltinRuntime val
-toBuiltinRuntime unlMode cost (BuiltinMeaning _ _ runtimeOpts) =
-    fromBuiltinRuntimeOptions unlMode cost runtimeOpts
+toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
+toBuiltinRuntime cost (BuiltinMeaning _ _ runtimeOpts) =
+    fromBuiltinRuntimeOptions cost runtimeOpts
+{-# INLINE toBuiltinRuntime #-}
 
 -- See Note [Inlining meanings of builtins].
 -- | Calculate runtime info for all built-in functions given denotations of builtins
@@ -207,6 +206,5 @@ toBuiltinsRuntime
     :: (cost ~ CostingPart uni fun, HasConstantIn uni val, ToBuiltinMeaning uni fun)
     => cost -> BuiltinsRuntime fun val
 toBuiltinsRuntime cost =
-    BuiltinsRuntime . tabulateArray $
-        toBuiltinRuntime UnliftingDeferred cost . inline toBuiltinMeaning
+    BuiltinsRuntime . tabulateArray $ toBuiltinRuntime cost . inline toBuiltinMeaning
 {-# INLINE toBuiltinsRuntime #-}
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index e259ecd8ca3..0d8f479a134 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -38,7 +38,7 @@ type ReadKnownM = Either (ErrorWithCause ReadKnownError ())
 
 type family ToDenotationType val (n :: Nat) :: GHC.Type where
     ToDenotationType val 'Z     = MakeKnownM val
-    ToDenotationType val ('S n) = val -> ReadKnownM (ToDenotationType val n)
+    ToDenotationType val ('S n) = val -> ToDenotationType val n
 
 type family ToCostingType (n :: Nat) :: GHC.Type where
     ToCostingType 'Z     = ExBudget
@@ -78,17 +78,14 @@ data BuiltinRuntime val =
 data BuiltinRuntimeOptions n val cost =
     BuiltinRuntimeOptions
         (RuntimeScheme n)
-        (ToDenotationType val n)
-        (ToDenotationType val n)
-        (cost -> ToCostingType n)
+        ~(ToDenotationType val n)
+        ~(cost -> ToCostingType n)
 
 fromBuiltinRuntimeOptions
-    :: UnliftingMode -> cost -> BuiltinRuntimeOptions n val cost -> BuiltinRuntime val
-fromBuiltinRuntimeOptions unlMode cost (BuiltinRuntimeOptions sch fImm fDef exF) =
+    :: cost -> BuiltinRuntimeOptions n val cost -> BuiltinRuntime val
+fromBuiltinRuntimeOptions cost (BuiltinRuntimeOptions sch f exF) =
     BuiltinRuntime sch f $ exF cost where
-        f = case unlMode of
-                UnliftingImmediate -> fImm
-                UnliftingDeferred  -> fDef
+{-# INLINE fromBuiltinRuntimeOptions #-}
 
 instance NFData (BuiltinRuntime val) where
     rnf (BuiltinRuntime rs f exF) = rnf rs `seq` f `seq` rwhnf exF
@@ -100,13 +97,6 @@ newtype BuiltinsRuntime fun val = BuiltinsRuntime
 
 deriving newtype instance (NFData fun) => NFData (BuiltinsRuntime fun val)
 
-data UnliftingMode
-    = UnliftingImmediate
-    | UnliftingDeferred
-
-unliftingMode :: UnliftingMode
-unliftingMode = UnliftingDeferred
-
 -- | Look up the runtime info of a built-in function during evaluation.
 lookupBuiltin
     :: (MonadError (ErrorWithCause err cause) m, AsMachineError err fun, Ix fun)
diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
index 1052c892b5c..8c02624f36b 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
@@ -306,14 +306,12 @@ applyEvaluate stack (VBuiltin term (BuiltinRuntime sch f exF)) arg = do
     case sch of
         -- It's only possible to apply a builtin application if the builtin expects a term
         -- argument next.
-        RuntimeSchemeArrow schB -> case f arg of
-            Left err  -> throwReadKnownErrorWithCause $ argTerm <$ err
-            Right y  -> do
-                -- The CK machine does not support costing, so we just apply the costing function
-                -- to 'mempty'.
-                let runtime' = BuiltinRuntime schB y (exF mempty)
-                res <- evalBuiltinApp term' runtime'
-                stack <| res
+        RuntimeSchemeArrow schB -> do
+            -- The CK machine does not support costing, so we just apply the costing function
+            -- to 'mempty'.
+            let runtime' = BuiltinRuntime schB (f arg) (exF mempty)
+            res <- evalBuiltinApp term' runtime'
+            stack <| res
         _ ->
             throwingWithCause _MachineError UnexpectedBuiltinTermArgumentMachineError (Just term')
 applyEvaluate _ val _ =
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Debug.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Debug.hs
new file mode 100644
index 00000000000..0eaef974fbb
--- /dev/null
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Debug.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies #-}
+
+{-# OPTIONS_GHC -ddump-simpl -ddump-to-file -dsuppress-all -fforce-recomp -dumpdir /tmp/dumps #-}
+
+module UntypedPlutusCore.Evaluation.Machine.Cek.Debug where
+
+import UntypedPlutusCore.Evaluation.Machine.Cek.Internal
+
+import PlutusCore.Builtin
+import PlutusCore.Default
+
+import GHC.Exts (inline)
+
+toBuiltinsRuntimeDef
+    :: (cost ~ CostingPart uni fun, uni ~ DefaultUni, fun ~ DefaultFun)
+    => cost -> BuiltinsRuntime fun (CekValue uni fun)
+toBuiltinsRuntimeDef = inline toBuiltinsRuntime
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
index fabca39874c..44658aa8638 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
@@ -709,15 +709,13 @@ enterComputeCek = computeCek (toWordArray 0) where
         case sch of
             -- It's only possible to apply a builtin application if the builtin expects a term
             -- argument next.
-            RuntimeSchemeArrow schB -> case f arg of
-                Left err  -> throwReadKnownErrorWithCause $ argTerm <$ err
-                Right app -> do
-                    -- TODO: should we bother computing that 'ExMemory' eagerly? We may not need it.
-                    -- We pattern match on @arg@ twice: in 'readKnown' and in 'toExMemory'.
-                    -- Maybe we could fuse the two?
-                    let runtime' = BuiltinRuntime schB app . exF $ toExMemory arg
-                    res <- evalBuiltinApp fun term' env runtime'
-                    returnCek unbudgetedSteps ctx res
+            RuntimeSchemeArrow schB -> do
+                -- TODO: should we bother computing that 'ExMemory' eagerly? We may not need it.
+                -- We pattern match on @arg@ twice: in 'readKnown' and in 'toExMemory'.
+                -- Maybe we could fuse the two?
+                let runtime' = BuiltinRuntime schB (f arg) . exF $ toExMemory arg
+                res <- evalBuiltinApp fun term' env runtime'
+                returnCek unbudgetedSteps ctx res
             _ ->
                 throwingWithCause _MachineError UnexpectedBuiltinTermArgumentMachineError (Just term')
     applyEvaluate !_ !_ val _ =

From 718499af0f6a08b94aebf0eb768e087d040d1fd5 Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Wed, 30 Mar 2022 20:28:27 +0300
Subject: [PATCH 10/17] Drop redundant laziness annotations

---
 plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index 0d8f479a134..4166c760d39 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -78,8 +78,8 @@ data BuiltinRuntime val =
 data BuiltinRuntimeOptions n val cost =
     BuiltinRuntimeOptions
         (RuntimeScheme n)
-        ~(ToDenotationType val n)
-        ~(cost -> ToCostingType n)
+        (ToDenotationType val n)
+        (cost -> ToCostingType n)
 
 fromBuiltinRuntimeOptions
     :: cost -> BuiltinRuntimeOptions n val cost -> BuiltinRuntime val

From f0709790221c290cc2db3c20d0d19242d9b629cc Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Fri, 1 Apr 2022 18:45:28 +0200
Subject: [PATCH 11/17] Integrate immediate unlifting

---
 .../budgeting-bench/Benchmarks/Nops.hs        |  4 +++-
 .../examples/PlutusCore/Examples/Builtins.hs  | 10 ++++-----
 plutus-core/plutus-core/src/PlutusCore.hs     |  3 +++
 .../src/PlutusCore/Builtin/Meaning.hs         | 19 ++++++++++------
 .../src/PlutusCore/Builtin/Runtime.hs         | 14 +++++++++---
 .../src/PlutusCore/Evaluation/Machine/Ck.hs   | 14 +++++++-----
 .../Evaluation/Machine/ExBudgetingDefaults.hs | 12 +++++++---
 .../Evaluation/Machine/MachineParameters.hs   |  7 +++---
 .../Evaluation/Machine/Cek/Debug.hs           |  2 +-
 .../Evaluation/Machine/Cek/Internal.hs        | 16 ++++++++------
 .../src/Plutus/V1/Ledger/EvaluationContext.hs | 22 ++++++++++++++-----
 11 files changed, 81 insertions(+), 42 deletions(-)

diff --git a/plutus-core/cost-model/budgeting-bench/Benchmarks/Nops.hs b/plutus-core/cost-model/budgeting-bench/Benchmarks/Nops.hs
index 628f67b5c32..8b35f6963e2 100644
--- a/plutus-core/cost-model/budgeting-bench/Benchmarks/Nops.hs
+++ b/plutus-core/cost-model/budgeting-bench/Benchmarks/Nops.hs
@@ -124,7 +124,9 @@ nopCostModel =
     }
 
 nopCostParameters :: MachineParameters CekMachineCosts CekValue DefaultUni NopFun
-nopCostParameters = mkMachineParameters $ CostModel defaultCekMachineCosts nopCostModel
+nopCostParameters =
+    mkMachineParameters defaultUnliftingMode $
+        CostModel defaultCekMachineCosts nopCostModel
 
 -- This is just to avoid some deeply nested case expressions for the NopNc
 -- functions below.  There is a Monad instance for EvaluationResult, but that
diff --git a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
index df49442208b..cf164b3b4de 100644
--- a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
+++ b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
@@ -129,16 +129,16 @@ instance (ToBuiltinMeaning uni fun1, ToBuiltinMeaning uni fun2) =>
     type CostingPart uni (Either fun1 fun2) = (CostingPart uni fun1, CostingPart uni fun2)
 
     toBuiltinMeaning (Left  fun) = case toBuiltinMeaning fun of
-        BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch f toExF) ->
-            BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch f (toExF . fst))
+        BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch immF defF toExF) ->
+            BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch immF defF (toExF . fst))
     toBuiltinMeaning (Right fun) = case toBuiltinMeaning fun of
-        BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch f toExF) ->
-            BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch f (toExF . snd))
+        BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch immF defF toExF) ->
+            BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch immF defF (toExF . snd))
 
 defBuiltinsRuntimeExt
     :: HasConstantIn DefaultUni term
     => BuiltinsRuntime (Either DefaultFun ExtensionFun) term
-defBuiltinsRuntimeExt = toBuiltinsRuntime (defaultBuiltinCostModel, ())
+defBuiltinsRuntimeExt = toBuiltinsRuntime UnliftingImmediate (defaultBuiltinCostModel, ())
 
 data PlcListRep (a :: GHC.Type)
 instance KnownTypeAst uni a => KnownTypeAst uni (PlcListRep a) where
diff --git a/plutus-core/plutus-core/src/PlutusCore.hs b/plutus-core/plutus-core/src/PlutusCore.hs
index 84c6ea02b48..a81ce299bd2 100644
--- a/plutus-core/plutus-core/src/PlutusCore.hs
+++ b/plutus-core/plutus-core/src/PlutusCore.hs
@@ -117,6 +117,7 @@ module PlutusCore
     , freshTyName
     -- * Evaluation
     , EvaluationResult (..)
+    , UnliftingMode (..)
     -- * Combining programs
     , applyProgram
     -- * Benchmarking
@@ -132,6 +133,7 @@ module PlutusCore
     , defaultCekMachineCosts
     , defaultCekParameters
     , defaultCostModelParams
+    , defaultUnliftingMode
     , unitCekParameters
     -- * CEK machine costs
     , cekMachineCostsPrefix
@@ -140,6 +142,7 @@ module PlutusCore
 
 import PlutusPrelude
 
+import PlutusCore.Builtin
 import PlutusCore.Check.Uniques qualified as Uniques
 import PlutusCore.Core
 import PlutusCore.DeBruijn
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
index 7adc7fcbea5..28491b4100e 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
@@ -134,6 +134,7 @@ type family GetArgs a :: [GHC.Type] where
 class KnownMonotype val args res a | args res -> a, a -> res where
     knownMonotype :: TypeScheme val args res
     knownMonoruntime :: RuntimeScheme (Length args)
+    toImmediateF :: FoldArgs args res -> ToDenotationType val (Length args)
     toDeferredF :: ReadKnownM (FoldArgs args res) -> ToDenotationType val (Length args)
 
 -- | Once we've run out of term-level arguments, we return a 'TypeSchemeResult'.
@@ -141,6 +142,7 @@ instance (res ~ res', KnownTypeAst (UniOf val) res, MakeKnown val res) =>
             KnownMonotype val '[] res res' where
     knownMonotype = TypeSchemeResult
     knownMonoruntime = RuntimeSchemeResult
+    toImmediateF = makeKnown (Just ())
     toDeferredF getRes = liftEither getRes >>= makeKnown (Just ())
     {-# INLINE toDeferredF #-}
 
@@ -151,7 +153,9 @@ instance
         ) => KnownMonotype val (arg ': args) res (arg -> a) where
     knownMonotype = TypeSchemeArrow knownMonotype
     knownMonoruntime = RuntimeSchemeArrow $ knownMonoruntime @val @args @res
-    toDeferredF getF = \arg -> toDeferredF @val @args @res $! getF <*> readKnown (Just ()) arg
+    toImmediateF f = fmap (toImmediateF @val @args @res . f) . readKnown (Just ())
+    toDeferredF getF = \arg ->
+        pure . toDeferredF @val @args @res $! getF <*> readKnown (Just ()) arg
     {-# INLINE toDeferredF #-}
 
 -- | A class that allows us to derive a polytype for a builtin.
@@ -191,12 +195,13 @@ makeBuiltinMeaning f
     = BuiltinMeaning (knownPolytype @binds @val @args @res) f
     . BuiltinRuntimeOptions
         (knownPolyruntime @binds @val @args @res)
+        (toImmediateF @val @args @res f)
         (toDeferredF @val @args @res $ pure f)
 {-# INLINE makeBuiltinMeaning #-}
 
-toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
-toBuiltinRuntime cost (BuiltinMeaning _ _ runtimeOpts) =
-    fromBuiltinRuntimeOptions cost runtimeOpts
+toBuiltinRuntime :: UnliftingMode -> cost -> BuiltinMeaning val cost -> BuiltinRuntime val
+toBuiltinRuntime unlMode cost (BuiltinMeaning _ _ runtimeOpts) =
+    fromBuiltinRuntimeOptions unlMode cost runtimeOpts
 {-# INLINE toBuiltinRuntime #-}
 
 -- See Note [Inlining meanings of builtins].
@@ -204,7 +209,7 @@ toBuiltinRuntime cost (BuiltinMeaning _ _ runtimeOpts) =
 -- and a cost model.
 toBuiltinsRuntime
     :: (cost ~ CostingPart uni fun, HasConstantIn uni val, ToBuiltinMeaning uni fun)
-    => cost -> BuiltinsRuntime fun val
-toBuiltinsRuntime cost =
-    BuiltinsRuntime . tabulateArray $ toBuiltinRuntime cost . inline toBuiltinMeaning
+    => UnliftingMode -> cost -> BuiltinsRuntime fun val
+toBuiltinsRuntime unlMode cost =
+    BuiltinsRuntime . tabulateArray $ toBuiltinRuntime unlMode cost . inline toBuiltinMeaning
 {-# INLINE toBuiltinsRuntime #-}
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index 4166c760d39..f5912f01cf9 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -38,7 +38,7 @@ type ReadKnownM = Either (ErrorWithCause ReadKnownError ())
 
 type family ToDenotationType val (n :: Nat) :: GHC.Type where
     ToDenotationType val 'Z     = MakeKnownM val
-    ToDenotationType val ('S n) = val -> ToDenotationType val n
+    ToDenotationType val ('S n) = val -> ReadKnownM (ToDenotationType val n)
 
 type family ToCostingType (n :: Nat) :: GHC.Type where
     ToCostingType 'Z     = ExBudget
@@ -79,12 +79,20 @@ data BuiltinRuntimeOptions n val cost =
     BuiltinRuntimeOptions
         (RuntimeScheme n)
         (ToDenotationType val n)
+        (ToDenotationType val n)
         (cost -> ToCostingType n)
 
+data UnliftingMode
+    = UnliftingImmediate
+    | UnliftingDeferred
+
 fromBuiltinRuntimeOptions
-    :: cost -> BuiltinRuntimeOptions n val cost -> BuiltinRuntime val
-fromBuiltinRuntimeOptions cost (BuiltinRuntimeOptions sch f exF) =
+    :: UnliftingMode -> cost -> BuiltinRuntimeOptions n val cost -> BuiltinRuntime val
+fromBuiltinRuntimeOptions unlMode cost (BuiltinRuntimeOptions sch immF defF exF) =
     BuiltinRuntime sch f $ exF cost where
+        f = case unlMode of
+                UnliftingImmediate -> immF
+                UnliftingDeferred  -> defF
 {-# INLINE fromBuiltinRuntimeOptions #-}
 
 instance NFData (BuiltinRuntime val) where
diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
index 8c02624f36b..c5348e864bb 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
@@ -306,12 +306,14 @@ applyEvaluate stack (VBuiltin term (BuiltinRuntime sch f exF)) arg = do
     case sch of
         -- It's only possible to apply a builtin application if the builtin expects a term
         -- argument next.
-        RuntimeSchemeArrow schB -> do
-            -- The CK machine does not support costing, so we just apply the costing function
-            -- to 'mempty'.
-            let runtime' = BuiltinRuntime schB (f arg) (exF mempty)
-            res <- evalBuiltinApp term' runtime'
-            stack <| res
+        RuntimeSchemeArrow schB -> case f arg of
+            Left err -> throwReadKnownErrorWithCause $ argTerm <$ err
+            Right y  -> do
+                -- The CK machine does not support costing, so we just apply the costing function
+                -- to 'mempty'.
+                let runtime' = BuiltinRuntime schB y (exF mempty)
+                res <- evalBuiltinApp term' runtime'
+                stack <| res
         _ ->
             throwingWithCause _MachineError UnexpectedBuiltinTermArgumentMachineError (Just term')
 applyEvaluate _ val _ =
diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs
index a584cd3b5d4..379402e6f1b 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs
@@ -8,6 +8,7 @@ module PlutusCore.Evaluation.Machine.ExBudgetingDefaults
     , defaultCekMachineCosts
     , defaultCekParameters
     , defaultCostModelParams
+    , defaultUnliftingMode
     , defaultBuiltinCostModel
     , unitCekMachineCosts
     , unitCekParameters
@@ -74,14 +75,19 @@ defaultCekCostModel = CostModel defaultCekMachineCosts defaultBuiltinCostModel
 defaultCostModelParams :: Maybe CostModelParams
 defaultCostModelParams = extractCostModelParams defaultCekCostModel
 
+defaultUnliftingMode :: UnliftingMode
+defaultUnliftingMode = UnliftingImmediate
+
 defaultCekParameters :: MachineParameters CekMachineCosts CekValue DefaultUni DefaultFun
-defaultCekParameters = mkMachineParameters defaultCekCostModel
+defaultCekParameters = mkMachineParameters defaultUnliftingMode defaultCekCostModel
 
 unitCekParameters :: MachineParameters CekMachineCosts CekValue DefaultUni DefaultFun
-unitCekParameters = mkMachineParameters (CostModel unitCekMachineCosts unitCostBuiltinCostModel)
+unitCekParameters =
+    mkMachineParameters defaultUnliftingMode $
+        CostModel unitCekMachineCosts unitCostBuiltinCostModel
 
 defaultBuiltinsRuntime :: HasConstantIn DefaultUni term => BuiltinsRuntime DefaultFun term
-defaultBuiltinsRuntime = toBuiltinsRuntime defaultBuiltinCostModel
+defaultBuiltinsRuntime = toBuiltinsRuntime UnliftingImmediate defaultBuiltinCostModel
 
 
 -- A cost model with unit costs, so we can count how often each builtin is called
diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/MachineParameters.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/MachineParameters.hs
index 2cd619c076b..e262bff57af 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/MachineParameters.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/MachineParameters.hs
@@ -51,8 +51,9 @@ mkMachineParameters ::
     , HasConstantIn uni (val uni fun)
     , ToBuiltinMeaning uni fun
     )
-    => CostModel machinecosts builtincosts
+    => UnliftingMode
+    -> CostModel machinecosts builtincosts
     -> MachineParameters machinecosts val uni fun
-mkMachineParameters (CostModel mchnCosts builtinCosts) =
-    MachineParameters mchnCosts (inline toBuiltinsRuntime builtinCosts)
+mkMachineParameters unlMode (CostModel mchnCosts builtinCosts) =
+    MachineParameters mchnCosts (inline toBuiltinsRuntime unlMode builtinCosts)
 {-# INLINE mkMachineParameters #-}
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Debug.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Debug.hs
index 0eaef974fbb..49d75cbe21f 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Debug.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Debug.hs
@@ -14,4 +14,4 @@ import GHC.Exts (inline)
 toBuiltinsRuntimeDef
     :: (cost ~ CostingPart uni fun, uni ~ DefaultUni, fun ~ DefaultFun)
     => cost -> BuiltinsRuntime fun (CekValue uni fun)
-toBuiltinsRuntimeDef = inline toBuiltinsRuntime
+toBuiltinsRuntimeDef = inline toBuiltinsRuntime UnliftingImmediate
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
index 44658aa8638..11f47c5a3f0 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
@@ -709,13 +709,15 @@ enterComputeCek = computeCek (toWordArray 0) where
         case sch of
             -- It's only possible to apply a builtin application if the builtin expects a term
             -- argument next.
-            RuntimeSchemeArrow schB -> do
-                -- TODO: should we bother computing that 'ExMemory' eagerly? We may not need it.
-                -- We pattern match on @arg@ twice: in 'readKnown' and in 'toExMemory'.
-                -- Maybe we could fuse the two?
-                let runtime' = BuiltinRuntime schB (f arg) . exF $ toExMemory arg
-                res <- evalBuiltinApp fun term' env runtime'
-                returnCek unbudgetedSteps ctx res
+            RuntimeSchemeArrow schB -> case f arg of
+                Left err -> throwReadKnownErrorWithCause $ argTerm <$ err
+                Right y  -> do
+                    -- TODO: should we bother computing that 'ExMemory' eagerly? We may not need it.
+                    -- We pattern match on @arg@ twice: in 'readKnown' and in 'toExMemory'.
+                    -- Maybe we could fuse the two?
+                    let runtime' = BuiltinRuntime schB y . exF $ toExMemory arg
+                    res <- evalBuiltinApp fun term' env runtime'
+                    returnCek unbudgetedSteps ctx res
             _ ->
                 throwingWithCause _MachineError UnexpectedBuiltinTermArgumentMachineError (Just term')
     applyEvaluate !_ !_ val _ =
diff --git a/plutus-ledger-api/src/Plutus/V1/Ledger/EvaluationContext.hs b/plutus-ledger-api/src/Plutus/V1/Ledger/EvaluationContext.hs
index 5cdf16c2d9f..ba0b19a77fa 100644
--- a/plutus-ledger-api/src/Plutus/V1/Ledger/EvaluationContext.hs
+++ b/plutus-ledger-api/src/Plutus/V1/Ledger/EvaluationContext.hs
@@ -9,7 +9,8 @@ module Plutus.V1.Ledger.EvaluationContext
     , evalCtxForTesting
     ) where
 
-import PlutusCore as Plutus (DefaultFun, DefaultUni, defaultCekCostModel, defaultCostModelParams)
+import PlutusCore as Plutus (DefaultFun, DefaultUni, UnliftingMode (..), defaultCekCostModel, defaultCostModelParams,
+                             defaultUnliftingMode)
 import PlutusCore.Evaluation.Machine.CostModelInterface as Plutus
 import PlutusCore.Evaluation.Machine.MachineParameters as Plutus
 import UntypedPlutusCore.Evaluation.Machine.Cek as Plutus
@@ -53,10 +54,19 @@ inlining).
 -- | Build the 'EvaluationContext'.
 --
 -- The input is a `Map` of strings to cost integer values (aka `Plutus.CostModelParams`, `Alonzo.CostModel`)
-mkEvaluationContext :: Plutus.CostModelParams
-                    -> Maybe EvaluationContext
-mkEvaluationContext newCMP =
-    EvaluationContext . inline Plutus.mkMachineParameters <$> Plutus.applyCostModelParams Plutus.defaultCekCostModel newCMP
+mkEvaluationContextUnliftingImmediate :: Plutus.CostModelParams -> Maybe EvaluationContext
+mkEvaluationContextUnliftingImmediate newCMP =
+    EvaluationContext . inline Plutus.mkMachineParameters UnliftingImmediate <$>
+        Plutus.applyCostModelParams Plutus.defaultCekCostModel newCMP
+
+mkEvaluationContextUnliftingDeferred :: Plutus.CostModelParams -> Maybe EvaluationContext
+mkEvaluationContextUnliftingDeferred newCMP =
+    EvaluationContext . inline Plutus.mkMachineParameters UnliftingImmediate <$>
+        Plutus.applyCostModelParams Plutus.defaultCekCostModel newCMP
+
+mkEvaluationContext :: UnliftingMode -> Plutus.CostModelParams -> Maybe EvaluationContext
+mkEvaluationContext UnliftingImmediate = mkEvaluationContextUnliftingImmediate
+mkEvaluationContext UnliftingDeferred  = mkEvaluationContextUnliftingDeferred
 
 -- | Comparably expensive to `mkEvaluationContext`, so it should only be used sparingly.
 isCostModelParamsWellFormed :: Plutus.CostModelParams -> Bool
@@ -73,4 +83,4 @@ costModelParamsForTesting = fromJust Plutus.defaultCostModelParams
 
 -- | only to be for testing purposes: make an evaluation context by applying an empty set of protocol parameters
 evalCtxForTesting :: EvaluationContext
-evalCtxForTesting = fromJust $ mkEvaluationContext mempty
+evalCtxForTesting = fromJust $ mkEvaluationContext defaultUnliftingMode mempty

From ba403c3fcb7457ff91706f2e3685d8ccf3a93a48 Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Fri, 1 Apr 2022 22:36:56 +0200
Subject: [PATCH 12/17] Fix tests

---
 .../test/Evaluation/Builtins/Definition.hs                | 3 ++-
 .../Golden/iteAtIntegerWrongCondType.plc.golden           | 8 ++++----
 .../Golden/iteAtIntegerWrongCondType.uplc.golden          | 8 ++++----
 .../untyped-plutus-core/test/Evaluation/Machines.hs       | 2 +-
 4 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Definition.hs b/plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Definition.hs
index 7541c13c972..06a07423a79 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Definition.hs
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Definition.hs
@@ -48,7 +48,8 @@ import Test.Tasty.Hedgehog
 defaultCekParametersExt
     :: MachineParameters CekMachineCosts CekValue DefaultUni (Either DefaultFun ExtensionFun)
 defaultCekParametersExt =
-    mkMachineParameters $ CostModel defaultCekMachineCosts (defaultBuiltinCostModel, ())
+    mkMachineParameters defaultUnliftingMode $
+        CostModel defaultCekMachineCosts (defaultBuiltinCostModel, ())
 
 -- | Check that 'Factorial' from the above computes to the same thing as
 -- a factorial defined in PLC itself.
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
index 17e15ddf9b2..9b591585958 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
@@ -1,4 +1,4 @@
-(Right [
-  [ (force (builtin ifThenElse)) (con string "11 <= 22") ]
-  (con string "\172(11 <= 22)")
-])
\ No newline at end of file
+(Left An error has occurred:  error:
+Could not unlift a builtin:
+Type mismatch: expected: bool; actual: string
+Caused by: (con string "11 <= 22"))
\ No newline at end of file
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
index 17e15ddf9b2..9b591585958 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
@@ -1,4 +1,4 @@
-(Right [
-  [ (force (builtin ifThenElse)) (con string "11 <= 22") ]
-  (con string "\172(11 <= 22)")
-])
\ No newline at end of file
+(Left An error has occurred:  error:
+Could not unlift a builtin:
+Type mismatch: expected: bool; actual: string
+Caused by: (con string "11 <= 22"))
\ No newline at end of file
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Machines.hs b/plutus-core/untyped-plutus-core/test/Evaluation/Machines.hs
index 1fb5a1b4bdc..d0d83a684c7 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Machines.hs
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Machines.hs
@@ -113,7 +113,7 @@ test_budget
     . testNested "Budget"
     $ concat
         [ folder Plc.defaultBuiltinsRuntime bunchOfFibs
-        , folder (toBuiltinsRuntime ()) bunchOfIdNats
+        , folder (toBuiltinsRuntime Plc.defaultUnliftingMode ()) bunchOfIdNats
         , folder Plc.defaultBuiltinsRuntime bunchOfIfThenElseNats
         ]
   where

From 50d93e7a60149c7e6f51307e6470fb691a348003 Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Fri, 1 Apr 2022 22:47:19 +0200
Subject: [PATCH 13/17] And now with deferred unlifting

---
 .../src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs    | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs
index 379402e6f1b..558ebaebaa2 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs
@@ -76,7 +76,7 @@ defaultCostModelParams :: Maybe CostModelParams
 defaultCostModelParams = extractCostModelParams defaultCekCostModel
 
 defaultUnliftingMode :: UnliftingMode
-defaultUnliftingMode = UnliftingImmediate
+defaultUnliftingMode = UnliftingDeferred
 
 defaultCekParameters :: MachineParameters CekMachineCosts CekValue DefaultUni DefaultFun
 defaultCekParameters = mkMachineParameters defaultUnliftingMode defaultCekCostModel

From 3b26af54fa02cca6a3f4edff21446faf4e346b93 Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Tue, 5 Apr 2022 20:43:19 +0200
Subject: [PATCH 14/17] Docs and fixes and a test

---
 .../.plan.nix/plutus-core.nix                 |   2 +-
 .../.plan.nix/plutus-core.nix                 |   2 +-
 .../.plan.nix/plutus-core.nix                 |   2 +-
 plutus-core/plutus-core.cabal                 |   2 +-
 .../src/PlutusCore/Builtin/KnownType.hs       |  84 +++++++------
 .../src/PlutusCore/Builtin/Meaning.hs         |  54 +++++++--
 .../src/PlutusCore/Builtin/Runtime.hs         | 112 +++++++++++-------
 .../src/PlutusCore/Evaluation/Machine/Ck.hs   |   8 +-
 .../Evaluation/Machine/ExBudgetingDefaults.hs |   4 +-
 .../Evaluation/Machine/Cek/Debug.hs           |  17 ---
 .../Evaluation/Machine/Cek/Internal.hs        |   6 +-
 .../test/Evaluation/Builtins.hs               |   2 +
 .../test/Evaluation/Builtins/Coherence.hs     |  32 +++++
 13 files changed, 212 insertions(+), 115 deletions(-)
 delete mode 100644 plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Debug.hs
 create mode 100644 plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Coherence.hs

diff --git a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix
index 38c767c1bdd..7c08b3a7ff6 100644
--- a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix
+++ b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix
@@ -277,7 +277,6 @@
           "UntypedPlutusCore/DeBruijn"
           "UntypedPlutusCore/Evaluation/Machine/Cek"
           "UntypedPlutusCore/Evaluation/Machine/Cek/Internal"
-          "UntypedPlutusCore/Evaluation/Machine/Cek/Debug"
           "UntypedPlutusCore/Parser"
           "UntypedPlutusCore/Rename"
           "UntypedPlutusCore/MkUPlc"
@@ -618,6 +617,7 @@
           buildable = true;
           modules = [
             "Evaluation/Builtins"
+            "Evaluation/Builtins/Coherence"
             "Evaluation/Builtins/Common"
             "Evaluation/Builtins/Definition"
             "Evaluation/Builtins/MakeRead"
diff --git a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix
index 38c767c1bdd..7c08b3a7ff6 100644
--- a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix
+++ b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix
@@ -277,7 +277,6 @@
           "UntypedPlutusCore/DeBruijn"
           "UntypedPlutusCore/Evaluation/Machine/Cek"
           "UntypedPlutusCore/Evaluation/Machine/Cek/Internal"
-          "UntypedPlutusCore/Evaluation/Machine/Cek/Debug"
           "UntypedPlutusCore/Parser"
           "UntypedPlutusCore/Rename"
           "UntypedPlutusCore/MkUPlc"
@@ -618,6 +617,7 @@
           buildable = true;
           modules = [
             "Evaluation/Builtins"
+            "Evaluation/Builtins/Coherence"
             "Evaluation/Builtins/Common"
             "Evaluation/Builtins/Definition"
             "Evaluation/Builtins/MakeRead"
diff --git a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix
index 38c767c1bdd..7c08b3a7ff6 100644
--- a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix
+++ b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix
@@ -277,7 +277,6 @@
           "UntypedPlutusCore/DeBruijn"
           "UntypedPlutusCore/Evaluation/Machine/Cek"
           "UntypedPlutusCore/Evaluation/Machine/Cek/Internal"
-          "UntypedPlutusCore/Evaluation/Machine/Cek/Debug"
           "UntypedPlutusCore/Parser"
           "UntypedPlutusCore/Rename"
           "UntypedPlutusCore/MkUPlc"
@@ -618,6 +617,7 @@
           buildable = true;
           modules = [
             "Evaluation/Builtins"
+            "Evaluation/Builtins/Coherence"
             "Evaluation/Builtins/Common"
             "Evaluation/Builtins/Definition"
             "Evaluation/Builtins/MakeRead"
diff --git a/plutus-core/plutus-core.cabal b/plutus-core/plutus-core.cabal
index 909c846ee47..1500d9f63e8 100644
--- a/plutus-core/plutus-core.cabal
+++ b/plutus-core/plutus-core.cabal
@@ -140,7 +140,6 @@ library
         UntypedPlutusCore.DeBruijn
         UntypedPlutusCore.Evaluation.Machine.Cek
         UntypedPlutusCore.Evaluation.Machine.Cek.Internal
-        UntypedPlutusCore.Evaluation.Machine.Cek.Debug
         UntypedPlutusCore.Parser
         UntypedPlutusCore.Rename
         UntypedPlutusCore.MkUPlc
@@ -446,6 +445,7 @@ test-suite untyped-plutus-core-test
     hs-source-dirs: untyped-plutus-core/test
     other-modules:
         Evaluation.Builtins
+        Evaluation.Builtins.Coherence
         Evaluation.Builtins.Common
         Evaluation.Builtins.Definition
         Evaluation.Builtins.MakeRead
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs
index 1523fd8112b..b049cd8e3dd 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs
@@ -14,10 +14,12 @@
 {-# LANGUAGE UndecidableInstances  #-}
 
 module PlutusCore.Builtin.KnownType
-    ( ReadKnownError
-    , throwReadKnownErrorWithCause
+    ( KnownTypeError
+    , throwKnownTypeErrorWithCause
     , KnownBuiltinTypeIn
     , KnownBuiltinType
+    , MakeKnownM
+    , ReadKnownM
     , readKnownConstant
     , MakeKnownIn (..)
     , MakeKnown
@@ -48,10 +50,12 @@ import GHC.Exts (inline, oneShot)
 import GHC.TypeLits
 import Universe
 
--- | A constraint for \"@a@ is a 'KnownType' by means of being included in @uni@\".
+-- | 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)
 
--- | A constraint for \"@a@ is a 'KnownType' by means of being included in @UniOf term@\".
+-- | A constraint for \"@a@ is a 'ReadKnownIn' and 'MakeKnownIn' by means of being included
+-- in @UniOf term@\".
 type KnownBuiltinType val a = KnownBuiltinTypeIn (UniOf val) val a
 
 {- Note [Performance of ReadKnownIn and MakeKnownIn instances]
@@ -60,7 +64,7 @@ It's critically important that 'readKnown' runs in the concrete 'Either' rather
 https://github.com/input-output-hk/plutus/pull/4307
 
 Replacing the @AsUnliftingError err, AsEvaluationFailure err@ constraints with the dedicated
-'ReadKnownError' data type gave us a speedup of up to 4%.
+'KnownTypeError' data type gave us a speedup of up to 4%.
 
 All the same considerations apply to 'makeKnown': https://github.com/input-output-hk/plutus/pull/4421
 
@@ -160,27 +164,27 @@ constraints are completely different in the two cases and we keep the two concep
 (there doesn't seem to be any cons to that).
 -}
 
--- | The type of errors that 'readKnown' can return.
-data ReadKnownError
-    = ReadKnownUnliftingError UnliftingError
-    | ReadKnownEvaluationFailure
+-- | The type of errors that 'readKnown' and 'makeKnown' can return.
+data KnownTypeError
+    = KnownTypeUnliftingError UnliftingError
+    | KnownTypeEvaluationFailure
     deriving stock (Eq)
 
-makeClassyPrisms ''ReadKnownError
+makeClassyPrisms ''KnownTypeError
 
-instance AsUnliftingError ReadKnownError where
-    _UnliftingError = _ReadKnownUnliftingError
+instance AsUnliftingError KnownTypeError where
+    _UnliftingError = _KnownTypeUnliftingError
 
-instance AsEvaluationFailure ReadKnownError where
-    _EvaluationFailure = _EvaluationFailureVia ReadKnownEvaluationFailure
+instance AsEvaluationFailure KnownTypeError where
+    _EvaluationFailure = _EvaluationFailureVia KnownTypeEvaluationFailure
 
--- | Throw a @ErrorWithCause ReadKnownError cause@.
-throwReadKnownErrorWithCause
+-- | Throw a @ErrorWithCause KnownTypeError cause@.
+throwKnownTypeErrorWithCause
     :: (MonadError (ErrorWithCause err cause) m, AsUnliftingError err, AsEvaluationFailure err)
-    => ErrorWithCause ReadKnownError cause -> m void
-throwReadKnownErrorWithCause (ErrorWithCause rkErr cause) = case rkErr of
-    ReadKnownUnliftingError unlErr -> throwingWithCause _UnliftingError unlErr cause
-    ReadKnownEvaluationFailure     -> throwingWithCause _EvaluationFailure () cause
+    => ErrorWithCause KnownTypeError cause -> m void
+throwKnownTypeErrorWithCause (ErrorWithCause rkErr cause) = case rkErr of
+    KnownTypeUnliftingError unlErr -> throwingWithCause _UnliftingError unlErr cause
+    KnownTypeEvaluationFailure     -> throwingWithCause _EvaluationFailure () cause
 
 typeMismatchError
     :: GShow uni
@@ -196,17 +200,35 @@ typeMismatchError uniExp uniAct = fromString $ concat
 -- failure message and evaluation is about to be shut anyway.
 {-# NOINLINE typeMismatchError #-}
 
+{- Note [MakeKnownM and ReadKnownM being type synonyms]
+Normally it's a good idea for an exported abstraction not to be a type synonym, since a @newtype@
+is cheap, looks good in error messages and clearly emphasize an abstraction barrier. However we
+make 'MakeKnownM' and 'ReadKnownM' type synonyms for convenience: that way we don't need to derive
+a ton of instances (and add new ones whenever we need them), wrap and unwrap all the time
+(including in user code), which can be non-trivial for such performance-sensitive code (see e.g.
+'coerceVia' and 'coerceArg') and there is no abstraction barrier anyway.
+-}
+
+-- See Note [MakeKnownM and ReadKnownM being type synonyms].
+-- | The monad that 'makeKnown' runs in.
+type MakeKnownM cause = ExceptT (ErrorWithCause KnownTypeError cause) Emitter
+
+-- See Note [MakeKnownM and ReadKnownM being type synonyms].
+-- | The monad that 'readKnown' runs in.
+type ReadKnownM cause = Either (ErrorWithCause KnownTypeError cause)
+
 -- See Note [Unlifting values of built-in types].
 -- | Convert a constant embedded into a PLC term to the corresponding Haskell value.
 readKnownConstant
     :: forall val a cause. KnownBuiltinType val a
-    => Maybe cause -> val -> Either (ErrorWithCause ReadKnownError cause) a
--- See Note [Performance of KnownTypeIn instances].
+    => Maybe cause -> val -> ReadKnownM cause a
+-- Note [Performance of ReadKnownIn and MakeKnownIn instances]
 readKnownConstant mayCause val = asConstant mayCause val >>= oneShot \case
     Some (ValueOf uniAct x) -> do
         let uniExp = knownUni @_ @(UniOf val) @a
         -- 'geq' matches on its first argument first, so we make the type tag that will be known
-        -- statically (because this function will be inlined) go first in order for GHC to optimize some of the matching away.
+        -- statically (because this function will be inlined) go first in order for GHC to
+        -- optimize some of the matching away.
         case uniExp `geq` uniAct of
             Just Refl -> pure x
             Nothing   -> Left $
@@ -227,10 +249,8 @@ class uni ~ UniOf val => MakeKnownIn uni val a where
     -- See Note [Cause of failure].
     -- | Convert a Haskell value to the corresponding PLC val.
     -- The inverse of 'readKnown'.
-    makeKnown :: Maybe cause -> a -> ExceptT (ErrorWithCause ReadKnownError cause) Emitter val
-    default makeKnown
-        :: KnownBuiltinType val a
-        => Maybe cause -> a -> ExceptT (ErrorWithCause ReadKnownError cause) Emitter val
+    makeKnown :: Maybe cause -> a -> MakeKnownM cause val
+    default makeKnown :: KnownBuiltinType 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.
@@ -244,10 +264,8 @@ class uni ~ UniOf val => ReadKnownIn uni val a where
     -- See Note [Cause of failure].
     -- | Convert a PLC val to the corresponding Haskell value.
     -- The inverse of 'makeKnown'.
-    readKnown :: Maybe cause -> val -> Either (ErrorWithCause ReadKnownError cause) a
-    default readKnown
-        :: KnownBuiltinType val a
-        => Maybe cause -> val -> Either (ErrorWithCause ReadKnownError cause) a
+    readKnown :: Maybe cause -> val -> ReadKnownM cause a
+    default readKnown :: KnownBuiltinType 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 #-}
@@ -256,7 +274,7 @@ type ReadKnown val = ReadKnownIn (UniOf val) val
 
 makeKnownRun
     :: MakeKnownIn uni val a
-    => Maybe cause -> a -> (Either (ErrorWithCause ReadKnownError cause) val, DList Text)
+    => Maybe cause -> a -> (ReadKnownM cause val, DList Text)
 makeKnownRun mayCause = runEmitter . runExceptT . makeKnown mayCause
 {-# INLINE makeKnownRun #-}
 
@@ -271,7 +289,7 @@ readKnownSelf
        , AsUnliftingError err, AsEvaluationFailure err
        )
     => val -> Either (ErrorWithCause err val) a
-readKnownSelf val = either throwReadKnownErrorWithCause pure $ readKnown (Just val) val
+readKnownSelf val = either throwKnownTypeErrorWithCause pure $ readKnown (Just val) val
 {-# INLINE readKnownSelf #-}
 
 instance MakeKnownIn uni val a => MakeKnownIn uni val (EvaluationResult a) where
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
index 28491b4100e..04e22407b16 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
@@ -7,6 +7,7 @@
 {-# LANGUAGE FlexibleInstances         #-}
 {-# LANGUAGE FunctionalDependencies    #-}
 {-# LANGUAGE PolyKinds                 #-}
+{-# LANGUAGE StandaloneKindSignatures  #-}
 {-# LANGUAGE TypeApplications          #-}
 {-# LANGUAGE TypeFamilies              #-}
 {-# LANGUAGE TypeOperators             #-}
@@ -122,11 +123,15 @@ function and the 'TypeScheme' of the built-in function will be derived automatic
 monomorphic and simply-polymorphic cases no types need to be specified at all.
 -}
 
+-- | Compute the length of a type-level list.
+type Length :: forall a. [a] -> Peano
 type family Length xs where
     Length '[]       = 'Z
     Length (_ ': xs) = 'S (Length xs)
 
-type family GetArgs a :: [GHC.Type] where
+-- | Chop a function type to get a list of its argument types.
+type GetArgs :: GHC.Type -> [GHC.Type]
+type family GetArgs a where
     GetArgs (a -> b) = a ': GetArgs b
     GetArgs _        = '[]
 
@@ -134,15 +139,27 @@ type family GetArgs a :: [GHC.Type] where
 class KnownMonotype val args res a | args res -> a, a -> res where
     knownMonotype :: TypeScheme val args res
     knownMonoruntime :: RuntimeScheme (Length args)
-    toImmediateF :: FoldArgs args res -> ToDenotationType val (Length args)
-    toDeferredF :: ReadKnownM (FoldArgs args res) -> ToDenotationType val (Length args)
+
+    -- | Convert the denotation of a builtin to its runtime counterpart with immediate unlifting.
+    toImmediateF :: FoldArgs args res -> ToRuntimeDenotationType val (Length args)
+
+    -- | Convert the denotation of a builtin to its runtime counterpart with deferred unlifting.
+    -- The argument is in 'ReadKnownM', because that's what deferred unlifting amounts to:
+    -- passing the action returning the builtin application around until full saturation, which is
+    -- when the action actually gets run.
+    toDeferredF :: ReadKnownM () (FoldArgs args res) -> ToRuntimeDenotationType val (Length args)
 
 -- | Once we've run out of term-level arguments, we return a 'TypeSchemeResult'.
 instance (res ~ res', KnownTypeAst (UniOf val) res, MakeKnown val res) =>
             KnownMonotype val '[] res res' where
     knownMonotype = TypeSchemeResult
     knownMonoruntime = RuntimeSchemeResult
+
     toImmediateF = makeKnown (Just ())
+    {-# INLINE toImmediateF #-}
+
+    -- For deferred unlifting we need to lift the 'ReadKnownM' action into 'MakeKnownM',
+    -- hence 'liftEither'.
     toDeferredF getRes = liftEither getRes >>= makeKnown (Just ())
     {-# INLINE toDeferredF #-}
 
@@ -153,8 +170,24 @@ instance
         ) => KnownMonotype val (arg ': args) res (arg -> a) where
     knownMonotype = TypeSchemeArrow knownMonotype
     knownMonoruntime = RuntimeSchemeArrow $ knownMonoruntime @val @args @res
+
+    -- Unlift, then recurse.
     toImmediateF f = fmap (toImmediateF @val @args @res . f) . readKnown (Just ())
+    {-# INLINE toImmediateF #-}
+
+    -- Grow the builtin application within the received action and recurse on the result.
     toDeferredF getF = \arg ->
+        -- The bang is very important: without it GHC thinks that the argument may not be needed in
+        -- the end and so creates a thunk for it, which is not only unnecessary allocation, but also
+        -- prevents things from being unboxed. So ironically computing the unlifted value strictly
+        -- is the best way of doing deferred unlifting. All this means that while the resulting
+        -- 'Either' is only handled upon full saturation and any evaluation failure is only
+        -- registered when the whole builtin application is evaluated, a Haskell exception will
+        -- occur the same way as with immediate unlifting. It shouldn't matter though, because a
+        -- builtin is not supposed to throw an exception at any stage, that would be a bug regardless
+        -- of how unlifting is aligned.
+        --
+        -- 'pure' signifies that no failure can occur at this point.
         pure . toDeferredF @val @args @res $! getF <*> readKnown (Just ()) arg
     {-# INLINE toDeferredF #-}
 
@@ -191,14 +224,17 @@ makeBuiltinMeaning
        , ElaborateFromTo 0 j val a, KnownPolytype binds val args res a
        )
     => a -> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
-makeBuiltinMeaning f
-    = BuiltinMeaning (knownPolytype @binds @val @args @res) f
-    . BuiltinRuntimeOptions
-        (knownPolyruntime @binds @val @args @res)
-        (toImmediateF @val @args @res f)
-        (toDeferredF @val @args @res $ pure f)
+makeBuiltinMeaning f toExF =
+    BuiltinMeaning (knownPolytype @binds @val @args @res) f $
+        BuiltinRuntimeOptions
+            { _broRuntimeScheme = knownPolyruntime @binds @val @args @res
+            , _broImmediateF    = toImmediateF @val @args @res f
+            , _broDeferredF     = toDeferredF @val @args @res $ pure f
+            , _broToExF         = toExF
+            }
 {-# INLINE makeBuiltinMeaning #-}
 
+-- | Convert a 'BuiltinMeaning' to a 'BuiltinRuntime' given an 'UnliftingMode' and a cost model.
 toBuiltinRuntime :: UnliftingMode -> cost -> BuiltinMeaning val cost -> BuiltinRuntime val
 toBuiltinRuntime unlMode cost (BuiltinMeaning _ _ runtimeOpts) =
     fromBuiltinRuntimeOptions unlMode cost runtimeOpts
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index f5912f01cf9..87bc2427462 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -1,17 +1,17 @@
-{-# LANGUAGE RankNTypes     #-}
-{-# LANGUAGE TypeFamilies   #-}
+{-# LANGUAGE DataKinds                #-}
+{-# LANGUAGE GADTs                    #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies             #-}
+{-# LANGUAGE TypeOperators            #-}
 
-{-# LANGUAGE DataKinds      #-}
-{-# LANGUAGE GADTs          #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE TypeOperators  #-}
-
-{-# LANGUAGE StrictData     #-}
+{-# LANGUAGE StrictData               #-}
 
 module PlutusCore.Builtin.Runtime where
 
 import PlutusPrelude
 
+import PlutusCore.Evaluation.Machine.ExBudget
+import PlutusCore.Evaluation.Machine.ExMemory
 import PlutusCore.Evaluation.Machine.Exception
 
 import Control.DeepSeq
@@ -21,28 +21,20 @@ import Data.Array
 import Data.Kind qualified as GHC (Type)
 import PlutusCore.Builtin.KnownType
 
-import PlutusCore.Builtin.Emitter
-import PlutusCore.Evaluation.Machine.ExBudget
-import PlutusCore.Evaluation.Machine.ExMemory
-
-data Nat = Z | S Nat
+-- | Peano numbers. Normally called @Nat@, but that is already reserved by @base@.
+data Peano
+    = Z
+    | S Peano
 
 -- | Same as 'TypeScheme' except this one doesn't contain any evaluation-irrelevant types stuff.
+-- @n@ represents the number of term-level arguments that a builtin takes.
 data RuntimeScheme n where
     RuntimeSchemeResult :: RuntimeScheme 'Z
-    RuntimeSchemeArrow :: RuntimeScheme n -> RuntimeScheme ('S n)
-    RuntimeSchemeAll :: RuntimeScheme n -> RuntimeScheme n
-
-type MakeKnownM = ExceptT (ErrorWithCause ReadKnownError ()) Emitter
-type ReadKnownM = Either (ErrorWithCause ReadKnownError ())
+    RuntimeSchemeArrow  :: RuntimeScheme n -> RuntimeScheme ('S n)
+    RuntimeSchemeAll    :: RuntimeScheme n -> RuntimeScheme n
 
-type family ToDenotationType val (n :: Nat) :: GHC.Type where
-    ToDenotationType val 'Z     = MakeKnownM val
-    ToDenotationType val ('S n) = val -> ReadKnownM (ToDenotationType val n)
-
-type family ToCostingType (n :: Nat) :: GHC.Type where
-    ToCostingType 'Z     = ExBudget
-    ToCostingType ('S n) = ExMemory -> ToCostingType n
+deriving stock instance Eq   (RuntimeScheme n)
+deriving stock instance Show (RuntimeScheme n)
 
 -- we use strictdata, so this is just for the purpose of completeness
 instance NFData (RuntimeScheme n) where
@@ -51,45 +43,79 @@ instance NFData (RuntimeScheme n) where
         RuntimeSchemeArrow arg -> rnf arg
         RuntimeSchemeAll arg   -> rnf arg
 
+-- | Compute the runtime denotation type of a builtin given the type of values and the number of
+-- arguments that the builtin takes. A \"runtime denotation type\" is different from a regular
+-- denotation type in that a regular one can have any 'ReadKnownIn' type as an argument and can
+-- return any 'MakeKnownIn' type, while in a runtime one only @val@ can appear as the type of an
+-- argument, as well as in the result type. This is what we get by calling 'readKnown' over each
+-- argument of the denotation and calling 'makeKnown' over its result.
+type ToRuntimeDenotationType :: GHC.Type -> Peano -> GHC.Type
+type family ToRuntimeDenotationType val n where
+    ToRuntimeDenotationType val 'Z     = MakeKnownM () val
+    -- 'ReadKnownM' is required here only for immediate unlifting, because deferred unlifting
+    -- doesn't need the ability to fail in the middle of a builtin application, but having a uniform
+    -- interface for both the ways of doing unlifting is way too convenient, hence we decided to pay
+    -- the price (about 1-2% of total evaluation time) for now.
+    ToRuntimeDenotationType val ('S n) = val -> ReadKnownM () (ToRuntimeDenotationType val n)
+
+-- | Compute the costing type for a builtin given the number of arguments that the builtin takes.
+type ToCostingType :: Peano -> GHC.Type
+type family ToCostingType n where
+    ToCostingType 'Z     = ExBudget
+    ToCostingType ('S n) = ExMemory -> ToCostingType n
+
 -- We tried instantiating 'BuiltinMeaning' on the fly and that was slower than precaching
 -- 'BuiltinRuntime's.
 -- | A 'BuiltinRuntime' represents a possibly partial builtin application.
 -- We get an initial 'BuiltinRuntime' representing an empty builtin application (i.e. just the
--- builtin with no arguments) by instantiating (via 'toBuiltinRuntime') a 'BuiltinMeaning'.
+-- builtin with no arguments) by instantiating (via 'fromBuiltinRuntimeOptions') a
+-- 'BuiltinRuntimeOptions'.
 --
 -- A 'BuiltinRuntime' contains info that is used during evaluation:
 --
--- 1. the 'TypeScheme' of the uninstantiated part of the builtin. I.e. initially it's the type
+-- 1. the 'RuntimeScheme' of the uninstantiated part of the builtin. I.e. initially it's the runtime
 --      scheme of the whole builtin, but applying or type-instantiating the builtin peels off
---      the corresponding constructor from the type scheme
--- 2. the (possibly partially instantiated) denotation
+--      the corresponding constructor from the runtime scheme
+-- 2. the (possibly partially instantiated) runtime denotation
 -- 3. the (possibly partially instantiated) costing function
 --
--- All the three are in sync in terms of partial instantiatedness due to 'TypeScheme' being a
--- GADT and 'FoldArgs' and 'FoldArgsEx' operating on the index of that GADT.
+-- All the three are in sync in terms of partial instantiatedness due to 'RuntimeScheme' being a
+-- GADT and 'ToRuntimeDenotationType' and 'ToCostingType' operating on the index of that GADT.
 data BuiltinRuntime val =
     forall n. BuiltinRuntime
         (RuntimeScheme n)
-        ~(ToDenotationType val n)  -- Must be lazy, because we don't want to compute the denotation
-                                   -- when it's fully saturated before figuring out what it's going
-                                   -- to cost.
+        ~(ToRuntimeDenotationType val n)  -- Must be lazy, because we don't want to compute the
+                                          -- denotation when it's fully saturated before figuring
+                                          -- out what it's going to cost.
         (ToCostingType n)
 
-data BuiltinRuntimeOptions n val cost =
-    BuiltinRuntimeOptions
-        (RuntimeScheme n)
-        (ToDenotationType val n)
-        (ToDenotationType val n)
-        (cost -> ToCostingType n)
-
+-- | Determines how to unlift arguments. The difference is that with 'UnliftingImmediate' unlifting
+-- is performed immediately after a builtin gets the argument and so can fail immediately too, while
+-- with deferred unlifting all arguments are unlifted upon full saturation, hence no failure can
+-- occur until that. The former makes it much harder to specify the behaviour of builtins and
+-- so 'UnliftingDeferred' is the prefered mode. 'UnliftingDeferred' is faster too, but not by much
+-- (in the order of a few percent of total evaluation time).
 data UnliftingMode
     = UnliftingImmediate
     | UnliftingDeferred
 
+-- | A 'BuiltinRuntimeOptions' is a precursor to 'BuiltinRuntime'. One gets the latter from the
+-- former by choosing the runtime denotation of the builtin (either '_broImmediateF' for immediate
+-- unlifting or '_broDeferredF' for deferred unlifting, see 'UnliftingMode' for detauls) and by
+-- instantiating '_broToExF' with a cost model to get the costing function for the builtin.
+data BuiltinRuntimeOptions n val cost = BuiltinRuntimeOptions
+    { _broRuntimeScheme :: RuntimeScheme n
+    , _broImmediateF    :: ToRuntimeDenotationType val n
+    , _broDeferredF     :: ToRuntimeDenotationType val n
+    , _broToExF         :: cost -> ToCostingType n
+    }
+
+-- | Convert a 'BuiltinRuntimeOptions' to a 'BuiltinRuntime' given an 'UnliftingMode' and a cost
+-- model.
 fromBuiltinRuntimeOptions
     :: UnliftingMode -> cost -> BuiltinRuntimeOptions n val cost -> BuiltinRuntime val
-fromBuiltinRuntimeOptions unlMode cost (BuiltinRuntimeOptions sch immF defF exF) =
-    BuiltinRuntime sch f $ exF cost where
+fromBuiltinRuntimeOptions unlMode cost (BuiltinRuntimeOptions sch immF defF toExF) =
+    BuiltinRuntime sch f $ toExF cost where
         f = case unlMode of
                 UnliftingImmediate -> immF
                 UnliftingDeferred  -> defF
diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
index c5348e864bb..5c8a4f1af43 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
@@ -71,9 +71,9 @@ evalBuiltinApp term runtime@(BuiltinRuntime sch getX _) = case sch of
         let (errOrRes, logs) = runEmitter $ runExceptT getX
         emitCkM logs
         case errOrRes of
-            Left err -> throwReadKnownErrorWithCause $ term <$ err
-            Right x  -> pure x
-    _                   -> pure $ VBuiltin term runtime
+            Left err  -> throwKnownTypeErrorWithCause $ term <$ err
+            Right res -> pure res
+    _ -> pure $ VBuiltin term runtime
 
 ckValueToTerm :: CkValue uni fun -> Term TyName Name uni fun ()
 ckValueToTerm = \case
@@ -307,7 +307,7 @@ applyEvaluate stack (VBuiltin term (BuiltinRuntime sch f exF)) arg = do
         -- It's only possible to apply a builtin application if the builtin expects a term
         -- argument next.
         RuntimeSchemeArrow schB -> case f arg of
-            Left err -> throwReadKnownErrorWithCause $ argTerm <$ err
+            Left err -> throwKnownTypeErrorWithCause $ argTerm <$ err
             Right y  -> do
                 -- The CK machine does not support costing, so we just apply the costing function
                 -- to 'mempty'.
diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs
index 558ebaebaa2..3bfb15fb926 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs
@@ -76,7 +76,7 @@ defaultCostModelParams :: Maybe CostModelParams
 defaultCostModelParams = extractCostModelParams defaultCekCostModel
 
 defaultUnliftingMode :: UnliftingMode
-defaultUnliftingMode = UnliftingDeferred
+defaultUnliftingMode = UnliftingImmediate
 
 defaultCekParameters :: MachineParameters CekMachineCosts CekValue DefaultUni DefaultFun
 defaultCekParameters = mkMachineParameters defaultUnliftingMode defaultCekCostModel
@@ -87,7 +87,7 @@ unitCekParameters =
         CostModel unitCekMachineCosts unitCostBuiltinCostModel
 
 defaultBuiltinsRuntime :: HasConstantIn DefaultUni term => BuiltinsRuntime DefaultFun term
-defaultBuiltinsRuntime = toBuiltinsRuntime UnliftingImmediate defaultBuiltinCostModel
+defaultBuiltinsRuntime = toBuiltinsRuntime defaultUnliftingMode defaultBuiltinCostModel
 
 
 -- A cost model with unit costs, so we can count how often each builtin is called
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Debug.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Debug.hs
deleted file mode 100644
index 49d75cbe21f..00000000000
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Debug.hs
+++ /dev/null
@@ -1,17 +0,0 @@
-{-# LANGUAGE TypeFamilies #-}
-
-{-# OPTIONS_GHC -ddump-simpl -ddump-to-file -dsuppress-all -fforce-recomp -dumpdir /tmp/dumps #-}
-
-module UntypedPlutusCore.Evaluation.Machine.Cek.Debug where
-
-import UntypedPlutusCore.Evaluation.Machine.Cek.Internal
-
-import PlutusCore.Builtin
-import PlutusCore.Default
-
-import GHC.Exts (inline)
-
-toBuiltinsRuntimeDef
-    :: (cost ~ CostingPart uni fun, uni ~ DefaultUni, fun ~ DefaultFun)
-    => cost -> BuiltinsRuntime fun (CekValue uni fun)
-toBuiltinsRuntimeDef = inline toBuiltinsRuntime UnliftingImmediate
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
index 11f47c5a3f0..81d6f864a62 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
@@ -568,8 +568,8 @@ evalBuiltinApp fun term env runtime@(BuiltinRuntime sch getX cost) = case sch of
         let !(errOrRes, logs) = runEmitter $ runExceptT getX
         ?cekEmitter logs
         case errOrRes of
-            Left err -> throwReadKnownErrorWithCause $ term <$ err
-            Right x  -> pure x
+            Left err  -> throwKnownTypeErrorWithCause $ term <$ err
+            Right res -> pure res
     _ -> pure $ VBuiltin fun term env runtime
 {-# INLINE evalBuiltinApp #-}
 
@@ -710,7 +710,7 @@ enterComputeCek = computeCek (toWordArray 0) where
             -- It's only possible to apply a builtin application if the builtin expects a term
             -- argument next.
             RuntimeSchemeArrow schB -> case f arg of
-                Left err -> throwReadKnownErrorWithCause $ argTerm <$ err
+                Left err -> throwKnownTypeErrorWithCause $ argTerm <$ err
                 Right y  -> do
                     -- TODO: should we bother computing that 'ExMemory' eagerly? We may not need it.
                     -- We pattern match on @arg@ twice: in 'readKnown' and in 'toExMemory'.
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Builtins.hs b/plutus-core/untyped-plutus-core/test/Evaluation/Builtins.hs
index 45b284317c6..0b7342ed887 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Builtins.hs
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Builtins.hs
@@ -1,5 +1,6 @@
 module Evaluation.Builtins (test_builtins) where
 
+import Evaluation.Builtins.Coherence (test_TypeSchemesAndRuntimeSchemesAgree)
 import Evaluation.Builtins.Definition (test_definition)
 import Evaluation.Builtins.MakeRead (test_makeRead)
 
@@ -10,4 +11,5 @@ test_builtins =
     testGroup "builtins"
         [ test_definition
         , test_makeRead
+        , test_TypeSchemesAndRuntimeSchemesAgree
         ]
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Coherence.hs b/plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Coherence.hs
new file mode 100644
index 00000000000..74f0a49f21d
--- /dev/null
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Builtins/Coherence.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE GADTs            #-}
+{-# LANGUAGE TypeApplications #-}
+
+-- Turning off all optimization, because otherwise 'toBuiltinMeaning' seems to inline separately for
+-- each builtin, causing the simplifier to exhaust all its ticks.
+{-# OPTIONS_GHC -O0 #-}
+
+module Evaluation.Builtins.Coherence where
+
+import PlutusPrelude
+
+import PlutusCore
+import PlutusCore.Builtin
+
+import Data.Foldable
+import Test.Tasty
+import Test.Tasty.HUnit
+
+typeSchemeToRuntimeScheme :: TypeScheme val args res -> RuntimeScheme (Length args)
+typeSchemeToRuntimeScheme TypeSchemeResult = RuntimeSchemeResult
+typeSchemeToRuntimeScheme (TypeSchemeArrow schB) =
+    RuntimeSchemeArrow $ typeSchemeToRuntimeScheme schB
+typeSchemeToRuntimeScheme (TypeSchemeAll _ schK) =
+    RuntimeSchemeAll $ typeSchemeToRuntimeScheme schK
+
+test_TypeSchemesAndRuntimeSchemesAgree :: TestTree
+test_TypeSchemesAndRuntimeSchemesAgree =
+    testCase "type schemes are coherent with runtime schemes" $
+        for_ (enumeration @DefaultFun) $ \fun ->
+            case toBuiltinMeaning @_ @_ @(Term TyName Name _ _ ()) fun of
+                BuiltinMeaning typeSch _ (BuiltinRuntimeOptions runtimeSch _ _ _) ->
+                    typeSchemeToRuntimeScheme typeSch @?= runtimeSch

From e80dbb757d6e686b6fb17b3d362a6377328fbe3c Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Wed, 6 Apr 2022 17:10:06 +0200
Subject: [PATCH 15/17] Compile both the ways of doing unlifting

---
 .../examples/PlutusCore/Examples/Builtins.hs  |  2 +-
 .../src/PlutusCore/Builtin/Meaning.hs         |  1 +
 .../src/Plutus/V1/Ledger/EvaluationContext.hs | 52 +++++++++++++------
 3 files changed, 37 insertions(+), 18 deletions(-)

diff --git a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
index cf164b3b4de..96a99b69476 100644
--- a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
+++ b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
@@ -138,7 +138,7 @@ instance (ToBuiltinMeaning uni fun1, ToBuiltinMeaning uni fun2) =>
 defBuiltinsRuntimeExt
     :: HasConstantIn DefaultUni term
     => BuiltinsRuntime (Either DefaultFun ExtensionFun) term
-defBuiltinsRuntimeExt = toBuiltinsRuntime UnliftingImmediate (defaultBuiltinCostModel, ())
+defBuiltinsRuntimeExt = toBuiltinsRuntime defaultUnliftingMode (defaultBuiltinCostModel, ())
 
 data PlcListRep (a :: GHC.Type)
 instance KnownTypeAst uni a => KnownTypeAst uni (PlcListRep a) where
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
index 04e22407b16..c9363519b06 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
@@ -70,6 +70,7 @@ class (Bounded fun, Enum fun, Ix fun) => ToBuiltinMeaning uni fun where
     -- | The @cost@ part of 'BuiltinMeaning'.
     type CostingPart uni fun
 
+    -- | Get the 'BuiltinMeaning' of a built-in function.
     toBuiltinMeaning :: HasConstantIn uni val => fun -> BuiltinMeaning val (CostingPart uni fun)
 
 -- | Get the type of a built-in function.
diff --git a/plutus-ledger-api/src/Plutus/V1/Ledger/EvaluationContext.hs b/plutus-ledger-api/src/Plutus/V1/Ledger/EvaluationContext.hs
index ba0b19a77fa..2fe7369d947 100644
--- a/plutus-ledger-api/src/Plutus/V1/Ledger/EvaluationContext.hs
+++ b/plutus-ledger-api/src/Plutus/V1/Ledger/EvaluationContext.hs
@@ -1,8 +1,16 @@
+{-# LANGUAGE DeriveAnyClass #-}
+
+-- GHC is asked to do quite a lot of optimization in this module, so we're increasing the amount of
+-- ticks for the simplifier not to run out of them.
+{-# OPTIONS_GHC -fsimpl-tick-factor=200 #-}
+
 module Plutus.V1.Ledger.EvaluationContext
     ( EvaluationContext
     , mkEvaluationContext
     , CostModelParams
     , isCostModelParamsWellFormed
+    , machineParametersImmediate
+    , machineParametersDeferred
     , toMachineParameters
     , costModelParamNames
     , costModelParamsForTesting
@@ -21,12 +29,24 @@ import Data.Maybe
 import Data.Set as Set
 import Data.Text qualified as Text
 import GHC.Exts (inline)
+import GHC.Generics
+
+type DefaultMachineParameters =
+    Plutus.MachineParameters CekMachineCosts CekValue DefaultUni DefaultFun
 
 -- | An opaque type that contains all the static parameters that the evaluator needs to evaluate a script.
 -- This is so that they can be computed once and cached, rather than recomputed on every evaluation.
-newtype EvaluationContext = EvaluationContext
-    { toMachineParameters :: Plutus.MachineParameters CekMachineCosts CekValue DefaultUni DefaultFun }
-    deriving newtype NFData
+data EvaluationContext = EvaluationContext
+    { machineParametersImmediate :: DefaultMachineParameters
+    , machineParametersDeferred  :: DefaultMachineParameters
+    }
+    deriving stock Generic
+    deriving anyclass NFData
+
+toMachineParameters :: EvaluationContext -> DefaultMachineParameters
+toMachineParameters = case defaultUnliftingMode of
+    UnliftingImmediate -> machineParametersImmediate
+    UnliftingDeferred  -> machineParametersDeferred
 
 {- Note [Inlining meanings of builtins]
 It's vitally important to inline the 'toBuiltinMeaning' method of a set of built-in functions as
@@ -50,23 +70,21 @@ as we did have cases where sticking 'inline' on something that already had @INLI
 inlining).
 -}
 
+mkMachineParametersFor :: UnliftingMode -> Plutus.CostModelParams -> Maybe DefaultMachineParameters
+mkMachineParametersFor unlMode newCMP =
+    inline Plutus.mkMachineParameters unlMode <$>
+        Plutus.applyCostModelParams Plutus.defaultCekCostModel newCMP
+{-# INLINE mkMachineParametersFor #-}
+
 -- See Note [Inlining meanings of builtins].
 -- | Build the 'EvaluationContext'.
 --
 -- The input is a `Map` of strings to cost integer values (aka `Plutus.CostModelParams`, `Alonzo.CostModel`)
-mkEvaluationContextUnliftingImmediate :: Plutus.CostModelParams -> Maybe EvaluationContext
-mkEvaluationContextUnliftingImmediate newCMP =
-    EvaluationContext . inline Plutus.mkMachineParameters UnliftingImmediate <$>
-        Plutus.applyCostModelParams Plutus.defaultCekCostModel newCMP
-
-mkEvaluationContextUnliftingDeferred :: Plutus.CostModelParams -> Maybe EvaluationContext
-mkEvaluationContextUnliftingDeferred newCMP =
-    EvaluationContext . inline Plutus.mkMachineParameters UnliftingImmediate <$>
-        Plutus.applyCostModelParams Plutus.defaultCekCostModel newCMP
-
-mkEvaluationContext :: UnliftingMode -> Plutus.CostModelParams -> Maybe EvaluationContext
-mkEvaluationContext UnliftingImmediate = mkEvaluationContextUnliftingImmediate
-mkEvaluationContext UnliftingDeferred  = mkEvaluationContextUnliftingDeferred
+mkEvaluationContext :: Plutus.CostModelParams -> Maybe EvaluationContext
+mkEvaluationContext newCMP =
+    EvaluationContext
+        <$> inline mkMachineParametersFor UnliftingImmediate newCMP
+        <*> inline mkMachineParametersFor UnliftingDeferred newCMP
 
 -- | Comparably expensive to `mkEvaluationContext`, so it should only be used sparingly.
 isCostModelParamsWellFormed :: Plutus.CostModelParams -> Bool
@@ -83,4 +101,4 @@ costModelParamsForTesting = fromJust Plutus.defaultCostModelParams
 
 -- | only to be for testing purposes: make an evaluation context by applying an empty set of protocol parameters
 evalCtxForTesting :: EvaluationContext
-evalCtxForTesting = fromJust $ mkEvaluationContext defaultUnliftingMode mempty
+evalCtxForTesting = fromJust $ mkEvaluationContext mempty

From 540c0cbb7d9f241dcd31d4669bfc7d2e6ab76a4a Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Wed, 6 Apr 2022 19:48:01 +0200
Subject: [PATCH 16/17] More docs

---
 .../plutus-core/src/PlutusCore/Builtin/Meaning.hs    | 12 ++++++++++++
 .../plutus-core/src/PlutusCore/Builtin/Runtime.hs    |  5 ++---
 2 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
index c9363519b06..0cc57c28d46 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
@@ -137,6 +137,18 @@ type family GetArgs a where
     GetArgs _        = '[]
 
 -- | A class that allows us to derive a monotype for a builtin.
+-- We could've easily computed a 'RuntimeScheme' from a 'TypeScheme' but not statically (due to
+-- unfolding not working for recursive functions and 'TypeScheme' is recursive, i.e. the conversion
+-- can only be a recursive function), and so it would cause us to retain a lot of
+-- evaluation-irrelevant stuff in the constructors of 'TypeScheme', which makes it much harder to
+-- read the Core. Technically speaking, we could convert a 'TypeScheme' to a 'RuntimeScheme'
+-- statically if we changed the definition of 'TypeScheme' and made it a singleton, but then the
+-- conversion function would have to become a class anyway and we'd just replicate what we have here,
+-- except in a much more complicated way.
+-- It's also more efficient to generate 'RuntimeScheme's directly, but that shouldn't really matter, -- given that they computed only once and cached afterwards.
+--
+-- 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
     knownMonoruntime :: RuntimeScheme (Length args)
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index 87bc2427462..214c613065c 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -93,15 +93,14 @@ data BuiltinRuntime val =
 -- is performed immediately after a builtin gets the argument and so can fail immediately too, while
 -- with deferred unlifting all arguments are unlifted upon full saturation, hence no failure can
 -- occur until that. The former makes it much harder to specify the behaviour of builtins and
--- so 'UnliftingDeferred' is the prefered mode. 'UnliftingDeferred' is faster too, but not by much
--- (in the order of a few percent of total evaluation time).
+-- so 'UnliftingDeferred' is the preferred mode.
 data UnliftingMode
     = UnliftingImmediate
     | UnliftingDeferred
 
 -- | A 'BuiltinRuntimeOptions' is a precursor to 'BuiltinRuntime'. One gets the latter from the
 -- former by choosing the runtime denotation of the builtin (either '_broImmediateF' for immediate
--- unlifting or '_broDeferredF' for deferred unlifting, see 'UnliftingMode' for detauls) and by
+-- unlifting or '_broDeferredF' for deferred unlifting, see 'UnliftingMode' for details) and by
 -- instantiating '_broToExF' with a cost model to get the costing function for the builtin.
 data BuiltinRuntimeOptions n val cost = BuiltinRuntimeOptions
     { _broRuntimeScheme :: RuntimeScheme n

From 64f3e9a20c12f6e1bfd6e8eac419ce2c6f62adb6 Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Wed, 6 Apr 2022 20:03:45 +0200
Subject: [PATCH 17/17] And a bit more

---
 .../src/Plutus/V1/Ledger/EvaluationContext.hs          | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/plutus-ledger-api/src/Plutus/V1/Ledger/EvaluationContext.hs b/plutus-ledger-api/src/Plutus/V1/Ledger/EvaluationContext.hs
index 2fe7369d947..c40962378cc 100644
--- a/plutus-ledger-api/src/Plutus/V1/Ledger/EvaluationContext.hs
+++ b/plutus-ledger-api/src/Plutus/V1/Ledger/EvaluationContext.hs
@@ -34,8 +34,14 @@ import GHC.Generics
 type DefaultMachineParameters =
     Plutus.MachineParameters CekMachineCosts CekValue DefaultUni DefaultFun
 
--- | An opaque type that contains all the static parameters that the evaluator needs to evaluate a script.
--- This is so that they can be computed once and cached, rather than recomputed on every evaluation.
+-- | An opaque type that contains all the static parameters that the evaluator needs to evaluate a
+-- script.  This is so that they can be computed once and cached, rather than recomputed on every
+-- evaluation.
+--
+-- There are two sets of parameters: one is with immediate unlifting and the other one is with
+-- deferred unlifting. We have to keep both of them, because depending on the language version
+-- either one has to be used or the other. We also compile them separately due to all the inlining
+-- and optimization that need to happen for things to be efficient.
 data EvaluationContext = EvaluationContext
     { machineParametersImmediate :: DefaultMachineParameters
     , machineParametersDeferred  :: DefaultMachineParameters