diff --git a/plutus-core/cost-model/budgeting-bench/Benchmarks/Nops.hs b/plutus-core/cost-model/budgeting-bench/Benchmarks/Nops.hs
index 9aac5e56194..69b96172052 100644
--- a/plutus-core/cost-model/budgeting-bench/Benchmarks/Nops.hs
+++ b/plutus-core/cost-model/budgeting-bench/Benchmarks/Nops.hs
@@ -120,7 +120,7 @@ nopCostModel =
                   (ModelSixArgumentsConstantCost 600)
     }
 
-nopCostParameters :: MachineParameters CekMachineCosts NopFun (CekValue DefaultUni NopFun ())
+nopCostParameters :: MachineParameters CekMachineCosts NopFun (CekValue DefaultUni NopFun)
 nopCostParameters =
     MachineParameters def . mkMachineVariantParameters def $
         CostModel defaultCekMachineCostsForTesting nopCostModel
diff --git a/plutus-core/cost-model/budgeting-bench/Common.hs b/plutus-core/cost-model/budgeting-bench/Common.hs
index 1812fe78731..552d586d661 100644
--- a/plutus-core/cost-model/budgeting-bench/Common.hs
+++ b/plutus-core/cost-model/budgeting-bench/Common.hs
@@ -77,7 +77,7 @@ pairWith f = fmap (\a -> (a, f a))
 
 benchWith
     :: (Pretty fun, Typeable fun)
-    => MachineParameters CekMachineCosts fun (CekValue DefaultUni fun ())
+    => MachineParameters CekMachineCosts fun (CekValue DefaultUni fun)
     -> String
     -> PlainTerm DefaultUni fun
     -> Benchmark
@@ -430,4 +430,3 @@ createThreeTermBuiltinBenchWithWrappers (wrapX, wrapY, wrapZ) fun tys xs ys zs =
     [bgroup (showMemoryUsage (wrapY y))
       [mkBM x y z | z <- zs] | y <- ys] | x <- xs]
   where mkBM x y z = benchDefault (showMemoryUsage (wrapZ z)) $ mkApp3 fun tys x y z
