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 9fd9f29796e..0a709c884b3 100644
--- a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix
+++ b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix
@@ -86,7 +86,6 @@
           (hsPkgs."serialise" or (errorHandler.buildDepError "serialise"))
           (hsPkgs."size-based" or (errorHandler.buildDepError "size-based"))
           (hsPkgs."some" or (errorHandler.buildDepError "some"))
-          (hsPkgs."sop-core" or (errorHandler.buildDepError "sop-core"))
           (hsPkgs."tasty" or (errorHandler.buildDepError "tasty"))
           (hsPkgs."tasty-golden" or (errorHandler.buildDepError "tasty-golden"))
           (hsPkgs."tasty-hedgehog" or (errorHandler.buildDepError "tasty-hedgehog"))
diff --git a/nix/pkgs/haskell/materialized-darwin/default.nix b/nix/pkgs/haskell/materialized-darwin/default.nix
index 0f5e07a9b6c..4306eb4ff51 100644
--- a/nix/pkgs/haskell/materialized-darwin/default.nix
+++ b/nix/pkgs/haskell/materialized-darwin/default.nix
@@ -184,7 +184,6 @@
         "charset".revision = (((hackage."charset")."0.3.9").revisions).default;
         "unix".revision = (((hackage."unix")."2.7.2.2").revisions).default;
         "dependent-sum-template".revision = (((hackage."dependent-sum-template")."0.1.0.3").revisions).default;
-        "sop-core".revision = (((hackage."sop-core")."0.5.0.1").revisions).default;
         "data-fix".revision = (((hackage."data-fix")."0.3.2").revisions).default;
         "dense-linear-algebra".revision = (((hackage."dense-linear-algebra")."0.1.0.0").revisions).default;
         "contravariant".revision = (((hackage."contravariant")."1.5.5").revisions).default;
@@ -774,7 +773,6 @@
           "case-insensitive".components.library.planned = lib.mkOverride 900 true;
           "data-fix".components.library.planned = lib.mkOverride 900 true;
           "dependent-sum-template".components.library.planned = lib.mkOverride 900 true;
-          "sop-core".components.library.planned = lib.mkOverride 900 true;
           "text-short".components.library.planned = lib.mkOverride 900 true;
           "plutus-tx".components.library.planned = lib.mkOverride 900 true;
           "wcwidth".components.library.planned = lib.mkOverride 900 true;
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 9fd9f29796e..0a709c884b3 100644
--- a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix
+++ b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix
@@ -86,7 +86,6 @@
           (hsPkgs."serialise" or (errorHandler.buildDepError "serialise"))
           (hsPkgs."size-based" or (errorHandler.buildDepError "size-based"))
           (hsPkgs."some" or (errorHandler.buildDepError "some"))
-          (hsPkgs."sop-core" or (errorHandler.buildDepError "sop-core"))
           (hsPkgs."tasty" or (errorHandler.buildDepError "tasty"))
           (hsPkgs."tasty-golden" or (errorHandler.buildDepError "tasty-golden"))
           (hsPkgs."tasty-hedgehog" or (errorHandler.buildDepError "tasty-hedgehog"))
diff --git a/nix/pkgs/haskell/materialized-linux/default.nix b/nix/pkgs/haskell/materialized-linux/default.nix
index 0f5e07a9b6c..4306eb4ff51 100644
--- a/nix/pkgs/haskell/materialized-linux/default.nix
+++ b/nix/pkgs/haskell/materialized-linux/default.nix
@@ -184,7 +184,6 @@
         "charset".revision = (((hackage."charset")."0.3.9").revisions).default;
         "unix".revision = (((hackage."unix")."2.7.2.2").revisions).default;
         "dependent-sum-template".revision = (((hackage."dependent-sum-template")."0.1.0.3").revisions).default;
-        "sop-core".revision = (((hackage."sop-core")."0.5.0.1").revisions).default;
         "data-fix".revision = (((hackage."data-fix")."0.3.2").revisions).default;
         "dense-linear-algebra".revision = (((hackage."dense-linear-algebra")."0.1.0.0").revisions).default;
         "contravariant".revision = (((hackage."contravariant")."1.5.5").revisions).default;
@@ -774,7 +773,6 @@
           "case-insensitive".components.library.planned = lib.mkOverride 900 true;
           "data-fix".components.library.planned = lib.mkOverride 900 true;
           "dependent-sum-template".components.library.planned = lib.mkOverride 900 true;
-          "sop-core".components.library.planned = lib.mkOverride 900 true;
           "text-short".components.library.planned = lib.mkOverride 900 true;
           "plutus-tx".components.library.planned = lib.mkOverride 900 true;
           "wcwidth".components.library.planned = lib.mkOverride 900 true;
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 9fd9f29796e..0a709c884b3 100644
--- a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix
+++ b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix
@@ -86,7 +86,6 @@
           (hsPkgs."serialise" or (errorHandler.buildDepError "serialise"))
           (hsPkgs."size-based" or (errorHandler.buildDepError "size-based"))
           (hsPkgs."some" or (errorHandler.buildDepError "some"))
-          (hsPkgs."sop-core" or (errorHandler.buildDepError "sop-core"))
           (hsPkgs."tasty" or (errorHandler.buildDepError "tasty"))
           (hsPkgs."tasty-golden" or (errorHandler.buildDepError "tasty-golden"))
           (hsPkgs."tasty-hedgehog" or (errorHandler.buildDepError "tasty-hedgehog"))
diff --git a/nix/pkgs/haskell/materialized-windows/default.nix b/nix/pkgs/haskell/materialized-windows/default.nix
index 7ae285ff310..9227d896e8a 100644
--- a/nix/pkgs/haskell/materialized-windows/default.nix
+++ b/nix/pkgs/haskell/materialized-windows/default.nix
@@ -181,7 +181,6 @@
         "ieee754".revision = (((hackage."ieee754")."0.8.0").revisions).default;
         "charset".revision = (((hackage."charset")."0.3.9").revisions).default;
         "dependent-sum-template".revision = (((hackage."dependent-sum-template")."0.1.0.3").revisions).default;
-        "sop-core".revision = (((hackage."sop-core")."0.5.0.1").revisions).default;
         "data-fix".revision = (((hackage."data-fix")."0.3.2").revisions).default;
         "dense-linear-algebra".revision = (((hackage."dense-linear-algebra")."0.1.0.0").revisions).default;
         "contravariant".revision = (((hackage."contravariant")."1.5.5").revisions).default;
@@ -751,7 +750,6 @@
           "case-insensitive".components.library.planned = lib.mkOverride 900 true;
           "data-fix".components.library.planned = lib.mkOverride 900 true;
           "dependent-sum-template".components.library.planned = lib.mkOverride 900 true;
-          "sop-core".components.library.planned = lib.mkOverride 900 true;
           "text-short".components.library.planned = lib.mkOverride 900 true;
           "plutus-tx".components.library.planned = lib.mkOverride 900 true;
           "fail".components.library.planned = lib.mkOverride 900 true;
diff --git a/plutus-core/plutus-core.cabal b/plutus-core/plutus-core.cabal
index 1ed9b6e6c3c..1b2872d92a9 100644
--- a/plutus-core/plutus-core.cabal
+++ b/plutus-core/plutus-core.cabal
@@ -304,7 +304,6 @@ library
         serialise -any,
         size-based -any,
         some < 1.0.3,
-        sop-core -any,
         tasty -any,
         tasty-golden -any,
         tasty-hedgehog -any,
diff --git a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
index 58a05af936f..89e2d592942 100644
--- a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
+++ b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
@@ -102,6 +102,8 @@ data ExtensionFun
     | ExpensiveSucc
     | FailingPlus
     | ExpensivePlus
+    | UnsafeCoerce
+    | UnsafeCoerceEl
     | Undefined
     | Absurd
     | ErrorPrime  -- Like 'Error', but a builtin. What do we even need 'Error' for at this point?
@@ -132,6 +134,7 @@ defBuiltinsRuntimeExt = toBuiltinsRuntime (defaultBuiltinCostModel, ())
 
 data PlcListRep (a :: GHC.Type)
 instance KnownTypeAst uni a => KnownTypeAst uni (PlcListRep a) where
