IntersectMBO · effectfully · Nov 14, 2021 · Nov 14, 2021 · Nov 14, 2021 · Nov 15, 2021
diff --git a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
@@ -89,6 +89,8 @@ instance (Bounded a, Bounded b, Ix a, Ix b) => Ix (Either a b) where
 
     inRange (m, n) i = m <= i && i <= n
 
+-- TODO: UnsafeCoerce
+-- TODO: JoinOpaque
 -- See Note [Representable built-in functions over polymorphic built-in types]
 data ExtensionFun
     = Factorial
@@ -133,6 +135,7 @@ defBuiltinsRuntimeExt = toBuiltinsRuntime (defaultBuiltinCostModel, ())
 data PlcListRep (a :: GHC.Type)
 instance KnownTypeAst uni a => KnownTypeAst uni (PlcListRep a) where
     type ToBinds (PlcListRep a) = ToBinds a
+    type AsSpine (PlcListRep a) = '[ RepDone (PlcListRep a) ]
 
     toTypeAst _ = TyApp () Plc.listTy . toTypeAst $ Proxy @a
 
@@ -179,9 +182,7 @@ 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 :: ai ~ Opaque term (TyAppRep a Integer) => ai -> ai)
             (\_ _ -> ExBudget 1 0)
 
     toBuiltinMeaning IdList =
@@ -244,40 +245,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
@@ -10,10 +10,13 @@ module PlutusCore.Constant.Debug where
 import PlutusCore.Constant.Meaning
 import PlutusCore.Constant.Typed
 import PlutusCore.Core
-import PlutusCore.Default
+import PlutusCore.Default.Universe
 import PlutusCore.Name
 
-type TermDebug = Term TyName Name DefaultUni DefaultFun ()
+-- Just not to depend on any set of builtins, 'cause they might be broken when there's a need for
+-- debugging.
+data FunDebug
+type TermDebug = Term TyName Name DefaultUni FunDebug ()
 
 -- | Instantiate type variables in the type of a value using 'EnumerateFromTo'.
 -- This function only performs the enumeration and checks that the result does not have certain
@@ -23,11 +26,22 @@ type TermDebug = Term TyName Name DefaultUni DefaultFun ()
 -- >>> :t enumerateDebug False
 -- enumerateDebug False :: Bool
 -- >>> :t enumerateDebug $ Just 'a'
--- enumerateDebug $ Just 'a' :: Maybe Char
+-- <interactive>:1:1-25: error:
+--     • Ambiguous type variable ‘j0’ arising from a use of ‘enumerateDebug’
+--       prevents the constraint ‘(HandleSpecialCasesGo
+--                                   0
+--                                   j0
+--                                   (Term TyName Name DefaultUni FunDebug ())
+--                                   (AsSpine (Maybe Char)))’ from being solved.
+--       Probable fix: use a type annotation to specify what ‘j0’ should be.
+--       These potential instances exist:
+--         two instances involving out-of-scope types
+--         (use -fprint-potential-instances to see them all)
+--     • In the expression: enumerateDebug $ Just 'a'
 -- >>> :t enumerateDebug $ \_ -> ()
 -- enumerateDebug $ \_ -> ()
 --   :: Opaque
---        (Term TyName Name DefaultUni DefaultFun ())
+--        (Term TyName Name DefaultUni FunDebug ())
 --        (TyVarRep ('TyNameRep "a" 0))
 --      -> ()
 -- >>> :t enumerateDebug 42
@@ -46,13 +60,14 @@ enumerateDebug = id
 -- 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?
+--     • 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 $ \_ -> ()
 --   :: Opaque
---        (Term TyName Name DefaultUni DefaultFun ())
+--        (Term TyName Name DefaultUni FunDebug ())
 --        (TyVarRep ('TyNameRep "a" 0))
 --      -> ()
 inferDebug

diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs
@@ -21,13 +21,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, (^?))
@@ -243,52 +241,66 @@ type GetName i = Lookup i '["a", "b", "c", "d", "e", "f", "g", "h"]
 -- | 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
+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 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
+    ) => TrySpecializeAsVar i j f (a :: k)
+
+type Id :: forall a. a -> a
+data family Id x
+
+-- TODO
+-- 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.
 
 -- | 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.
+
+type HandleSpecialCase :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint
+class HandleSpecialCase i j term instr | i term instr -> j
+instance i ~ j => HandleSpecialCase i j term (BuiltinDone x)
+-- TODO: write a test for that
+instance TrySpecializeAsVar i j Id (Id x) => HandleSpecialCase i j term (RepDone x)
 instance
-    ( TrySpecializeAsVar i j term a
+    ( TrySpecializeAsVar i j (Opaque term) a
     , HandleSpecialCases j k term a
-    ) => EnumerateFromToOne i k term a
+    ) => HandleSpecialCase i k term (TypeInfer a)
+instance
+    ( TrySpecializeAsVar i j Id (Id x)
+    , HandleSpecialCases j k term x
+    ) => HandleSpecialCase i k term (RepInfer x)
+
+type HandleSpecialCasesGo :: Nat -> Nat -> GHC.Type -> [GHC.Type] -> GHC.Constraint
+class HandleSpecialCasesGo i j term instrs | i term instrs -> j
+instance i ~ j => HandleSpecialCasesGo i j term '[]
+instance
+      ( HandleSpecialCase i j term instr
+      , HandleSpecialCasesGo j k term instrs
+      ) => HandleSpecialCasesGo i k term (instr ': instrs)
+
+type HandleSpecialCases :: forall a. Nat -> Nat -> GHC.Type -> a -> GHC.Constraint
+type HandleSpecialCases i j term x = HandleSpecialCasesGo i j term (AsSpine x)
+
+-- EvaluationResult a
+-- '[AnyType a]
+
+-- Opaque term a
+-- '[AnyRep a]
+
+-- Opaque term ((a, b), c)
+-- '[AnyRep ((a, b), c)]
+-- '[BuiltinHead (,), AnyRep (a, b), AnyRep c]
 
 -- See https://github.com/effectfully/sketches/tree/master/poly-type-of-saga/part2-enumerate-type-vars
 -- for a detailed elaboration on how this works.
@@ -300,11 +312,13 @@ instance
 -- 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 {-# OVERLAPPABLE #-} HandleSpecialCases i j term a => EnumerateFromToRec i j term a
+-- | TODO: First try to instantiate @a@ as a PLC type variable, then handle all the special cases.
 instance {-# OVERLAPPING #-}
-    ( EnumerateFromToOne i j term a
-    , EnumerateFromTo j k term b
-    ) => EnumerateFromToRec i k term (a -> b)
+    ( TrySpecializeAsVar i j (Opaque term) a
+    , HandleSpecialCases j k term a
+    , EnumerateFromTo k l term b
+    ) => EnumerateFromToRec i l 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
@@ -318,7 +332,7 @@ instance {-# OVERLAPPING #-}
 type EnumerateFromTo :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint
 class EnumerateFromTo i j term a | i term a -> j
 instance
-    ( EnumerateFromToOne i j term a
+    ( TrySpecializeAsVar i j (Opaque term) a
     , EnumerateFromToRec j k term a
     ) => EnumerateFromTo i k term a