-
diff --git a/plutus-core/docs/BuiltinsOverview.md b/plutus-core/docs/BuiltinsOverview.md
index 08f2289375d..09d43ed5ad2 100644
--- a/plutus-core/docs/BuiltinsOverview.md
+++ b/plutus-core/docs/BuiltinsOverview.md
@@ -213,7 +213,7 @@ Here's a concrete example of what a `TypeScheme` for `DivideInteger` might look
 ```haskell
 divideIntegerTypeScheme ::
     TypeScheme
-        (CekValue DefaultUni fun ann)
+        (CekValue DefaultUni fun)
         '[Integer, Integer]
         (BuiltinResult Integer)
 divideIntegerTypeScheme = TypeSchemeArrow $ TypeSchemeArrow TypeSchemeResult
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 85c4b7de86e..bace2f21a03 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs
@@ -147,19 +147,19 @@ defaultCostModelParamsForVariant = \case
 We don't want this to get inlined in order for this definition not to appear
 faster than the used in production. Also see Note [noinline for saving on
 ticks]. -}
-defaultCekParametersA :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
+defaultCekParametersA :: MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun)
 defaultCekParametersA =
     MachineParameters def $
         noinline mkMachineVariantParameters DefaultFunSemanticsVariantA cekCostModelVariantA
 
 -- See Note [No inlining for MachineParameters]
-defaultCekParametersB :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
+defaultCekParametersB :: MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun)
 defaultCekParametersB =
     MachineParameters def $
         noinline mkMachineVariantParameters DefaultFunSemanticsVariantB cekCostModelVariantB
 
 -- See Note [No inlining for MachineParameters]
-defaultCekParametersC :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
+defaultCekParametersC :: MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun)
 defaultCekParametersC =
     MachineParameters def $
         noinline mkMachineVariantParameters DefaultFunSemanticsVariantC cekCostModelVariantC
@@ -182,9 +182,8 @@ defaultBuiltinsRuntimeForSemanticsVariant semvar =
           DefaultFunSemanticsVariantC -> builtinCostModelVariantC
 
 defaultCekParametersForVariant
-  :: Typeable ann
-  => BuiltinSemanticsVariant DefaultFun
-  -> MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
+  :: BuiltinSemanticsVariant DefaultFun
+  -> MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun)
 defaultCekParametersForVariant = \case
   DefaultFunSemanticsVariantA -> defaultCekParametersA
   DefaultFunSemanticsVariantB -> defaultCekParametersB
@@ -208,7 +207,7 @@ defaultBuiltinsRuntimeForTesting
 -- See Note [noinline for saving on ticks].
 defaultBuiltinsRuntimeForTesting = defaultBuiltinsRuntimeForSemanticsVariant DefaultFunSemanticsVariantC
 
-defaultCekParametersForTesting :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
+defaultCekParametersForTesting :: MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun)
 defaultCekParametersForTesting = defaultCekParametersC
 
 defaultCekMachineCostsForTesting :: CekMachineCosts
@@ -355,7 +354,7 @@ unitCostBuiltinCostModel = BuiltinCostModelBase
     , paramIndexArray                      = unitCostTwoArguments
     }
 
-unitCekParameters :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
+unitCekParameters :: MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun)
 unitCekParameters =
     -- See Note [noinline for saving on ticks].
     MachineParameters def $
diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/MachineParameters/Default.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/MachineParameters/Default.hs
index 82304a21698..e99277663bd 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/MachineParameters/Default.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/MachineParameters/Default.hs
@@ -18,13 +18,13 @@ import GHC.Exts (inline)
 
 -- | The semantics-variant-dependent part of 'MachineParameters'.
 type DefaultMachineVariantParameters =
-    MachineVariantParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ())
+    MachineVariantParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun)
 
 -- | 'MachineParameters' instantiated at CEK-machine-specific types and default builtins.
 -- Encompasses everything we need for evaluating a UPLC program with default builtins using the CEK
 -- machine.
 type DefaultMachineParameters =
-    MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ())
+    MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun)
 
 {- Note [Inlining meanings of builtins]
 It's vitally important to inline the 'toBuiltinMeaning' method of a set of built-in functions as
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek.hs
index 480ccdf8950..36bc79da5d9 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek.hs
@@ -68,7 +68,7 @@ A wrapper around the internal runCek to debruijn input and undebruijn output.
 -}
 runCek
     :: ThrowableBuiltins uni fun
-    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    => MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> ExBudgetMode cost uni fun
     -> EmitterMode uni fun
     -> Term Name uni fun ann
@@ -79,7 +79,7 @@ runCek = Common.runCek runCekDeBruijn
 -- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
 runCekNoEmit
     :: ThrowableBuiltins uni fun
-    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    => MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> ExBudgetMode cost uni fun
     -> Term Name uni fun ann
     -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), cost)
@@ -90,7 +90,7 @@ runCekNoEmit = Common.runCekNoEmit runCekDeBruijn
 evaluateCek
     :: ThrowableBuiltins uni fun
     => EmitterMode uni fun
-    -> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    -> MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> Term Name uni fun ann
     -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), [Text])
 evaluateCek = Common.evaluateCek runCekDeBruijn
@@ -99,7 +99,7 @@ evaluateCek = Common.evaluateCek runCekDeBruijn
 -- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
 evaluateCekNoEmit
     :: ThrowableBuiltins uni fun
-    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    => MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> Term Name uni fun ann
     -> Either (CekEvaluationException Name uni fun) (Term Name uni fun ())
 evaluateCekNoEmit = Common.evaluateCekNoEmit runCekDeBruijn
@@ -108,7 +108,7 @@ evaluateCekNoEmit = Common.evaluateCekNoEmit runCekDeBruijn
 -- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
 readKnownCek
     :: (ThrowableBuiltins uni fun, ReadKnown (Term Name uni fun ()) a)
-    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    => MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> Term Name uni fun ann
     -> Either (CekEvaluationException Name uni fun) a
 readKnownCek = Common.readKnownCek runCekDeBruijn
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 47b3ba3b90b..580c100e63b 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
@@ -60,6 +60,8 @@ module UntypedPlutusCore.Evaluation.Machine.Cek.Internal
     , Slippage
     , defaultSlippage
     , NTerm
+    , forgetAnn
+    , rememberAnn
     , runCekM
     )
 where
@@ -101,10 +103,12 @@ import Data.Semigroup (stimes)
 import Data.Text (Text)
 import Data.Vector qualified as V
 import Data.Word
+import GHC.Exts (Any)
 import GHC.Generics
 import GHC.TypeLits
 import Prettyprinter
 import Universe
+import Unsafe.Coerce (unsafeCoerce)
 
 {- Note [Compilation peculiarities]
 READ THIS BEFORE TOUCHING ANYTHING IN THIS FILE
@@ -163,6 +167,12 @@ this can make a surprisingly large difference.
 -- 'Name' is not necessary but we leave it here for simplicity and debuggability.
 type NTerm uni fun = Term NamedDeBruijn uni fun
 
+forgetAnn :: forall ann uni fun. NTerm uni fun ann -> NTerm uni fun Any
+forgetAnn = unsafeCoerce
+
+rememberAnn :: forall ann uni fun. NTerm uni fun Any -> NTerm uni fun ann
+rememberAnn = unsafeCoerce
+
 data StepKind
     = BConst
     | BVar
@@ -206,24 +216,25 @@ but functions are not printable and hence we provide a dummy instance.
 -}
 
 -- See Note [Show instance for BuiltinRuntime].
-instance Show (BuiltinRuntime (CekValue uni fun ann)) where
+instance Show (BuiltinRuntime (CekValue uni fun)) where
     show _ = "<builtin_runtime>"
 
 -- | A LIFO stack of 'CekValue's, useful for recording multiple arguments which will need to
 -- be pushed onto the context in reverse order.
-data ArgStack uni fun ann =
+data ArgStack uni fun =
   EmptyStack
-  | ConsStack !(CekValue uni fun ann) !(ArgStack uni fun ann)
+  | ConsStack !(CekValue uni fun) !(ArgStack uni fun)
 
-deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
-    => Show (ArgStack uni fun ann)
+instance (GShow uni, Everywhere uni Show, Show fun, Closed uni) => Show (ArgStack uni fun) where
+  show EmptyStack          = "EmptyStack"
+  show (ConsStack val arg) = unwords ["ConsStack", show val, show arg]
 
 -- 'Values' for the modified CEK machine.
-data CekValue uni fun ann =
+data CekValue uni fun =
     -- This bang gave us a 1-2% speed-up at the time of writing.
     VCon !(Some (ValueOf uni))
-  | VDelay !(NTerm uni fun ann) !(CekValEnv uni fun ann)
-  | VLamAbs !NamedDeBruijn !(NTerm uni fun ann) !(CekValEnv uni fun ann)
+  | VDelay !(NTerm uni fun Any) !(CekValEnv uni fun)
+  | VLamAbs !NamedDeBruijn !(NTerm uni fun Any) !(CekValEnv uni fun)
     -- | A partial builtin application, accumulating arguments for eventual full application.
     -- We don't need a 'CekValEnv' here unlike in the other constructors, because 'VBuiltin'
     -- values always store their corresponding 'Term's fully discharged, see the comments at
@@ -242,16 +253,20 @@ data CekValue uni fun ann =
       -- be returned in the result. The laziness is important, because the arguments are discharged
       -- values and discharging is expensive, so we don't want to do it unless we really have
       -- to. Making this field strict resulted in a 3-4.5% slowdown at the time of writing.
-      !(BuiltinRuntime (CekValue uni fun ann))
+      !(BuiltinRuntime (CekValue uni fun))
       -- ^ The partial application and its costing function.
       -- Check the docs of 'BuiltinRuntime' for details.
     -- | A constructor value, including fully computed arguments and the tag.
-  | VConstr {-# UNPACK #-} !Word64 !(ArgStack uni fun ann)
+  | VConstr {-# UNPACK #-} !Word64 !(ArgStack uni fun)
 
-deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
-    => Show (CekValue uni fun ann)
+instance (GShow uni, Everywhere uni Show, Show fun, Closed uni) => Show (CekValue uni fun) where
+  show (VCon val)             = unwords ["VCon", show val]
+  show (VDelay term env)      = unwords ["VDelay", show (() <$ term), show env]
+  show (VLamAbs ndb term env) = unwords ["VLamAbs", show ndb, show (() <$ term), show env]
+  show (VBuiltin f term rt)   = unwords ["VBuiltin ", show f, show (() <$ term), show rt]
+  show (VConstr idx arg)      = unwords ["VConstr", show idx, show arg]
 
-type CekValEnv uni fun ann = Env.RAList (CekValue uni fun ann)
+type CekValEnv uni fun = Env.RAList (CekValue uni fun)
 
 -- | The CEK machine is parameterized over a @spendBudget@ function. This makes the budgeting machinery extensible
 -- and allows us to separate budgeting logic from evaluation logic and avoid branching on the union
@@ -395,7 +410,7 @@ they don't actually take the context as an argument even at the source level.
 -}
 
 -- | Implicit parameter for the builtin runtime.
-type GivenCekRuntime uni fun ann = (?cekRuntime :: BuiltinsRuntime fun (CekValue uni fun ann))
+type GivenCekRuntime uni fun ann = (?cekRuntime :: BuiltinsRuntime fun (CekValue uni fun))
 type GivenCekCaserBuiltin uni = (?cekCaserBuiltin :: CaserBuiltin uni)
 -- | Implicit parameter for the log emitter reference.
 type GivenCekEmitter uni fun s = (?cekEmitter :: CekEmitter uni fun s)
@@ -472,7 +487,7 @@ But in our case this is okay, because:
 throwErrorDischarged
   :: ThrowableBuiltins uni fun
   => EvaluationError (MachineError fun) CekUserError
-  -> CekValue uni fun ann
+  -> CekValue uni fun
   -> CekM uni fun s x
 throwErrorDischarged err = throwErrorWithCause err . dischargeCekValue
 
@@ -536,7 +551,7 @@ instance Pretty CekUserError where
 
 -- | Instantiate all the free variables of a term by looking them up in an environment.
 -- Mutually recursive with dischargeCekVal.
-dischargeCekValEnv :: forall uni fun ann. CekValEnv uni fun ann -> NTerm uni fun () -> NTerm uni fun ()
+dischargeCekValEnv :: forall uni fun. CekValEnv uni fun -> NTerm uni fun () -> NTerm uni fun ()
 dischargeCekValEnv valEnv = go 0
  where
   -- The lamCnt is just a counter that measures how many lambda-abstractions
@@ -563,7 +578,7 @@ dischargeCekValEnv valEnv = go 0
 
 -- | Convert a 'CekValue' into a 'Term' by replacing all bound variables with the terms
 -- they're bound to (which themselves have to be obtain by recursively discharging values).
-dischargeCekValue :: CekValue uni fun ann -> NTerm uni fun ()
+dischargeCekValue :: CekValue uni fun -> NTerm uni fun ()
 dischargeCekValue = \case
     VCon     val                         -> Constant () val
     VDelay   body env                    -> dischargeCekValEnv env $ Delay () (void body)
@@ -583,12 +598,12 @@ dischargeCekValue = \case
         go acc EmptyStack           = acc
         go acc (ConsStack arg rest) = go (arg : acc) rest
 
-instance (PrettyUni uni, Pretty fun) => PrettyBy PrettyConfigPlc (CekValue uni fun ann) where
+instance (PrettyUni uni, Pretty fun) => PrettyBy PrettyConfigPlc (CekValue uni fun) where
     prettyBy cfg = prettyBy cfg . dischargeCekValue
 
-type instance UniOf (CekValue uni fun ann) = uni
+type instance UniOf (CekValue uni fun) = uni
 
-instance HasConstant (CekValue uni fun ann) where
+instance HasConstant (CekValue uni fun) where
     asConstant (VCon val) = pure val
     asConstant _          = throwError notAConstant
     {-# INLINE asConstant #-}
@@ -602,27 +617,27 @@ The context in which the machine operates.
 Morally, this is a stack of frames, but we use the "intrusive list" representation so that
 we can match on context and the top frame in a single, strict pattern match.
 -}
-data Context uni fun ann
-    = FrameAwaitArg !(CekValue uni fun ann) !(Context uni fun ann)
+data Context uni fun
+    = FrameAwaitArg !(CekValue uni fun) !(Context uni fun)
     -- ^ @[V _]@
-    | FrameAwaitFunTerm !(CekValEnv uni fun ann) !(NTerm uni fun ann) !(Context uni fun ann)
+    | FrameAwaitFunTerm !(CekValEnv uni fun) !(NTerm uni fun Any) !(Context uni fun)
     -- ^ @[_ N]@
-    | FrameAwaitFunValue !(CekValue uni fun ann) !(Context uni fun ann)
+    | FrameAwaitFunValue !(CekValue uni fun) !(Context uni fun)
     -- ^ @[_ V]@
-    | FrameForce !(Context uni fun ann)
+    | FrameForce !(Context uni fun)
     -- ^ @(force _)@
     -- See Note [Accumulators for terms]
-    | FrameConstr !(CekValEnv uni fun ann) {-# UNPACK #-} !Word64 ![NTerm uni fun ann] !(ArgStack uni fun ann) !(Context uni fun ann)
+    | FrameConstr !(CekValEnv uni fun) {-# UNPACK #-} !Word64 ![NTerm uni fun Any] !(ArgStack uni fun) !(Context uni fun)
     -- ^ @(constr i V0 ... Vj-1 _ Nj ... Nn)@
-    | FrameCases !(CekValEnv uni fun ann) !(V.Vector (NTerm uni fun ann)) !(Context uni fun ann)
+    | FrameCases !(CekValEnv uni fun) !(V.Vector (NTerm uni fun Any)) !(Context uni fun)
     -- ^ @(case _ C0 .. Cn)@
     | NoFrame
 
-deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
-    => Show (Context uni fun ann)
+-- deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
+--     => Show (Context uni fun)
 
 -- See Note [ExMemoryUsage instances for non-constants].
-instance (Closed uni, uni `Everywhere` ExMemoryUsage) => ExMemoryUsage (CekValue uni fun ann) where
+instance (Closed uni, uni `Everywhere` ExMemoryUsage) => ExMemoryUsage (CekValue uni fun) where
     memoryUsage = \case
         VCon c      -> memoryUsage c
         VDelay {}   -> singletonRose 1
@@ -647,23 +662,23 @@ directly to the head of the application. Which is why 'transferSpine' is a right
 
 -- See Note [ArgStack vs Spine].
 -- | Transfers an 'ArgStack' to a series of 'Context' frames.
-transferArgStack :: ArgStack uni fun ann -> Context uni fun ann -> Context uni fun ann
+transferArgStack :: ArgStack uni fun -> Context uni fun -> Context uni fun
 transferArgStack EmptyStack c           = c
 transferArgStack (ConsStack arg rest) c = transferArgStack rest (FrameAwaitFunValue arg c)
 
 -- See Note [ArgStack vs Spine].
 -- | Transfers a 'Spine' onto the stack. The first argument will be at the top of the stack.
 transferSpine
-    :: Spine (CekValue uni fun ann)
-    -> Context uni fun ann
-    -> Context uni fun ann
+    :: Spine (CekValue uni fun)
+    -> Context uni fun
+    -> Context uni fun
 transferSpine args ctx = foldr FrameAwaitFunValue ctx args
 {-# INLINE transferSpine #-}
 
 runCekM
     :: forall a cost uni fun ann
     . ThrowableBuiltins uni fun
-    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    => MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> ExBudgetMode cost uni fun
     -> EmitterMode uni fun
     -> (forall s. GivenCekReqs uni fun ann s => CekM uni fun s a)
@@ -694,9 +709,9 @@ runCekM
 enterComputeCek
     :: forall uni fun ann s
     . (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s)
-    => Context uni fun ann
-    -> CekValEnv uni fun ann
-    -> NTerm uni fun ann
+    => Context uni fun
+    -> CekValEnv uni fun
+    -> NTerm uni fun Any
     -> CekM uni fun s (NTerm uni fun ())
 enterComputeCek = computeCek
   where
@@ -707,9 +722,9 @@ enterComputeCek = computeCek
     -- 3. throws 'EvaluationFailure' ('Error')
     -- 4. looks up a variable in the environment and calls 'returnCek' ('Var')
     computeCek
-        :: Context uni fun ann
-        -> CekValEnv uni fun ann
-        -> NTerm uni fun ann
+        :: Context uni fun
+        -> CekValEnv uni fun
+        -> NTerm uni fun Any
         -> CekM uni fun s (NTerm uni fun ())
     -- s ; ρ ▻ {L A}  ↦ s , {_ A} ; ρ ▻ L
     computeCek !ctx !env (Var _ varName) = do
@@ -766,8 +781,8 @@ enterComputeCek = computeCek
           stored in the frame to an argument.
     -}
     returnCek
-        :: Context uni fun ann
-        -> CekValue uni fun ann
+        :: Context uni fun
+        -> CekValue uni fun
         -> CekM uni fun s (NTerm uni fun ())
     --- Instantiate all the free variable of the resulting term in case there are any.
     -- . ◅ V           ↦  [] V
@@ -812,8 +827,8 @@ enterComputeCek = computeCek
     -- | Evaluate a 'HeadSpine' by pushing the arguments (if any) onto the stack and proceeding with
     -- the returning phase of the CEK machine.
     returnCekHeadSpine
-        :: Context uni fun ann
-        -> HeadSpine (CekValue uni fun ann)
+        :: Context uni fun
+        -> HeadSpine (CekValue uni fun)
         -> CekM uni fun s (Term NamedDeBruijn uni fun ())
     returnCekHeadSpine ctx (HeadOnly  x)    = returnCek ctx x
     returnCekHeadSpine ctx (HeadSpine f xs) = returnCek (transferSpine xs ctx) f
@@ -825,8 +840,8 @@ enterComputeCek = computeCek
     -- representation depending on whether the application is saturated or not,
     -- if v is anything else, fail.
     forceEvaluate
-        :: Context uni fun ann
-        -> CekValue uni fun ann
+        :: Context uni fun
+        -> CekValue uni fun
         -> CekM uni fun s (NTerm uni fun ())
     forceEvaluate !ctx (VDelay body env) = computeCek ctx env body
     forceEvaluate !ctx (VBuiltin fun term runtime) = do
@@ -853,9 +868,9 @@ enterComputeCek = computeCek
     -- representation depending on whether the application is saturated or not.
     -- If v is anything else, fail.
     applyEvaluate
-        :: Context uni fun ann
-        -> CekValue uni fun ann   -- lhs of application
-        -> CekValue uni fun ann   -- rhs of application
+        :: Context uni fun
+        -> CekValue uni fun   -- lhs of application
+        -> CekValue uni fun   -- rhs of application
         -> CekM uni fun s (NTerm uni fun ())
     applyEvaluate !ctx (VLamAbs _ body env) arg =
         computeCek ctx (Env.cons arg env) body
@@ -918,10 +933,10 @@ enterComputeCek = computeCek
     --
     -- and proceed with the returning phase of the CEK machine.
     evalBuiltinApp
-        :: Context uni fun ann
+        :: Context uni fun
         -> fun
         -> NTerm uni fun ()
-        -> BuiltinRuntime (CekValue uni fun ann)
+        -> BuiltinRuntime (CekValue uni fun)
         -> CekM uni fun s (Term NamedDeBruijn uni fun ())
     evalBuiltinApp ctx fun term runtime = case runtime of
         BuiltinCostedResult budgets0 getFXs -> do
@@ -947,7 +962,7 @@ enterComputeCek = computeCek
     {-# INLINE spendBudget #-}
 
     -- | Look up a variable name in the environment.
-    lookupVarName :: NamedDeBruijn -> CekValEnv uni fun ann -> CekM uni fun s (CekValue uni fun ann)
+    lookupVarName :: NamedDeBruijn -> CekValEnv uni fun -> CekM uni fun s (CekValue uni fun)
     lookupVarName varName@(NamedDeBruijn _ varIx) varEnv =
         Env.contIndexOne
             (throwErrorWithCause (StructuralError OpenTermEvaluatedMachineError) $ Var () varName)
@@ -960,7 +975,7 @@ enterComputeCek = computeCek
 -- | Evaluate a term using the CEK machine and keep track of costing, logging is optional.
 runCekDeBruijn
     :: ThrowableBuiltins uni fun
-    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    => MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> ExBudgetMode cost uni fun
     -> EmitterMode uni fun
     -> NTerm uni fun ann
@@ -968,7 +983,7 @@ runCekDeBruijn
 runCekDeBruijn params mode emitMode term =
     runCekM params mode emitMode $ do
         unCekBudgetSpender ?cekBudgetSpender BStartup $ runIdentity $ cekStartupCost ?cekCosts
-        enterComputeCek NoFrame Env.empty term
+        enterComputeCek NoFrame Env.empty (forgetAnn term)
 
 {- Note [Accumulators for terms]
 At a couple of points in the CEK machine (notably building the arguments to a constructor value)
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/CommonAPI.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/CommonAPI.hs
index 1f5b10a9c94..a1376453267 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/CommonAPI.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/CommonAPI.hs
@@ -71,7 +71,7 @@ import Data.Text (Text)
 
 -- The type of the machine (runner function).
 type MachineRunner cost uni fun ann =
-      MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+      MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> ExBudgetMode cost uni fun
     -> EmitterMode uni fun
     -> NTerm uni fun ann
@@ -94,7 +94,7 @@ A wrapper around the internal runCek to debruijn input and undebruijn output.
 -}
 runCek ::
       MachineRunner cost uni fun ann
-    -> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    -> MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> ExBudgetMode cost uni fun
     -> EmitterMode uni fun
     -> Term Name uni fun ann
@@ -125,7 +125,7 @@ runCek runner params mode emitMode term =
 -- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
 runCekNoEmit ::
       MachineRunner cost uni fun ann
-    -> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    -> MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> ExBudgetMode cost uni fun
     -> Term Name uni fun ann
     -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), cost)
@@ -139,7 +139,7 @@ evaluateCek
     :: ThrowableBuiltins uni fun
     => MachineRunner RestrictingSt uni fun ann
     -> EmitterMode uni fun
-    -> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    -> MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> Term Name uni fun ann
     -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), [Text])
 evaluateCek runner emitMode params =
@@ -151,7 +151,7 @@ evaluateCek runner emitMode params =
 evaluateCekNoEmit
     :: ThrowableBuiltins uni fun
     => MachineRunner RestrictingSt uni fun ann
-    -> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    -> MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> Term Name uni fun ann
     -> Either (CekEvaluationException Name uni fun) (Term Name uni fun ())
 evaluateCekNoEmit runner params = fst . runCekNoEmit runner params restrictingEnormous
@@ -161,7 +161,7 @@ evaluateCekNoEmit runner params = fst . runCekNoEmit runner params restrictingEn
 readKnownCek
     :: (ThrowableBuiltins uni fun, ReadKnown (Term Name uni fun ()) a)
     => MachineRunner RestrictingSt uni fun ann
-    -> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    -> MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> Term Name uni fun ann
     -> Either (CekEvaluationException Name uni fun) a
 readKnownCek runner params = evaluateCekNoEmit runner params >=> readKnownSelf
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/SteppableCek.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/SteppableCek.hs
index 5f68a18e624..9f8f6ec8fce 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/SteppableCek.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/SteppableCek.hs
@@ -65,7 +65,7 @@ A wrapper around the internal runCek to debruijn input and undebruijn output.
 -}
 runCek
     :: ThrowableBuiltins uni fun
-    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    => MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> ExBudgetMode cost uni fun
     -> EmitterMode uni fun
     -> Term Name uni fun ann
@@ -77,7 +77,7 @@ runCek = Common.runCek S.runCekDeBruijn
 -- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
 runCekNoEmit
     :: ThrowableBuiltins uni fun
-    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    => MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> ExBudgetMode cost uni fun
     -> Term Name uni fun ann
     -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), cost)
@@ -88,7 +88,7 @@ runCekNoEmit = Common.runCekNoEmit S.runCekDeBruijn
 evaluateCek
     :: ThrowableBuiltins uni fun
     => EmitterMode uni fun
-    -> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    -> MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> Term Name uni fun ann
     -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), [Text])
 evaluateCek = Common.evaluateCek S.runCekDeBruijn
@@ -97,7 +97,7 @@ evaluateCek = Common.evaluateCek S.runCekDeBruijn
 -- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
 evaluateCekNoEmit
     :: ThrowableBuiltins uni fun
-    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    => MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> Term Name uni fun ann
     -> Either (CekEvaluationException Name uni fun) (Term Name uni fun ())
 evaluateCekNoEmit = Common.evaluateCekNoEmit S.runCekDeBruijn
@@ -106,7 +106,7 @@ evaluateCekNoEmit = Common.evaluateCekNoEmit S.runCekDeBruijn
 -- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
 readKnownCek
     :: (ThrowableBuiltins uni fun, ReadKnown (Term Name uni fun ()) a)
-    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    => MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> Term Name uni fun ann
     -> Either (CekEvaluationException Name uni fun) a
 readKnownCek = Common.readKnownCek S.runCekDeBruijn
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/SteppableCek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/SteppableCek/Internal.hs
index d61a028a917..f2cd0fbc89d 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/SteppableCek/Internal.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/SteppableCek/Internal.hs
@@ -63,6 +63,7 @@ import Data.Semigroup (stimes)
 import Data.Text (Text)
 import Data.Vector qualified as V
 import Data.Word (Word64)
+import GHC.Exts (Any)
 import GHC.TypeNats
 import Universe
 
@@ -80,9 +81,9 @@ data CekState uni fun ann =
     -- loaded a term but not fired the cek yet
     Starting (NTerm uni fun ann)
     -- the next state is computing
-    | Computing (Context uni fun ann) (CekValEnv uni fun ann) (NTerm uni fun ann)
+    | Computing (Context uni fun ann) (CekValEnv uni fun) (NTerm uni fun Any)
     -- the next state is returning
-    | Returning (Context uni fun ann) (CekValue uni fun ann)
+    | Returning (Context uni fun ann) (CekValue uni fun)
     -- evaluation finished
     | Terminating (NTerm uni fun ())
 
@@ -95,33 +96,33 @@ instance Pretty (CekState uni fun ann) where
 
 -- | Similar to 'Cek.Internal.Context', but augmented with an 'ann'
 data Context uni fun ann
-    = FrameAwaitArg ann !(CekValue uni fun ann) !(Context uni fun ann)                         -- ^ @[V _]@
-    | FrameAwaitFunTerm ann !(CekValEnv uni fun ann) !(NTerm uni fun ann) !(Context uni fun ann) -- ^ @[_ N]@
-    | FrameAwaitFunValue ann !(CekValue uni fun ann) !(Context uni fun ann)
+    = FrameAwaitArg ann !(CekValue uni fun) !(Context uni fun ann)                         -- ^ @[V _]@
+    | FrameAwaitFunTerm ann !(CekValEnv uni fun) !(NTerm uni fun ann) !(Context uni fun ann) -- ^ @[_ N]@
+    | FrameAwaitFunValue ann !(CekValue uni fun) !(Context uni fun ann)
     | FrameForce ann !(Context uni fun ann)                                               -- ^ @(force _)@
-    | FrameConstr ann !(CekValEnv uni fun ann) {-# UNPACK #-} !Word64 ![NTerm uni fun ann] !(ArgStack uni fun ann) !(Context uni fun ann)
-    | FrameCases ann !(CekValEnv uni fun ann) !(V.Vector (NTerm uni fun ann)) !(Context uni fun ann)
+    | FrameConstr ann !(CekValEnv uni fun) {-# UNPACK #-} !Word64 ![NTerm uni fun ann] !(ArgStack uni fun) !(Context uni fun ann)
+    | FrameCases ann !(CekValEnv uni fun) !(V.Vector (NTerm uni fun ann)) !(Context uni fun ann)
     | NoFrame
 
 deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
     => Show (Context uni fun ann)
 
 -- | Transfers an 'ArgStack' to a series of 'Context' frames.
-transferArgStack :: ann -> ArgStack uni fun ann -> Context uni fun ann -> Context uni fun ann
+transferArgStack :: ann -> ArgStack uni fun -> Context uni fun ann -> Context uni fun ann
 transferArgStack ann = go
   where
     go EmptyStack c           = c
     go (ConsStack arg rest) c = go rest (FrameAwaitFunValue ann arg c)
 
 -- | Transfers a 'Spine' onto the stack. The first argument will be at the top of the stack.
-transferSpine :: ann -> Spine (CekValue uni fun ann) -> Context uni fun ann -> Context uni fun ann
+transferSpine :: ann -> Spine (CekValue uni fun) -> Context uni fun ann -> Context uni fun ann
 transferSpine ann args ctx = foldr (FrameAwaitFunValue ann) ctx args
 
 computeCek
     :: forall uni fun ann s
     . (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s)
     => Context uni fun ann
-    -> CekValEnv uni fun ann
+    -> CekValEnv uni fun
     -> NTerm uni fun ann
     -> CekM uni fun s (CekState uni fun ann)
 -- s ; ρ ▻ {L A}  ↦ s , {_ A} ; ρ ▻ L
@@ -134,18 +135,18 @@ computeCek !ctx !_ (Constant _ val) = do
     pure $ Returning ctx (VCon val)
 computeCek !ctx !env (LamAbs _ name body) = do
     stepAndMaybeSpend BLamAbs
-    pure $ Returning ctx (VLamAbs name body env)
+    pure $ Returning ctx (VLamAbs name (forgetAnn body) env)
 computeCek !ctx !env (Delay _ body) = do
     stepAndMaybeSpend BDelay
-    pure $ Returning ctx (VDelay body env)
+    pure $ Returning ctx (VDelay (forgetAnn body) env)
 -- s ; ρ ▻ lam x L  ↦  s ◅ lam x (L , ρ)
 computeCek !ctx !env (Force _ body) = do
     stepAndMaybeSpend BForce
-    pure $ Computing (FrameForce (termAnn body) ctx) env body
+    pure $ Computing (FrameForce (termAnn body) ctx) env (forgetAnn body)
 -- s ; ρ ▻ [L M]  ↦  s , [_ (M,ρ)]  ; ρ ▻ L
 computeCek !ctx !env (Apply _ fun arg) = do
     stepAndMaybeSpend BApply
-    pure $ Computing (FrameAwaitFunTerm (termAnn fun) env arg ctx) env fun
+    pure $ Computing (FrameAwaitFunTerm (termAnn fun) env arg ctx) env (forgetAnn fun)
 -- s ; ρ ▻ abs α L  ↦  s ◅ abs α (L , ρ)
 -- s ; ρ ▻ con c  ↦  s ◅ con c
 -- s ; ρ ▻ builtin bn  ↦  s ◅ builtin bn arity arity [] [] ρ
@@ -158,12 +159,12 @@ computeCek !ctx !_ (Builtin _ bn) = do
 computeCek !ctx !env (Constr ann i es) = do
     stepAndMaybeSpend BConstr
     pure $ case es of
-        (t : rest) -> Computing (FrameConstr ann env i rest EmptyStack ctx) env t
+        (t : rest) -> Computing (FrameConstr ann env i rest EmptyStack ctx) env (forgetAnn t)
         []         -> Returning ctx $ VConstr i EmptyStack
 -- s ; ρ ▻ case S C0 ... Cn  ↦  s , case _ (C0 ... Cn, ρ) ; ρ ▻ S
 computeCek !ctx !env (Case ann scrut cs) = do
     stepAndMaybeSpend BCase
-    pure $ Computing (FrameCases ann env cs ctx) env scrut
+    pure $ Computing (FrameCases ann env cs ctx) env (forgetAnn scrut)
 -- s ; ρ ▻ error A  ↦  <> A
 computeCek !_ !_ (Error _) =
     throwErrorWithCause (OperationalError CekEvaluationFailure) (Error ())
@@ -172,7 +173,7 @@ returnCek
     :: forall uni fun ann s
     . (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s)
     => Context uni fun ann
-    -> CekValue uni fun ann
+    -> CekValue uni fun
     -> CekM uni fun s (CekState uni fun ann)
 --- Instantiate all the free variable of the resulting term in case there are any.
 -- . ◅ V           ↦  [] V
@@ -184,7 +185,7 @@ returnCek (FrameForce ann ctx) fun = forceEvaluate ann ctx fun
 -- s , [_ (M,ρ)] ◅ V  ↦  s , [V _] ; ρ ▻ M
 returnCek (FrameAwaitFunTerm _funAnn argVarEnv arg ctx) fun =
     -- MAYBE: perhaps it is worth here to merge the _funAnn with argAnn
-    pure $ Computing (FrameAwaitArg (termAnn arg) fun ctx) argVarEnv arg
+    pure $ Computing (FrameAwaitArg (termAnn arg) fun ctx) argVarEnv (forgetAnn arg)
 -- s , [(lam x (M,ρ)) _] ◅ V  ↦  s ; ρ [ x  ↦  V ] ▻ M
 -- FIXME: add rule for VBuiltin once it's in the specification.
 returnCek (FrameAwaitArg ann fun ctx) arg =
@@ -213,7 +214,7 @@ returnCek (FrameCases ann env cs ctx) e = case e of
         Nothing -> throwErrorDischarged (StructuralError $ MissingCaseBranchMachineError i) e
     VCon val -> case unCaserBuiltin ?cekCaserBuiltin val cs of
         Left err  -> throwErrorDischarged (OperationalError $ CekCaseBuiltinError err) e
-        Right res -> pure $ Computing ctx env res
+        Right res -> pure $ Computing ctx env (forgetAnn res)
     _ -> throwErrorDischarged (StructuralError NonConstrScrutinizedMachineError) e
 
 -- | @force@ a term and proceed.
@@ -227,7 +228,7 @@ forceEvaluate
     . (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s)
     => ann
     -> Context uni fun ann
-    -> CekValue uni fun ann
+    -> CekValue uni fun
     -> CekM uni fun s (CekState uni fun ann)
 forceEvaluate _ !ctx (VDelay body env) =
     pure $ Computing ctx env body
@@ -259,8 +260,8 @@ applyEvaluate
     . (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s)
     => ann
     -> Context uni fun ann
-    -> CekValue uni fun ann   -- lhs of application
-    -> CekValue uni fun ann   -- rhs of application
+    -> CekValue uni fun   -- lhs of application
+    -> CekValue uni fun   -- rhs of application
     -> CekM uni fun s (CekState uni fun ann)
 applyEvaluate _ !ctx (VLamAbs _ body env) arg =
     pure $ Computing ctx (Env.cons arg env) body
@@ -283,7 +284,7 @@ applyEvaluate _ !_ val _ =
 -- MAYBE: runCekDeBruijn can be shared between original&debug ceks by passing a `enterComputeCek` func.
 runCekDeBruijn
     :: ThrowableBuiltins uni fun
-    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    => MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> ExBudgetMode cost uni fun
     -> EmitterMode uni fun
     -> NTerm uni fun ann
@@ -299,10 +300,10 @@ enterComputeCek
     :: forall uni fun ann s
     . (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s)
     => Context uni fun ann
-    -> CekValEnv uni fun ann
+    -> CekValEnv uni fun
     -> NTerm uni fun ann
     -> CekM uni fun s (NTerm uni fun ())
-enterComputeCek ctx env term = iterToFinalState $ Computing ctx env term
+enterComputeCek ctx env term = iterToFinalState $ Computing ctx env (forgetAnn term)
  where
    iterToFinalState :: CekState uni fun ann -> CekM uni fun s (NTerm uni fun ())
    iterToFinalState = cekTrans
@@ -328,8 +329,8 @@ cekTrans :: forall uni fun ann s
            . (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s)
            => CekTrans uni fun ann s
 cekTrans = \case
-    Starting term          -> pure $ Computing NoFrame Env.empty term
-    Computing ctx env term -> computeCek ctx env term
+    Starting term          -> pure $ Computing NoFrame Env.empty (forgetAnn term)
+    Computing ctx env term -> computeCek ctx env (rememberAnn term)
     Returning ctx val      -> returnCek ctx val
     self@Terminating{}     -> pure self -- FINAL STATE, idempotent
 
@@ -340,7 +341,7 @@ mkCekTrans
     :: forall cost uni fun ann m s
     . ( ThrowableBuiltins uni fun
       , PrimMonad m, s ~ PrimState m) -- the outer monad that initializes the transition function
-    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
+    => MachineParameters CekMachineCosts fun (CekValue uni fun)
     -> ExBudgetMode cost uni fun
     -> EmitterMode uni fun
     -> Slippage
@@ -379,7 +380,7 @@ cekStateContext f = \case
 
 cekStateAnn :: CekState uni fun ann -> Maybe ann
 cekStateAnn = \case
-    Computing _ _ t -> pure $ termAnn t
+    Computing _ _ t -> pure $ termAnn $ rememberAnn t
     Returning ctx _ -> contextAnn ctx
     _               -> empty
 
@@ -428,15 +429,15 @@ cekStepCost costs = runIdentity . \case
 throwErrorDischarged
   :: ThrowableBuiltins uni fun
   => EvaluationError (MachineError fun) CekUserError
-  -> CekValue uni fun ann
+  -> CekValue uni fun
   -> CekM uni fun s x
 throwErrorDischarged err = throwErrorWithCause err . dischargeCekValue
 
 -- | Look up a variable name in the environment.
 lookupVarName
-    :: forall uni fun ann s .
+    :: forall uni fun s .
        ThrowableBuiltins uni fun
-    => NamedDeBruijn -> CekValEnv uni fun ann -> CekM uni fun s (CekValue uni fun ann)
+    => NamedDeBruijn -> CekValEnv uni fun -> CekM uni fun s (CekValue uni fun)
 lookupVarName varName@(NamedDeBruijn _ varIx) varEnv =
     case varEnv `Env.indexOne` coerce varIx of
         Nothing  ->
@@ -448,7 +449,7 @@ lookupVarName varName@(NamedDeBruijn _ varIx) varEnv =
 returnCekHeadSpine
     :: ann
     -> Context uni fun ann
-    -> HeadSpine (CekValue uni fun ann)
+    -> HeadSpine (CekValue uni fun)
     -> CekM uni fun s (CekState uni fun ann)
 returnCekHeadSpine _   ctx (HeadOnly  x)    = pure $ Returning ctx x
 returnCekHeadSpine ann ctx (HeadSpine f xs) = pure $ Returning (transferSpine ann xs ctx) f
@@ -466,7 +467,7 @@ evalBuiltinApp
     -> Context uni fun ann
     -> fun
     -> NTerm uni fun ()
-    -> BuiltinRuntime (CekValue uni fun ann)
+    -> BuiltinRuntime (CekValue uni fun)
     -> CekM uni fun s (CekState uni fun ann)
 evalBuiltinApp ann ctx fun term runtime = case runtime of
     BuiltinCostedResult budgets0 getFXs -> do
diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Common.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Common.hs
index 81e24c98227..96400bf1ba6 100644
--- a/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Common.hs
+++ b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Common.hs
@@ -63,7 +63,7 @@ typecheckAnd
        , CaseBuiltin uni, Closed uni, uni `Everywhere` ExMemoryUsage
        )
     => BuiltinSemanticsVariant fun
-    -> (MachineParameters CekMachineCosts fun (CekValue uni fun ()) ->
+    -> (MachineParameters CekMachineCosts fun (CekValue uni fun) ->
             UPLC.Term Name uni fun () -> a)
     -> CostingPart uni fun -> TPLC.Term TyName Name uni fun () -> m a
 typecheckAnd semvar action costingPart term = TPLC.runQuoteT $ do
@@ -195,5 +195,3 @@ evalOkEq t1 t2 =
 
 evalOkTrue :: PlcTerm -> Property
 evalOkTrue t = evalOkEq t true
-
-
diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs
index b38ecd8561b..f2225eb1362 100644
--- a/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs
+++ b/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs
@@ -58,7 +58,7 @@ testDischargeFree = testGroup "discharge" $ fmap (uncurry testCase)
   where
     freeRemains1 =
         -- dis( empty |- (delay (\x ->var0)) ) === (delay (\x -> var0))
-        dis (VDelay (toFakeTerm fun0var0)
+        dis (VDelay (forgetAnn $ toFakeTerm fun0var0)
             []) -- empty env
         @?=
         toFakeTerm (Delay () fun0var0)
@@ -69,7 +69,7 @@ testDischargeFree = testGroup "discharge" $ fmap (uncurry testCase)
         -- y is discharged from the env
         -- var0 is free so it is left alone
         dis (VLamAbs (fakeNameDeBruijn $ DeBruijn deBruijnInitIndex)
-                (toFakeTerm $
+                (forgetAnn $ toFakeTerm $
                  v 1 @@ -- x
                  [v 2 -- y
                  ,var0 -- free
diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/Machines.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/Machines.hs
index 1898d740735..f84b35a6967 100644
--- a/plutus-core/untyped-plutus-core/testlib/Evaluation/Machines.hs
+++ b/plutus-core/untyped-plutus-core/testlib/Evaluation/Machines.hs
@@ -70,7 +70,7 @@ test_machines =
 
 testBudget
     :: (Ix fun, Show fun, Hashable fun, Pretty fun, Typeable fun)
-    => BuiltinsRuntime fun (CekValue DefaultUni fun ())
+    => BuiltinsRuntime fun (CekValue DefaultUni fun)
     -> TestName
     -> Term Name DefaultUni fun ()
     -> TestNested