+    type ToHoles (PlcListRep a) = '[RepHole a]
     type ToBinds (PlcListRep a) = ToBinds a
 
     toTypeAst _ = TyApp () Plc.listTy . toTypeAst $ Proxy @a
@@ -179,25 +182,18 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni ExtensionFun where
 
     toBuiltinMeaning IdFInteger =
         makeBuiltinMeaning
-            (Prelude.id
-                :: a ~ Opaque term (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)
-                => a -> a)
+            (Prelude.id :: fi ~ Opaque term (TyAppRep f Integer) => fi -> fi)
             (\_ _ -> ExBudget 1 0)
 
     toBuiltinMeaning IdList =
         makeBuiltinMeaning
-            (Prelude.id
-                :: a ~ Opaque term (PlcListRep (TyVarRep ('TyNameRep "a" 0)))
-                => a -> a)
+            (Prelude.id :: la ~ Opaque term (PlcListRep a) => la -> la)
             (\_ _ -> ExBudget 1 0)
 
     toBuiltinMeaning IdRank2 =
         makeBuiltinMeaning
             (Prelude.id
-                :: ( f ~ 'TyNameRep "f" 0
-                   , a ~ 'TyNameRep @GHC.Type "a" 1
-                   , afa ~ Opaque term (TyForallRep a (TyAppRep (TyVarRep f) (TyVarRep a)))
-                   )
+                :: afa ~ Opaque term (TyForallRep a (TyAppRep (TyVarRep f) (TyVarRep a)))
                 => afa -> afa)
             (\_ _ -> ExBudget 1 0)
 
@@ -225,6 +221,23 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni ExtensionFun where
             (\_ _ -> throw BuiltinErrorCall)
             (\_ _ _ -> unExRestrictingBudget enormousBudget)
 
+    toBuiltinMeaning UnsafeCoerce =
+        makeBuiltinMeaning
+            (Opaque . unOpaque)
+            (\_ _ -> ExBudget 1 0)
+
+    toBuiltinMeaning UnsafeCoerceEl =
+        makeBuiltinMeaning
+            unsafeCoerceElPlc
+            (\_ _ -> ExBudget 1 0)
+      where
+        unsafeCoerceElPlc
+            :: SomeConstant DefaultUni [a]
+            -> EvaluationResult (SomeConstant DefaultUni [b])
+        unsafeCoerceElPlc (SomeConstant (Some (ValueOf uniList xs))) = do
+            DefaultUniList _ <- pure uniList
+            pure . SomeConstant $ someValueOf uniList xs
+
     toBuiltinMeaning Undefined =
         makeBuiltinMeaning
             undefined
@@ -244,40 +257,39 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni ExtensionFun where
         commaPlc
             :: SomeConstant uni a
             -> SomeConstant uni b
-            -> SomeConstantPoly uni (,) '[a, b]
+            -> SomeConstant uni (a, b)
         commaPlc (SomeConstant (Some (ValueOf uniA x))) (SomeConstant (Some (ValueOf uniB y))) =
-            SomeConstantPoly $ someValueOf (DefaultUniPair uniA uniB) (x, y)
+            SomeConstant $ someValueOf (DefaultUniPair uniA uniB) (x, y)
 
     toBuiltinMeaning BiconstPair = makeBuiltinMeaning biconstPairPlc mempty where
         biconstPairPlc
             :: SomeConstant uni a
             -> SomeConstant uni b
-            -> SomeConstantPoly uni (,) '[a, b]
-            -> EvaluationResult (SomeConstantPoly uni (,) '[a, b])
+            -> SomeConstant uni (a, b)
+            -> EvaluationResult (SomeConstant uni (a, b))
         biconstPairPlc
             (SomeConstant (Some (ValueOf uniA x)))
             (SomeConstant (Some (ValueOf uniB y)))
-            (SomeConstantPoly (Some (ValueOf uniPairAB _))) = do
+            (SomeConstant (Some (ValueOf uniPairAB _))) = do
                 DefaultUniPair uniA' uniB' <- pure uniPairAB
                 Just Refl <- pure $ uniA `geq` uniA'
                 Just Refl <- pure $ uniB `geq` uniB'
-                pure . SomeConstantPoly $ someValueOf uniPairAB (x, y)
+                pure . SomeConstant $ someValueOf uniPairAB (x, y)
 
     toBuiltinMeaning Swap = makeBuiltinMeaning swapPlc mempty where
         swapPlc
-            :: SomeConstantPoly uni (,) '[a, b]
-            -> EvaluationResult (SomeConstantPoly uni (,) '[b, a])
-        swapPlc (SomeConstantPoly (Some (ValueOf uniPairAB p))) = do
+            :: SomeConstant uni (a, b)
+            -> EvaluationResult (SomeConstant uni (b, a))
+        swapPlc (SomeConstant (Some (ValueOf uniPairAB p))) = do
             DefaultUniPair uniA uniB <- pure uniPairAB
-            pure . SomeConstantPoly $ someValueOf (DefaultUniPair uniB uniA) (snd p, fst p)
+            pure . SomeConstant $ someValueOf (DefaultUniPair uniB uniA) (snd p, fst p)
 
     toBuiltinMeaning SwapEls = makeBuiltinMeaning swapElsPlc mempty where
         -- The type reads as @[(a, Bool)] -> [(Bool, a)]@.
         swapElsPlc
-            :: a ~ Opaque term (TyVarRep ('TyNameRep "a" 0))
-            => SomeConstantPoly uni [] '[SomeConstantPoly uni (,) '[a, Bool]]
-            -> EvaluationResult (SomeConstantPoly uni [] '[SomeConstantPoly uni (,) '[Bool, a]])
-        swapElsPlc (SomeConstantPoly (Some (ValueOf uniList xs))) = do
+            :: SomeConstant uni [SomeConstant uni (a, Bool)]
+            -> EvaluationResult (SomeConstant uni [SomeConstant uni (Bool, a)])
+        swapElsPlc (SomeConstant (Some (ValueOf uniList xs))) = do
             DefaultUniList (DefaultUniPair uniA DefaultUniBool) <- pure uniList
             let uniList' = DefaultUniList $ DefaultUniPair DefaultUniBool uniA
-            pure . SomeConstantPoly . someValueOf uniList' $ map swap xs
+            pure . SomeConstant . someValueOf uniList' $ map swap xs
diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Debug.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Debug.hs
index f85877e43b9..bec58ea988b 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Constant/Debug.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Debug.hs
@@ -22,8 +22,6 @@ type TermDebug = Term TyName Name DefaultUni DefaultFun ()
 --
 -- >>> :t enumerateDebug False
 -- enumerateDebug False :: Bool
--- >>> :t enumerateDebug $ Just 'a'
--- enumerateDebug $ Just 'a' :: Maybe Char
 -- >>> :t enumerateDebug $ \_ -> ()
 -- enumerateDebug $ \_ -> ()
 --   :: Opaque
@@ -31,13 +29,13 @@ type TermDebug = Term TyName Name DefaultUni DefaultFun ()
 --        (TyVarRep ('TyNameRep "a" 0))
 --      -> ()
 -- >>> :t enumerateDebug 42
--- <interactive>:1:16-17: error:
+-- <interactive>:1:16: error:
 --     • Built-in functions are not allowed to have constraints
 --       To fix this error instantiate all constrained type variables
 --     • In the first argument of ‘enumerateDebug’, namely ‘42’
 --       In the expression: enumerateDebug 42
-enumerateDebug :: forall a j. EnumerateFromTo 0 j TermDebug a => a -> a
-enumerateDebug = id
+specializeDebug :: forall a j. SpecializeFromTo 0 j TermDebug a => a -> a
+specializeDebug = id
 
 -- | Instantiate type variables in the type of a value using 'EnumerateFromTo' and check that it's
 -- possible to construct a 'TypeScheme' out of the resulting type. Example usages:
@@ -45,9 +43,10 @@ enumerateDebug = id
 -- >>> :t inferDebug False
 -- inferDebug False :: Bool
 -- >>> :t inferDebug $ Just 'a'
--- <interactive>:1:1-21: error:
---     • There's no 'KnownType' instance for Maybe Char
---       Did you add a new built-in type and forget to provide a 'KnownType' instance for it?
+-- <interactive>:1:1: error:
+--     • No instance for (KnownPolytype
+--                          (ToBinds (Maybe Char)) TermDebug '[] (Maybe Char) (Maybe Char))
+--         arising from a use of ‘inferDebug’
 --     • In the expression: inferDebug $ Just 'a'
 -- >>> :t inferDebug $ \_ -> ()
 -- inferDebug $ \_ -> ()
@@ -58,8 +57,7 @@ enumerateDebug = id
 inferDebug
     :: forall a binds args res j.
        ( args ~ GetArgs a, a ~ FoldArgs args res, binds ~ Merge (ListToBinds args) (ToBinds res)
-       , KnownPolytype binds TermDebug args res a, EnumerateFromTo 0 j TermDebug a
-       , KnownMonotype TermDebug args res a
+       , KnownPolytype binds TermDebug args res a, SpecializeFromTo 0 j TermDebug a
        )
     => a -> a
 inferDebug = id
diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs
index 5ee65ae353b..21b3aacc081 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs
@@ -20,13 +20,11 @@ module PlutusCore.Constant.Meaning where
 
 import PlutusPrelude
 
-import PlutusCore.Constant.Dynamic.Emit
 import PlutusCore.Constant.Function
 import PlutusCore.Constant.Kinded
 import PlutusCore.Constant.Typed
 import PlutusCore.Core
 import PlutusCore.Evaluation.Machine.Exception
-import PlutusCore.Evaluation.Result
 import PlutusCore.Name
 
 import Control.Lens (ix, (^?))
@@ -232,94 +230,73 @@ type x ~?~ y = TryUnify (x === y) x y
 -- | Get the element at an @i@th position in a list.
 type Lookup :: forall a. Nat -> [a] -> a
 type family Lookup n xs where
+    Lookup _ '[]       = TypeError ('Text "Not enough elements")
     Lookup 0 (x ': xs) = x
     Lookup n (_ ': xs) = Lookup (n - 1) xs
 
 -- | Get the name at the @i@th position in the list of default names. We could use @a_0@, @a_1@,
 -- @a_2@ etc instead, but @a@, @b@, @c@ etc are nicer.
-type GetName i = Lookup i '["a", "b", "c", "d", "e", "f", "g", "h"]
+type GetName :: GHC.Type -> Nat -> Symbol
+type family GetName k i where
+    GetName GHC.Type i = Lookup i '["a", "b", "c", "d", "e", "i", "j", "k", "l"]
+    GetName _        i = Lookup i '["f", "g", "h", "m", "n"]  -- For higher-kinded types.
+
+-- | Like 'id', but a type constructor.
+type Id :: forall a. a -> a
+data family Id x
 
 -- | Try to specialize @a@ as a type representing a PLC type variable.
 -- @i@ is a fresh id and @j@ is a final one (either @i + 1@ or @i@ depending on whether
 -- specialization attempt is successful or not).
-type TrySpecializeAsVar :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint
-class TrySpecializeAsVar i j term a | i term a -> j
+-- @f@ is for wrapping 'TyVarRep' (see 'HandleHole' for how this is used).
+type TrySpecializeAsVar :: forall k. Nat -> Nat -> (k -> k) -> k -> GHC.Constraint
+class TrySpecializeAsVar i j f a | i f a -> j
 instance
-    ( var ~ Opaque term (TyVarRep ('TyNameRep (GetName i) i))
+    ( var ~ f (TyVarRep @k ('TyNameRep (GetName k i) i))
     -- Try to unify @a@ with a freshly created @var@.
     , a ~?~ var
     -- If @a@ is equal to @var@ then unification was successful and we just used the fresh id and
     -- so we need to bump it up. Otherwise @var@ was discarded and so the fresh id is still fresh.
     -- Replacing @(===)@ with @(==)@ causes errors at use site, for whatever reason.
     , j ~ If (a === var) (i + 1) i
-    ) => TrySpecializeAsVar i j term a
-
--- | For looking under special-case types, for example the type of a constant or the type arguments
--- of a polymorphic built-in type get specialized as types representing PLC type variables,
--- and for 'Emitter' and 'EvaluationResult' we simply recurse into the type that they receive.
--- @i@ is a fresh id and @j@ is a final one as in 'TrySpecializeAsVar', but since
--- 'HandleSpecialCases' can specialize multiple variables, @j@ can be equal to @i + n@ for any @n@
--- (including @0@).
-type HandleSpecialCases :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint
-class HandleSpecialCases i j term a | i term a -> j
-instance {-# OVERLAPPABLE #-} i ~ j => HandleSpecialCases i j term a
--- The 'Opaque' wrapper is due to 'TrySpecializeAsVar' trying to unify its last argument with
--- an 'Opaque' thing, but here we only want to instantiate the type representations.
--- | Take an argument of a polymorphic built-in type and try to specialize it as a type representing
--- a PLC type variable.
-instance {-# OVERLAPPING #-} TrySpecializeAsVar i j term (Opaque term rep) =>
-        HandleSpecialCases i j term (SomeConstant uni rep)
-instance {-# OVERLAPPING #-} EnumerateFromToOne i j term a =>
-        HandleSpecialCases i j term (EvaluationResult a)
-instance {-# OVERLAPPING #-} EnumerateFromToOne i j term a =>
-        HandleSpecialCases i j term (Emitter a)
--- Note that we don't explicitly handle the no-more-arguments case as it's handled by the
--- @OVERLAPPABLE@ instance above.
-instance {-# OVERLAPPING #-}
-    ( TrySpecializeAsVar i j term (Opaque term rep)
-    , HandleSpecialCases j k term (SomeConstantPoly uni f reps)
-    ) => HandleSpecialCases i k term (SomeConstantPoly uni f (rep ': reps))
-
--- | Instantiate an argument or result type.
-type EnumerateFromToOne :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint
-class EnumerateFromToOne i j term a | i term a -> j
--- | First try to instantiate @a@ as a PLC type variable, then handle all the special cases.
+    ) => TrySpecializeAsVar i j f (a :: k)
+
+-- | First try to specialize the hole using 'TrySpecializeAsVar' and then recurse on the result of
+-- that using 'HandleHoles'.
+-- @i@ is a fresh id and @j@ is a final one as in 'TrySpecializeAsVar', but since 'HandleHole' can
+-- specialize multiple variables, @j@ can be equal to @i + n@ for any @n@ (including @0@).
+type HandleHole :: Nat -> Nat -> GHC.Type -> Hole -> GHC.Constraint
+class HandleHole i j term hole | i term hole -> j
+-- In the Rep context @x@ is attempted to be instantiated as a 'TyVarRep'.
+instance
+    ( TrySpecializeAsVar i j Id (Id x)  -- The two 'Id's cancel each other.
+    , HandleHoles j k term x
+    ) => HandleHole i k term (RepHole x)
+-- In the Type context @a@ is attempted to be instantiated as a 'TyVarRep' wrapped in @Opaque term@.
 instance
-    ( TrySpecializeAsVar i j term a
-    , HandleSpecialCases j k term a
-    ) => EnumerateFromToOne i k term a
-
--- See https://github.com/effectfully/sketches/tree/master/poly-type-of-saga/part2-enumerate-type-vars
--- for a detailed elaboration on how this works.
--- | Specialize each Haskell type variable in @a@ as a type representing a PLC type variable by
--- deconstructing @a@ into an applied @(->)@ (we don't recurse to the left of @(->)@, only to the
--- right) and trying to specialize every argument and result type as a PLC type variable
--- (via 'TrySpecializeAsVar') until no deconstruction is possible, at which point we've got a result
--- which we don't try to specialize, because it's already monomorphic due to 'EnumerateFromTo'
--- trying to specialize its argument before recursing on it using this class.
-type EnumerateFromToRec :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint
-class EnumerateFromToRec i j term a | i term a -> j
-instance {-# OVERLAPPABLE #-} i ~ j => EnumerateFromToRec i j term a
-instance {-# OVERLAPPING #-}
-    ( EnumerateFromToOne i j term a
-    , EnumerateFromTo j k term b
-    ) => EnumerateFromToRec i k term (a -> b)
-
--- | Specialize each Haskell type variable in @a@ as a type representing a PLC type variable by
--- first trying to specialize the whole type using 'EnumerateFromToOne' and then recursing on the
--- result of that using 'EnumerateFromToRec'. The initial attempt to specialize the type allows us
--- to handle the case where the whole type is just a single type variable (such as @undefined :: a@)
--- and it also allows us to look into the result type due to 'EnumerateFromToRec' mutually
--- recursively calling 'EnumerateFromTo'. I.e. the initial attempt at specialization allows
--- 'EnumerateFromToRec' to cut one argument off the type and call 'EnumerateFromTo' over the rest
--- of the type and so forth until we get to the result, which is attempted to be specialized just
--- like in the @undefined@ case where there are no argument types in the first place.
-type EnumerateFromTo :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint
-class EnumerateFromTo i j term a | i term a -> j
+    ( TrySpecializeAsVar i j (Opaque term) a
+    , HandleHoles j k term a
+    ) => HandleHole i k term (TypeHole a)
+
+-- | Call 'HandleHole' over each hole from the list, threading the state (the fresh unique) through
+-- the calls.
+type HandleHolesGo :: Nat -> Nat -> GHC.Type -> [Hole] -> GHC.Constraint
+class HandleHolesGo i j term holes | i term holes -> j
+instance i ~ j => HandleHolesGo i j term '[]
 instance
-    ( EnumerateFromToOne i j term a
-    , EnumerateFromToRec j k term a
-    ) => EnumerateFromTo i k term a
+      ( HandleHole i j term hole
+      , HandleHolesGo j k term holes
+      ) => HandleHolesGo i k term (hole ': holes)
+
+-- | Get the holes of @x@ and recurse into them.
+type HandleHoles :: forall a. Nat -> Nat -> GHC.Type -> a -> GHC.Constraint
+type HandleHoles i j term x = HandleHolesGo i j term (ToHoles x)
+
+-- | Specialize each Haskell type variable in @a@ as a type representing a PLC type variable.
+-- @i@ is a fresh id and @j@ is a final one as in 'TrySpecializeAsVar', but since 'HandleHole' can
+-- specialize multiple variables, @j@ can be equal to @i + n@ for any @n@ (including @0@).
+type SpecializeFromTo :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint
+type SpecializeFromTo i j term a = HandleHole i j term (TypeHole a)
 
 -- See Note [Automatic derivation of type schemes]
 -- | Construct the meaning for a built-in function by automatically deriving its
@@ -330,13 +307,7 @@ instance
 makeBuiltinMeaning
     :: forall a term cost binds args res j.
        ( args ~ GetArgs a, a ~ FoldArgs args res, binds ~ Merge (ListToBinds args) (ToBinds res)
-       , KnownPolytype binds term args res a, EnumerateFromTo 0 j term a
-       -- This constraint is just to get through 'KnownPolytype' stuck on an unknown type straight
-       -- to the custom type error that we have in the @Typed@ module. Though, somehow, the error
-       -- gets triggered even without the constraint when this function in used, but I don't
-       -- understand how that is possible and it does not work when the function from the @Debug@
-       -- module is used. So we're just doing the right thing here and adding the constraint.
-       , KnownMonotype term args res a
+       , KnownPolytype binds term args res a, SpecializeFromTo 0 j term a
        )
     => a -> (cost -> FoldArgsEx args) -> BuiltinMeaning term cost
 makeBuiltinMeaning = BuiltinMeaning (knownPolytype (Proxy @binds) :: TypeScheme term args res)
diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs
index 49164e6529a..6167cf48141 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs
@@ -37,6 +37,9 @@ module PlutusCore.Constant.Typed
     , FromConstant (..)
     , HasConstant
     , HasConstantIn
+    , Hole
+    , RepHole
+    , TypeHole
     , KnownBuiltinTypeAst
     , KnownTypeAst (..)
     , Merge
@@ -50,7 +53,6 @@ module PlutusCore.Constant.Typed
     , readKnownSelf
     , makeKnownOrFail
     , SomeConstant (..)
-    , SomeConstantPoly (..)
     ) where
 
 import PlutusPrelude
@@ -66,10 +68,8 @@ import PlutusCore.MkPlc hiding (error)
 import PlutusCore.Name
 
 import Control.Monad.Except
-import Data.Functor.Const
-import Data.Kind qualified as GHC (Type)
+import Data.Kind qualified as GHC (Constraint, Type)
 import Data.Proxy
-import Data.SOP.Constraint
 import Data.Some.GADT qualified as GADT
 import Data.String
 import Data.Text (Text)
@@ -399,13 +399,13 @@ for built-in types.
 data TyNameRep (kind :: GHC.Type) = TyNameRep Symbol Nat
 
 -- | Representation of an intrinsically-kinded type variable: a name.
-data family TyVarRep (var :: TyNameRep kind) :: kind
+data family TyVarRep (name :: TyNameRep kind) :: kind
 
 -- | Representation of an intrinsically-kinded type application: a function and an argument.
 data family TyAppRep (fun :: dom -> cod) (arg :: dom) :: cod
 
 -- | Representation of of an intrinsically-kinded universal quantifier: a bound name and a body.
-data family TyForallRep (var :: TyNameRep kind) (a :: GHC.Type) :: GHC.Type
+data family TyForallRep (name :: TyNameRep kind) (a :: GHC.Type) :: GHC.Type
 
 -- | Throw an 'UnliftingError' saying that the received argument is not a constant.
 throwNotAConstant
@@ -457,39 +457,163 @@ type HasConstant term = (AsConstant term, FromConstant term)
 -- and connects @term@ and its @uni@.
 type HasConstantIn uni term = (UniOf term ~ uni, HasConstant term)
 
+{- Note [Rep vs Type context]
+Say you define an @Id@ built-in function and specify its Haskell type signature:
+
+    id :: forall a. a -> a
+
+This gets picked up by the 'TypeScheme' inference machinery, which detects @a@ and instantiates it
+to @Opaque term Var0@ where @Var0@ is some concrete type (the exact details don't matter here)
+representing a Plutus type variable of kind @*@ with the @0@ unique, so @id@ elaborates to
+
+    id :: Opaque term Var0 -> Opaque term Var0
+
+But consider also the case where you want to define @id@ only over lists. The signature of the
+built-in function then is
+
+    idList :: forall a. Opaque term [a] -> Opaque term [a]
+
+Now the 'Opaque' is explicit and the 'TypeScheme' inference machinery needs to go under it in order
+to instantiate @a@. Which now does not get instantiated to an 'Opaque' as before, since we're
+already inside an 'Opaque' and can just use @Var0@ directly. So @idList@ elaborates to
+
+    idList :: Opaque term [Var0] -> Opaque term [Var0]
+
+Now let's make up some syntax for annotating contexts so that it's clear what's going on:
+
+    idList @Type |
+        :: (@Type | Opaque term (@Rep | [Var0]))
+        -> (@Type | Opaque term (@Rep | [Var0]))
+
+'@ann |' annotates everything to the right of it. The whole thing then reads as
+
+1. a builtin is always defined in the Type context
+2. @->@ preserves the Type context, i.e. it accepts it and passes it down to the domain and codomain
+3. @Opaque term@ switches the context from Type to Rep, i.e. it accepts the Type context, but
+creates the Rep context for its argument that represents a Plutus type
+
+So why the distinction?
+
+The difference between the Rep and the Type contexts that we've seen so far is that in the Rep
+context we don't need any @Opaque@, but this is a very superficial reason to keep the distinction
+between contexts, since everything that is legal in the Type context is legal in the Rep context
+as well. For example we could've elaborated @idList@ into a bit more verbose
+
+    idList :: Opaque term [Opaque term Var0] -> Opaque term [Opaque term Var0]
+
+and the world wouldn't end because of that, everything would work correctly.
+
+The opposite however is not true: certain types that are legal in the Rep context are not legal in
+the Type one and this is the reason why the distinction exists. The simplest example is
+
+    id :: Var0 -> Var0
+
+@Var0@ represents a Plutus type variable and it's a data family with no inhabitants, so it does not
+make sense to try to unlift a value of that type.
+
+Now let's say we added a @term@ argument to @Var0@ and said that when @Var0 term@ is a @GHC.Type@,
+it has a @term@ inside, just like 'Opaque'. Then we would be able to unlift it, but we also have
+things like @TyAppRep@, @TyForallRep@ and that set is open, any Plutus type can be represented
+using such combinators and we can even name particular types, e.g. we could have @PlcListRep@,
+so we'd have to special-case @GHC.Type@ for each of them and it would be a huge mess.
+
+So instead of mixing up types whose values are actually unliftable with types that are only used
+for type checking, we keep the distinction explicit.
+
+The barrier between Haskell and Plutus is the barrier between the Type and the Rep contexts and
+that barrier must always be some explicit type constructor that switches the context from Type to
+Rep. We've only considered 'Opaque' as an example of such type constructor, but we also have
+'SomeConstant' as another example.
+
+Some type constructors turn any context into the Type one, for example 'EvaluationResult' and
+'Emitter', although they are useless inside the Rep context, given that it's only for type checking
+Plutus and they don't exist in the type language of Plutus.
+
+These @*Rep@ data families like 'TyVarRep', 'TyAppRep' etc all require the Rep context and preserve
+it, since they're only for representing Plutus types for type checking purposes.
+
+We call a thing in a Rep or 'Type' context a 'RepHole' or 'TypeHole' respectively. The reason for
+the name is that the inference machinery looks at the thing and tries to instantiate it, like fill
+a hole.
+
+We could also have a third type of hole/context, Name, because binders bind names rather than
+variables and so it makes sense to infer names sometimes, like for 'TyForallRep' for example.
+We don't do that currently, because we don't have such builtins anyway.
+
+And there could be even fancier kinds of holes like "infer anything" for cases where the hole
+is determined by some other part of the signature. We don't have that either, for the same reason.
+
+For the user defining a builtin this all is pretty much invisible.
+-}
+
+-- See Note [Rep vs Type context].
+-- | The kind of holes.
+data Hole
+
+-- See Note [Rep vs Type context].
+-- | A hole in the Rep context.
+type RepHole :: forall a hole. a -> hole
+data family RepHole x
+
+-- See Note [Rep vs Type context].
+-- | A hole in the Type context.
+type TypeHole :: forall hole. GHC.Type -> hole
+data family TypeHole a
+
+-- | For annotating an uninstantiated built-in type, so that it gets handled by the right instance
+-- or type family.
+type BuiltinHead :: forall k. k -> k
+data family BuiltinHead f
+
+-- | Take an iterated application of a built-in type and elaborate every function application
+-- inside of it to 'TypeAppRep', plus annotate the head with 'BuiltinHead'.
+-- The idea is that we don't need to process built-in types manually if we simply add some
+-- annotations for instance resolution to look for. Think what we'd have to do manually for, say,
+-- 'ToHoles': traverse the spine of the application and collect all the holes into a list, which is
+-- troubling, because type applications are left-nested and lists are right-nested, so we'd have to
+-- use accumulators or an explicit 'Reverse' type family. And then we also have 'KnownTypeAst' and
+-- 'ToBinds', so handling built-in types in a special way for each of those would be a hassle,
+-- especially given the fact that type-level Haskell is not exactly good at computing things.
+-- With the 'ElaborateBuiltin' approach we get 'KnownTypeAst', 'ToHoles' and 'ToBinds' for free.
+type ElaborateBuiltin :: forall k. k -> k
+type family ElaborateBuiltin a where
+    ElaborateBuiltin (f x) = ElaborateBuiltin f `TyAppRep` x
+    ElaborateBuiltin f     = BuiltinHead f
+
 -- | A constraint for \"@a@ is a 'KnownTypeAst' by means of being included in @uni@\".
--- We add such a trivial type synonym to make instances of 'KnownTypeAst' for built-in types look
--- better. For example, the \"abstract\" 'KnownBuiltinTypeAst' looks sensible here:
---
--- > instance KnownBuiltinTypeAst DefaultUni Integer => KnownTypeAst DefaultUni Integer
---
--- while inlining the definition would give us
---
--- > instance DefaultUni `Contains` Integer => KnownTypeAst DefaultUni Integer
---
--- which is nonsense, because the @DefaultUni `Contains` Integer@ constraint is redundant
--- (by means of being trivially satisfied).
---
--- We could omit the constraint in both the cases due to `Integer` being monomorphic, but for
--- polymorphic built-in types we do need it and so we keep things uniform by introducing this
--- type synonym. Which also allows us to replicate the same pattern as with 'KnownTypeIn':
---
--- > instance KnownBuiltinTypeIn DefaultUni term Integer => KnownTypeIn DefaultUni term Integer
-type KnownBuiltinTypeAst = Contains
+type KnownBuiltinTypeAst uni a = KnownTypeAst uni (ElaborateBuiltin a)
+
+type KnownTypeAst :: forall k. (GHC.Type -> GHC.Type) -> k -> GHC.Constraint
+class KnownTypeAst uni a where
+    -- | Return every part of the type that can be a to-be-instantiated type variable.
+    -- For example, in @Integer@ there's no such types and in @(a, b)@ it's the two arguments
+    -- (@a@ and @b@) and the same applies to @a -> b@ (to mention a type that is not built-in).
+    type ToHoles a :: [Hole]
+    type ToHoles a = ToHoles (ElaborateBuiltin a)
 
-class KnownTypeAst uni (a :: k) where
-    -- One can't directly put a PLC type variable into lists or tuples ('SomeConstantPoly' has to be
-    -- used for that), hence we say that polymorphic built-in types can't directly contain any PLC
-    -- type variables in them just like monomorphic ones.
     -- | Collect all unique variables (a variable consists of a textual name, a unique and a kind)
     -- in an @a@.
-    type ToBinds (a :: k) :: [GADT.Some TyNameRep]
-    type ToBinds _ = '[]
+    type ToBinds a :: [GADT.Some TyNameRep]
+    type ToBinds a = ToBinds (ElaborateBuiltin a)
 
     -- | The type representing @a@ used on the PLC side.
     toTypeAst :: proxy a -> Type TyName uni ()
     default toTypeAst :: KnownBuiltinTypeAst uni a => proxy a -> Type TyName uni ()
-    toTypeAst _ = mkTyBuiltin @_ @a ()
+    toTypeAst _ = toTypeAst $ Proxy @(ElaborateBuiltin a)
+    {-# INLINE toTypeAst #-}
+
+instance (KnownTypeAst uni a, KnownTypeAst uni b) => KnownTypeAst uni (a -> b) where
+    type ToHoles (a -> b) = '[TypeHole a, TypeHole b]
+    type ToBinds (a -> b) = Merge (ToBinds a) (ToBinds b)
+
+    toTypeAst _ = TyFun () (toTypeAst $ Proxy @a) (toTypeAst $ Proxy @b)
+    {-# INLINE toTypeAst #-}
+
+instance uni `Contains` f => KnownTypeAst uni (BuiltinHead f) where
+    type ToHoles (BuiltinHead f) = '[]
+    type ToBinds (BuiltinHead f) = '[]
+
+    toTypeAst _ = mkTyBuiltin @_ @f ()
     {-# INLINE toTypeAst #-}
 
 -- | Delete all @x@s from a list.
@@ -510,17 +634,13 @@ type family Merge xs ys :: [a] where
 -- @type instance@ themselves (which is no big deal, but it's nicer not to ask the user to do that).
 -- | Collect all unique variables (a variable consists of a textual name, a unique and a kind)
 -- in a list.
-type family ListToBinds (x :: [a]) :: [GADT.Some TyNameRep]
+type ListToBinds :: forall a. [a] -> [GADT.Some TyNameRep]
+type family ListToBinds xs
 type instance ListToBinds '[]       = '[]
 type instance ListToBinds (x ': xs) = Merge (ToBinds x) (ListToBinds xs)
 
--- We need to be able to partially apply that in the definition of 'ImplementedKnownBuiltinTypeIn',
--- hence defining it as a class synonym.
 -- | A constraint for \"@a@ is a 'KnownType' by means of being included in @uni@\".
-class    (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) =>
-            KnownBuiltinTypeIn uni term a
-instance (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) =>
-            KnownBuiltinTypeIn uni term a
+type KnownBuiltinTypeIn uni term a = (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a)
 
 -- | A constraint for \"@a@ is a 'KnownType' by means of being included in @UniOf term@\".
 type KnownBuiltinType term a = KnownBuiltinTypeIn (UniOf term) term a
@@ -562,6 +682,66 @@ builtins this is rarely the case as most of the time we want aggressive inlining
 and the "just compute the damn thing" behavior.
 -}
 
+{- Note [Unlifting values of built-in types]
+It's trivial to unlift from a term a value of a monomorphic type like 'Integer': just check that
+the term is a constant, extract the type tag and check it for equality with the type tag of
+'Integer'.
+
+Things work the same way for a fully monomorphized polymorphic type, i.e. @(Integer, Bool@) is not
+any different from just 'Integer' unlifting-wise.
+
+However there's no sensible way of unlifting a value of, say, @[a]@ where @a@ in not a built-in
+type. So let's say we instantiated @a@ to an @Opaque term rep@ like we do for polymorphic functions
+that don't deal with polymorphic built-in types (e.g. `id`, `ifThenElse` etc). That would mean we'd
+need to write a function from a @[a]@ for some arbitrary built-in @a@ to @[Opaque term a]@. Which
+is really easy to do: it's just @map makeKnown@. But the problem is, unlifting is supposed to be
+cheap and that @map@ is O(n), so for example 'MkCons' would become an O(n) operation making
+perfectly linear algorithms quadratic. See https://github.com/input-output-hk/plutus/pull/4215 for
+how that would look like.
+
+So the problem is that we can't convert in O(1) time a @[a]@ coming from a constant of
+statically-unknown type (that @a@ is existential) to @[a']@ where @a'@ is known statically.
+Thus it's impossible to instantiate @a@ in Haskell's
+
+    nullList :: [a] -> Bool
+
+so that there's a 'TypeScheme' for this function.
+
+One non-solution would be to instantiate @a@, then recurse on the type, construct a new function
+that defers to the original @nullList@ but wraps its argument in a specific way (more on that below)
+making it possible to assign a 'TypeScheme' to the resulting function. Astonishingly enough, that
+could actually work and if we ever write a paper on builtins, we should mention that example, but:
+
+1. such a trick requires a generic machinery that knows how to check that the head of the builtin
+   application is a particular built-in type. We used to have that, but it was just way too slow
+2. that would only work for functions that don't care about @a@ at all. But for example when
+   elaborating @cons :: a -> [a] -> [a]@ as a Plutus builtin we need to unlift both the arguments
+   and check that their @a@s are equal
+   (See Note [Representable built-in functions over polymorphic built-in types])
+   and it's either way too complex or even impossible to do that automatically within some generic
+   machinery
+
+So what we do is we simply require the user to write
+
+    nullList :: Opaque term [a] -> Bool
+
+and unlift a @[a]@ manually within the definition of the builtin. This works, because the
+existential @a@ never escapes the definition of the builtin. I.e. it's fine to unpack an existential
+and use it immediately without ever exposing the existential parts to the outside and it's not fine
+to try to return a value having an existential inside of it, which is what unlifting of @[a]@ would
+amount to.
+
+Could we somehow align the unlifting machinery so that it does not construct values of particular
+types, but rather feeds them to a continuation or something, so that the existential parts never
+try to escape? Maybe, but see point 2 from the above, we do want to get our hands on the particular
+universes sometimes and point 1 prevents us from doing that generically, so it doesn't seem like
+we could do that within some automated machinery.
+
+Overall, asking the user to manually unlift from @Opaque term [a]@ is just always going to be
+faster than any kind of fancy encoding.
+-}
+
+-- See Note [Unlifting values of built-in types].
 -- | Convert a constant embedded into a PLC term to the corresponding Haskell value.
 readKnownConstant
     :: forall term a err cause. (AsUnliftingError err, KnownBuiltinType term a)
@@ -583,7 +763,7 @@ readKnownConstant mayCause term = asConstant mayCause term >>= oneShot \case
 
 -- See Note [Performance of KnownTypeIn instances].
 -- We use @default@ for providing instances for built-in types instead of @DerivingVia@, because
--- the latter breaks on @m a@ (and for brevity).
+-- the latter breaks on @m term@ (and for brevity).
 -- | Haskell types known to exist on the PLC side.
 -- Both the methods take a @Maybe cause@ argument to report the cause of a potential failure.
 -- @cause@ is different to @term@ to support evaluators that distinguish between terms and values
@@ -591,7 +771,12 @@ readKnownConstant mayCause term = asConstant mayCause term >>= oneShot \case
 -- as a term). Note that an evaluator might require the cause to be computed lazily for best
 -- performance on the happy path and @Maybe@ ensures that even if we somehow force the argument,
 -- the cause stored in it is not forced due to @Maybe@ being a lazy data type.
-class (uni ~ UniOf term, KnownTypeAst uni a) => KnownTypeIn uni term a where
+-- Note that 'KnownTypeAst' is not a superclass of 'KnownTypeIn'. This is due to the fact that
+-- polymorphic built-in types are only liftable/unliftable when they're fully monomorphized, while
+-- 'toTypeAst' works for polymorphic built-in types that have type variables in them, and so the
+-- constraints are completely different in the two cases and we keep the two classes apart
+-- (there doesn't seem to be any cons to that).
+class uni ~ UniOf term => KnownTypeIn uni term a where
     -- | Convert a Haskell value to the corresponding PLC term.
     -- The inverse of 'readKnown'.
     makeKnown
@@ -625,7 +810,7 @@ class (uni ~ UniOf term, KnownTypeAst uni a) => KnownTypeIn uni term a where
     {-# INLINE readKnown #-}
 
 -- | Haskell types known to exist on the PLC side. See 'KnownTypeIn'.
-type KnownType term = KnownTypeIn (UniOf term) term
+type KnownType term a = (KnownTypeAst (UniOf term) a, KnownTypeIn (UniOf term) term a)
 
 -- | Same as 'readKnown', but the cause of a potential failure is the provided term itself.
 readKnownSelf
@@ -664,13 +849,13 @@ makeKnownOrFail :: (KnownType term a, MonadError err m, AsEvaluationFailure err)
 makeKnownOrFail = unNoCauseT . makeKnown (\_ -> pure ()) Nothing
 
 instance KnownTypeAst uni a => KnownTypeAst uni (EvaluationResult a) where
+    type ToHoles (EvaluationResult a) = '[TypeHole a]
     type ToBinds (EvaluationResult a) = ToBinds a
 
     toTypeAst _ = toTypeAst $ Proxy @a
     {-# INLINE toTypeAst #-}
 
-instance (KnownTypeAst uni a, KnownTypeIn uni term a) =>
-            KnownTypeIn uni term (EvaluationResult a) where
+instance KnownTypeIn uni term a => KnownTypeIn uni term (EvaluationResult a) where
     makeKnown _    mayCause EvaluationFailure     = throwingWithCause _EvaluationFailure () mayCause
     makeKnown emit mayCause (EvaluationSuccess x) = makeKnown emit mayCause x
     {-# INLINE makeKnown #-}
@@ -686,6 +871,7 @@ instance (KnownTypeAst uni a, KnownTypeIn uni term a) =>
     {-# INLINE readKnown #-}
 
 instance KnownTypeAst uni a => KnownTypeAst uni (Emitter a) where
+    type ToHoles (Emitter a) = '[TypeHole a]
     type ToBinds (Emitter a) = ToBinds a
 
     toTypeAst _ = toTypeAst $ Proxy @a
@@ -704,54 +890,24 @@ instance KnownTypeIn uni term a => KnownTypeIn uni term (Emitter a) where
 --
 -- The @rep@ parameter specifies how the type looks on the PLC side (i.e. just like with
 -- @Opaque term rep@).
-newtype SomeConstant uni rep = SomeConstant
+newtype SomeConstant uni (rep :: GHC.Type) = SomeConstant
     { unSomeConstant :: Some (ValueOf uni)
     }
 
-instance (uni ~ uni', KnownTypeAst uni rep) => KnownTypeAst uni (SomeConstant uni' rep) where
+instance KnownTypeAst uni rep => KnownTypeAst uni (SomeConstant uni rep) where
+    type ToHoles (SomeConstant _ rep) = '[RepHole rep]
     type ToBinds (SomeConstant _ rep) = ToBinds rep
 
     toTypeAst _ = toTypeAst $ Proxy @rep
     {-# INLINE toTypeAst #-}
 
-instance (HasConstantIn uni term, KnownTypeAst uni rep) =>
-            KnownTypeIn uni term (SomeConstant uni rep) where
+instance HasConstantIn uni term => KnownTypeIn uni term (SomeConstant uni rep) where
     makeKnown _ _ = coerceArg $ pure . fromConstant
     {-# INLINE makeKnown #-}
 
     readKnown = coerceVia (\asC mayCause -> fmap SomeConstant . asC mayCause) asConstant
     {-# INLINE readKnown #-}
 
--- | For unlifting from the 'Constant' constructor when the stored value is of a polymorphic
--- built-in type.
---
--- The @f@ is the built-in type and @reps@ are its arguments representing PLC types.
-newtype SomeConstantPoly uni f reps = SomeConstantPoly
-    { unSomeConstantPoly :: Some (ValueOf uni)
-    }
-
-instance (uni `Contains` f, uni ~ uni', All (KnownTypeAst uni) reps) =>
-            KnownTypeAst uni (SomeConstantPoly uni' f reps) where
-    type ToBinds (SomeConstantPoly uni' f reps) = ListToBinds reps
-
-    toTypeAst _ =
-        -- Convert the type-level list of arguments into a term-level one and feed it to @f@.
-        mkIterTyApp () (mkTyBuiltin @_ @f ()) $
-            cfoldr_SList
-                (Proxy @(All (KnownTypeAst uni) reps))
-                (\(_ :: Proxy (rep ': _reps')) rs -> toTypeAst (Proxy @rep) : rs)
-                []
-    {-# INLINE toTypeAst #-}
-
-instance ( uni `Contains` f, uni ~ uni', All (KnownTypeAst uni) reps
-         , HasConstantIn uni term
-         ) => KnownTypeIn uni term (SomeConstantPoly uni f reps) where
-    makeKnown _ _ = coerceArg $ pure . fromConstant
-    {-# INLINE makeKnown #-}
-
-    readKnown = coerceVia (\asC mayCause -> fmap SomeConstantPoly . asC mayCause) asConstant
-    {-# INLINE readKnown #-}
-
 toTyNameAst
     :: forall text uniq. (KnownSymbol text, KnownNat uniq)
     => Proxy ('TyNameRep text uniq) -> TyName
@@ -760,24 +916,27 @@ toTyNameAst _ =
         (Text.pack $ symbolVal @text Proxy)
         (Unique . fromIntegral $ natVal @uniq Proxy)
 
-instance (var ~ 'TyNameRep text uniq, KnownSymbol text, KnownNat uniq) =>
-            KnownTypeAst uni (TyVarRep var) where
-    type ToBinds (TyVarRep var) = '[ 'GADT.Some var ]
+instance (name ~ 'TyNameRep text uniq, KnownSymbol text, KnownNat uniq) =>
+            KnownTypeAst uni (TyVarRep name) where
+    type ToHoles (TyVarRep name) = '[]
+    type ToBinds (TyVarRep name) = '[ 'GADT.Some name ]
 
     toTypeAst _ = TyVar () . toTyNameAst $ Proxy @('TyNameRep text uniq)
     {-# INLINE toTypeAst #-}
 
 instance (KnownTypeAst uni fun, KnownTypeAst uni arg) => KnownTypeAst uni (TyAppRep fun arg) where
+    type ToHoles (TyAppRep fun arg) = '[RepHole fun, RepHole arg]
     type ToBinds (TyAppRep fun arg) = Merge (ToBinds fun) (ToBinds arg)
 
     toTypeAst _ = TyApp () (toTypeAst $ Proxy @fun) (toTypeAst $ Proxy @arg)
     {-# INLINE toTypeAst #-}
 
 instance
-        ( var ~ 'TyNameRep @kind text uniq, KnownSymbol text, KnownNat uniq
+        ( name ~ 'TyNameRep @kind text uniq, KnownSymbol text, KnownNat uniq
         , KnownKind kind, KnownTypeAst uni a
-        ) => KnownTypeAst uni (TyForallRep var a) where
-    type ToBinds (TyForallRep var a) = Delete ('GADT.Some var) (ToBinds a)
+        ) => KnownTypeAst uni (TyForallRep name a) where
+    type ToHoles (TyForallRep name a) = '[RepHole a]
+    type ToBinds (TyForallRep name a) = Delete ('GADT.Some name) (ToBinds a)
 
     toTypeAst _ =
         TyForall ()
@@ -787,13 +946,13 @@ instance
     {-# INLINE toTypeAst #-}
 
 instance KnownTypeAst uni rep => KnownTypeAst uni (Opaque term rep) where
+    type ToHoles (Opaque _ rep) = '[RepHole rep]
     type ToBinds (Opaque _ rep) = ToBinds rep
 
     toTypeAst _ = toTypeAst $ Proxy @rep
     {-# INLINE toTypeAst #-}
 
-instance (term ~ term', uni ~ UniOf term, KnownTypeAst uni rep) =>
-            KnownTypeIn uni term (Opaque term' rep) where
+instance uni ~ UniOf term => KnownTypeIn uni term (Opaque term rep) where
     makeKnown _ _ = coerceArg pure  -- A faster @pure . Opaque@.
     {-# INLINE makeKnown #-}
 
@@ -875,22 +1034,3 @@ coerceVia _ = coerce
 coerceArg :: Coercible a b => (a -> r) -> b -> r
 coerceArg = coerce
 {-# INLINE coerceArg #-}
-
--- | Like 'cpara_SList' but the folding function takes a 'Proxy' argument for the convenience of
--- the caller.
-cparaP_SList
-    :: forall k c (xs :: [k]) proxy r. All c xs
-    => proxy c
-    -> r '[]
-    -> (forall y ys. (c y, All c ys) => Proxy (y ': ys) -> r ys -> r (y ': ys))
-    -> r xs
-cparaP_SList p z f = cpara_SList p z $ f Proxy
-
--- | A right fold over reflected lists. Like 'cparaP_SList' except not indexed.
-cfoldr_SList
-    :: forall c xs r proxy. All c xs
-    => proxy (All c xs)
-    -> (forall y ys. (c y, All c ys) => Proxy (y ': ys) -> r -> r)
-    -> r
-    -> r
-cfoldr_SList _ f z = getConst $ cparaP_SList @_ @c @xs Proxy (coerce z) (coerce . f)
diff --git a/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs b/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs
index fb7ca5f6453..043e8157637 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs
@@ -267,8 +267,8 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
             fstPlc
             (runCostingFunOneArgument . paramFstPair)
         where
-          fstPlc :: SomeConstantPoly uni (,) '[a, b] -> EvaluationResult (Opaque term a)
-          fstPlc (SomeConstantPoly (Some (ValueOf uniPairAB xy))) = do
+          fstPlc :: SomeConstant uni (a, b) -> EvaluationResult (Opaque term a)
+          fstPlc (SomeConstant (Some (ValueOf uniPairAB xy))) = do
               DefaultUniPair uniA _ <- pure uniPairAB
               pure . fromConstant . someValueOf uniA $ fst xy
           {-# INLINE fstPlc #-}
@@ -277,8 +277,8 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
             sndPlc
             (runCostingFunOneArgument . paramSndPair)
         where
-          sndPlc :: SomeConstantPoly uni (,) '[a, b] -> EvaluationResult (Opaque term b)
-          sndPlc (SomeConstantPoly (Some (ValueOf uniPairAB xy))) = do
+          sndPlc :: SomeConstant uni (a, b) -> EvaluationResult (Opaque term b)
+          sndPlc (SomeConstant (Some (ValueOf uniPairAB xy))) = do
               DefaultUniPair _ uniB <- pure uniPairAB
               pure . fromConstant . someValueOf uniB $ snd xy
           {-# INLINE sndPlc #-}
@@ -288,8 +288,8 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
             choosePlc
             (runCostingFunThreeArguments . paramChooseList)
         where
-          choosePlc :: SomeConstantPoly uni [] '[a] -> b -> b -> EvaluationResult b
-          choosePlc (SomeConstantPoly (Some (ValueOf uniListA xs))) a b = do
+          choosePlc :: SomeConstant uni [a] -> b -> b -> EvaluationResult b
+          choosePlc (SomeConstant (Some (ValueOf uniListA xs))) a b = do
             DefaultUniList _ <- pure uniListA
             pure $ case xs of
                 []    -> a
@@ -302,11 +302,11 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
         where
           consPlc
               :: SomeConstant uni a
-              -> SomeConstantPoly uni [] '[a]
-              -> EvaluationResult (Opaque term (SomeConstantPoly uni [] '[a]))
+              -> SomeConstant uni [a]
+              -> EvaluationResult (Opaque term [a])
           consPlc
             (SomeConstant (Some (ValueOf uniA x)))
-            (SomeConstantPoly (Some (ValueOf uniListA xs))) = do
+            (SomeConstant (Some (ValueOf uniListA xs))) = do
                 DefaultUniList uniA' <- pure uniListA
                 -- Checking that the type of the constant is the same as the type of the elements
                 -- of the unlifted list. Note that there's no way we could enforce this statically
@@ -322,8 +322,8 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
             headPlc
             (runCostingFunOneArgument . paramHeadList)
         where
-          headPlc :: SomeConstantPoly uni [] '[a] -> EvaluationResult (Opaque term a)
-          headPlc (SomeConstantPoly (Some (ValueOf uniListA xs))) = do
+          headPlc :: SomeConstant uni [a] -> EvaluationResult (Opaque term a)
+          headPlc (SomeConstant (Some (ValueOf uniListA xs))) = do
               DefaultUniList uniA <- pure uniListA
               x : _ <- pure xs
               pure . fromConstant $ someValueOf uniA x
@@ -333,10 +333,8 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
             tailPlc
             (runCostingFunOneArgument . paramTailList)
         where
-          tailPlc
-            :: listA ~ SomeConstantPoly uni [] '[a]
-            => listA -> EvaluationResult (Opaque term listA)
-          tailPlc (SomeConstantPoly (Some (ValueOf uniListA xs))) = do
+          tailPlc :: SomeConstant uni [a] -> EvaluationResult (Opaque term [a])
+          tailPlc (SomeConstant (Some (ValueOf uniListA xs))) = do
               DefaultUniList _ <- pure uniListA
               _ : xs' <- pure xs
               pure . fromConstant $ someValueOf uniListA xs'
@@ -346,8 +344,8 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
             nullPlc
             (runCostingFunOneArgument . paramNullList)
         where
-          nullPlc :: SomeConstantPoly uni [] '[a] -> EvaluationResult Bool
-          nullPlc (SomeConstantPoly (Some (ValueOf uniListA xs))) = do
+          nullPlc :: SomeConstant uni [a] -> EvaluationResult Bool
+          nullPlc (SomeConstant (Some (ValueOf uniListA xs))) = do
               DefaultUniList _ <- pure uniListA
               pure $ null xs
           {-# INLINE nullPlc #-}
diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/ConstrData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/ConstrData.plc.golden
index fe32ff4613e..5fa1482c828 100644
--- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/ConstrData.plc.golden
+++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/ConstrData.plc.golden
@@ -1 +1 @@
-(fun (con integer) (fun (con list (data)) (con data)))
\ No newline at end of file
+(fun (con integer) (fun [ (con list) (con data) ] (con data)))
\ No newline at end of file
diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/IdRank2.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/IdRank2.plc.golden
index 9bf820ba54f..5b55553b890 100644
--- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/IdRank2.plc.golden
+++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/IdRank2.plc.golden
@@ -1 +1 @@
-(all f (fun (type) (type)) (fun (all a (type) [ f a ]) (all a (type) [ f a ])))
\ No newline at end of file
+(all f (fun (type) (type)) (fun (all b (type) [ f b ]) (all b (type) [ f b ])))
\ No newline at end of file
diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/ListData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/ListData.plc.golden
index db1c0d46832..650a37e4f13 100644
--- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/ListData.plc.golden
+++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/ListData.plc.golden
@@ -1 +1 @@
-(fun (con list (data)) (con data))
\ No newline at end of file
+(fun [ (con list) (con data) ] (con data))
\ No newline at end of file
diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MapData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MapData.plc.golden
index 4528e44fc2d..c05e012e32d 100644
--- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MapData.plc.golden
+++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MapData.plc.golden
@@ -1 +1 @@
-(fun (con list (pair (data) (data))) (con data))
\ No newline at end of file
+(fun [ (con list) [ [ (con pair) (con data) ] (con data) ] ] (con data))
\ No newline at end of file
diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilData.plc.golden
index 5aa049e4e5d..5cdcb2c0c12 100644
--- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilData.plc.golden
+++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilData.plc.golden
@@ -1 +1 @@
-(fun (con unit) (con list (data)))
\ No newline at end of file
+(fun (con unit) [ (con list) (con data) ])
\ No newline at end of file
diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilPairData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilPairData.plc.golden
index 03cfed066e4..754dae6673f 100644
--- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilPairData.plc.golden
+++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilPairData.plc.golden
@@ -1 +1 @@
-(fun (con unit) (con list (pair (data) (data))))
\ No newline at end of file
+(fun (con unit) [ (con list) [ [ (con pair) (con data) ] (con data) ] ])
\ No newline at end of file
diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkPairData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkPairData.plc.golden
index 95b239b007d..2c3fb473d97 100644
--- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkPairData.plc.golden
+++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkPairData.plc.golden
@@ -1 +1 @@
-(fun (con data) (fun (con data) (con pair (data) (data))))
\ No newline at end of file
+(fun (con data) (fun (con data) [ [ (con pair) (con data) ] (con data) ]))
\ No newline at end of file
diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnConstrData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnConstrData.plc.golden
index 4bc2e6fad6d..5c617498086 100644
--- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnConstrData.plc.golden
+++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnConstrData.plc.golden
@@ -1 +1 @@
-(fun (con data) (con pair (integer) (list (data))))
\ No newline at end of file
+(fun (con data) [ [ (con pair) (con integer) ] [ (con list) (con data) ] ])
\ No newline at end of file
diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnListData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnListData.plc.golden
index 47c39980724..5ef033d37fe 100644
--- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnListData.plc.golden
+++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnListData.plc.golden
@@ -1 +1 @@
-(fun (con data) (con list (data)))
\ No newline at end of file
+(fun (con data) [ (con list) (con data) ])
\ No newline at end of file
diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnMapData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnMapData.plc.golden
index 9865ed48054..4a2082f4f8f 100644
--- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnMapData.plc.golden
+++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnMapData.plc.golden
@@ -1 +1 @@
-(fun (con data) (con list (pair (data) (data))))
\ No newline at end of file
+(fun (con data) [ (con list) [ [ (con pair) (con data) ] (con data) ] ])
\ No newline at end of file
diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnsafeCoerce.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnsafeCoerce.plc.golden
new file mode 100644
index 00000000000..6126ad090f6
--- /dev/null
+++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnsafeCoerce.plc.golden
@@ -0,0 +1 @@
+(all a (type) (all b (type) (fun a b)))
\ No newline at end of file
diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnsafeCoerceEl.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnsafeCoerceEl.plc.golden
new file mode 100644
index 00000000000..ef3a9750e3d
--- /dev/null
+++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnsafeCoerceEl.plc.golden
@@ -0,0 +1 @@
+(all a (type) (all b (type) (fun [ (con list) a ] [ (con list) b ])))
\ No newline at end of file