[Builtins] Add 'MakeBuiltinMeaning' and type errors doctests (#4649)

This polishes the `PlutusCore.Builtin.Meaning` module and adds another tool to `PlutusCore.Builtin.Debug` allowing us to debug the whole `BuiltinMeaning` inference pipeline.

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

@@ -3,15 +3,17 @@
 
 {-# LANGUAGE DataKinds #-}
 
--- | This module helps to visualize and debug the 'TypeScheme' inference machinery from the
--- @Meaning@ module.
+-- | This module helps to visualize and debug the 'BuiltinMeaning' inference machinery from the
+-- @Elaborate@ and @Meaning@ modules.
 module PlutusCore.Builtin.Debug
   ( elaborateDebug
+  , makeBuiltinMeaningDebug
   -- Reexporting a bunch of stuff, so that debug output is not littered with module names.
   , module Export
   ) where
 
 import PlutusCore.Builtin.Elaborate as Export
+import PlutusCore.Builtin.Meaning as Export
 import PlutusCore.Builtin.Polymorphism as Export
 import PlutusCore.Core as Export
 import PlutusCore.Default as Export
@@ -21,31 +23,60 @@ import PlutusCore.Name as Export
 --
 -- >>> :t elaborateDebug False
 -- elaborateDebug False :: Bool
--- >>> :t elaborateDebug $ \_ -> ()
--- elaborateDebug $ \_ -> ()
+-- >>> :t elaborateDebug fst
+-- elaborateDebug fst
+--   :: (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
+--      -> TyVarRep ('TyNameRep "a" 0)
+elaborateDebug
+    :: forall a j. ElaborateFromTo 0 j (Term TyName Name DefaultUni DefaultFun ()) a
+    => a -> a
+elaborateDebug = id
+
+-- >>> :t makeBuiltinMeaningDebug $ \_ -> ()
+-- makeBuiltinMeaningDebug $ \_ -> ()
 --   :: Opaque
 --        (Term TyName Name DefaultUni DefaultFun ())
 --        (TyVarRep ('TyNameRep "a" 0))
 --      -> ()
--- >>> :t elaborateDebug $ Just ()
+-- >>> :t makeBuiltinMeaningDebug False
+-- <interactive>:1:1: error:
+--     • A built-in function must take at least one type or term argument
+--       ‘Bool’ is a built-in type so you can embed any of its values as a constant
+--       If you still want a built-in function, add a dummy ‘()’ argument
+--     • In the expression: makeBuiltinMeaningDebug False
+-- >>> :t makeBuiltinMeaningDebug $ 0 + 42
+-- <interactive>:1:27: error:
+--     • Built-in functions are not allowed to have constraints
+--       To fix this error instantiate all constrained type variables
+--     • In the second argument of ‘($)’, namely ‘0 + 42’
+--       In the expression: makeBuiltinMeaningDebug $ 0 + 42
+-- >>> :t makeBuiltinMeaningDebug $ 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)
+--         then go add the instance (you may need a few others 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 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
+--     • In the expression: makeBuiltinMeaningDebug $ Just ()
+-- >>> :t makeBuiltinMeaningDebug fst
+-- <interactive>:1:1: error:
+--     • Plutus type variables can't directly appear inside built-in types
+--       Are you trying to define a polymorphic built-in function over a polymorphic type?
+--       In that case you need to wrap all polymorphic built-in types having type variables
+--         in them with either ‘SomeConstant’ or ‘Opaque’ depending on whether its the type
+--         of an argument or the type of the result, respectively
+--     • In the expression: makeBuiltinMeaningDebug fst
+-- >>> :t makeBuiltinMeaningDebug null
+-- <interactive>:1:25: error:
+--     • Built-in functions are not allowed to have higher-kinded type variables applied via regular type application
+--       To fix this error instantiate all higher-kinded type variables
+--     • In the first argument of ‘makeBuiltinMeaningDebug’, namely ‘null’
+--       In the expression: makeBuiltinMeaningDebug null
+makeBuiltinMeaningDebug
+    :: forall a. MakeBuiltinMeaning a (Term TyName Name DefaultUni DefaultFun ())
     => a -> a
-elaborateDebug = id
+makeBuiltinMeaningDebug = id

plutus-core/plutus-core/src/PlutusCore/Builtin/Elaborate.hs

@@ -128,7 +128,7 @@ type family UnknownTypeError val x where
         ':$$: '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 "  then go add the instance (you may need a few others 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)"