[Builtins] Add detection of stuck 'ToHoles'

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

@@ -1,63 +1,51 @@
 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+{-# OPTIONS_GHC -fno-warn-simplifiable-class-constraints #-}
 
-{-# LANGUAGE DataKinds    #-}
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
 
 -- | This module helps to visualize and debug the 'TypeScheme' inference machinery from the
 -- @Meaning@ module.
-module PlutusCore.Constant.Debug where
+module PlutusCore.Constant.Debug
+  ( module PlutusCore.Constant.Debug
+  -- Reexporting a bunch of stuff, so that debug output is not littered with module names.
+  , module Export
+  ) where
 
-import PlutusCore.Constant.Meaning
-import PlutusCore.Constant.Typed
-import PlutusCore.Core
-import PlutusCore.Default
-import PlutusCore.Name
+import PlutusCore.Constant.Meaning as Export
+import PlutusCore.Constant.Typed as Export
+import PlutusCore.Core as Export
+import PlutusCore.Default as Export
+import PlutusCore.Name as Export
 
-type TermDebug = Term TyName Name DefaultUni DefaultFun ()
-
--- | 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
--- constraints, so it's allowed for the type to reference types that are not in the universe.
--- Example usages:
+-- | Instantiate type variables in the type of a value using 'ElaborateFromTo'. Example usages:
 --
--- >>> :t enumerateDebug False
--- enumerateDebug False :: Bool
--- >>> :t enumerateDebug $ \_ -> ()
--- enumerateDebug $ \_ -> ()
+-- >>> :t elaborateDebug False
+-- elaborateDebug False :: Bool
+-- >>> :t elaborateDebug $ \_ -> ()
+-- elaborateDebug $ \_ -> ()
 --   :: Opaque
 --        (Term TyName Name DefaultUni DefaultFun ())
 --        (TyVarRep ('TyNameRep "a" 0))
 --      -> ()
--- >>> :t enumerateDebug 42
--- <interactive>:1:16: error:
+-- >>> :t elaborateDebug $ Just ()
+-- <interactive>:1:1: error:
+--     • No instance for ‘KnownTypeAst DefaultUni (Maybe ())’
+--       Which means
+--         ‘Maybe ()’
+--       is neither a built-in type, nor one of the control types.
+--       If it can be represented in terms of one of the built-in types
+--         then go add the instance (you may need a ‘KnownTypeIn’ one too)
+--         alongside the instance for the built-in type.
+--       Otherwise you may need to add a new built-in type
+--         (provided you're doing something that can be supported in principle)
+--     • In the expression: elaborateDebug $ Just ()
+-- >>> :t elaborateDebug $ 0 + 42
+-- <interactive>:1:18: 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
-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:
---
--- >>> :t inferDebug False
--- inferDebug False :: Bool
--- >>> :t inferDebug $ Just 'a'
--- <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 $ \_ -> ()
---   :: Opaque
---        (Term TyName Name DefaultUni DefaultFun ())
---        (TyVarRep ('TyNameRep "a" 0))
---      -> ()
-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, SpecializeFromTo 0 j TermDebug a
-       )
+--     • In the second argument of ‘($)’, namely ‘0 + 42’
+--       In the expression: elaborateDebug $ 0 + 42
+elaborateDebug
+    :: forall a j. ElaborateFromTo 0 j (Term TyName Name DefaultUni DefaultFun ()) a
     => a -> a
-inferDebug = id
+elaborateDebug = id

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

@@ -288,15 +288,46 @@ instance
       , HandleHolesGo j k term holes
       ) => HandleHolesGo i k term (hole ': holes)
 
+-- | If the outermost constructor of the second argument is known and happens to be one of the
+-- constructors of the list data type, then the second argument is returned back. Otherwise the
+-- first one is returned, which is meant to be a custom type error.
+type ThrowOnStuckList :: forall a. [a] -> [a] -> [a]
+type family ThrowOnStuckList err xs where
+    ThrowOnStuckList _   '[]       = '[]
+    ThrowOnStuckList _   (x ': xs) = x ': xs
+    ThrowOnStuckList err _         = err
+
+type UnknownTypeError :: forall a any. GHC.Type -> a -> any
+type family UnknownTypeError term x where
+    UnknownTypeError term x = TypeError
+        (         'Text "No instance for ‘KnownTypeAst "
+            ':<>: 'ShowType (UniOf term)
+            ':<>: 'Text " ("
+            ':<>: 'ShowType x
+            ':<>: 'Text ")’"
+        ':$$: 'Text "Which means"
+        ':$$: 'Text "  ‘" ':<>: 'ShowType x ':<>: 'Text "’"
+        ':$$: 'Text "is neither a built-in type, nor one of the control types."
+        ':$$: 'Text "If it can be represented in terms of one of the built-in types"
+        ':$$: 'Text "  then go add the instance (you may need a ‘KnownTypeIn’ one too)"
+        ':$$: 'Text "  alongside the instance for the built-in type."
+        ':$$: 'Text "Otherwise you may need to add a new built-in type"
+        ':$$: 'Text "  (provided you're doing something that can be supported in principle)"
+        )
+
 -- | 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)
+type HandleHoles i j term x =
+    -- Here we detect a stuck application of 'ToHoles' and throw 'UnknownTypeError' on it.
+    -- See https://blog.csongor.co.uk/report-stuck-families for a detailed description of how
+    -- detection of stuck type families works.
+    HandleHolesGo i j term (ThrowOnStuckList (UnknownTypeError term x) (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)
+type ElaborateFromTo :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint
+type ElaborateFromTo 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
@@ -306,8 +337,8 @@ type SpecializeFromTo i j term a = HandleHole i j term (TypeHole a)
 -- 2. an uninstantiated costing function
 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, SpecializeFromTo 0 j term a
+       ( binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res
+       , ElaborateFromTo 0 j term a, KnownPolytype binds term args res a
        )
     => a -> (cost -> FoldArgsEx args) -> BuiltinMeaning term cost
 makeBuiltinMeaning = BuiltinMeaning (knownPolytype (Proxy @binds) :: TypeScheme term args res)

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

@@ -44,7 +44,6 @@ module PlutusCore.Constant.Typed
     , KnownBuiltinTypeAst
     , KnownTypeAst (..)
     , Merge
-    , ListToBinds
     , KnownBuiltinTypeIn
     , KnownBuiltinType
     , readKnownConstant
@@ -622,18 +621,6 @@ type family Merge xs ys :: [a] where
     Merge '[]       ys = ys
     Merge (x ': xs) ys = x ': Delete x (Merge xs ys)
 
--- There's no sensible way to provide a 'KnownTypeAst' instance for a type-level list, so we
--- create a separate type family. We could have a single type family on the top level for both
--- 'ToBinds' and 'ListToBinds', but then we'd lose a very convenient default of each type from the
--- universe returning an empty list from 'ToBinds' and the user would need to do provide a
--- @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 ListToBinds :: forall a. [a] -> [GADT.Some TyNameRep]
-type family ListToBinds xs
-type instance ListToBinds '[]       = '[]
-type instance ListToBinds (x ': xs) = Merge (ToBinds x) (ListToBinds xs)
-
 -- | A constraint for \"@a@ is a 'KnownType' by means of being included in @uni@\".
 type KnownBuiltinTypeIn uni term a = (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a)