[Builtins] Throw on nullary builtins

plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs

@@ -142,6 +142,7 @@ defBuiltinsRuntimeExt = toBuiltinsRuntime defaultUnliftingMode (defaultBuiltinCo
 
 data PlcListRep (a :: GHC.Type)
 instance KnownTypeAst uni a => KnownTypeAst uni (PlcListRep a) where
+    type IsBuiltin (PlcListRep a) = 'False
     type ToHoles (PlcListRep a) = '[RepHole a]
     type ToBinds (PlcListRep a) = ToBinds a
 

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

@@ -36,6 +36,7 @@ import Data.Kind qualified as GHC (Constraint, Type)
 import Data.Proxy
 import Data.Some.GADT qualified as GADT
 import Data.Text qualified as Text
+import Data.Type.Bool
 import GHC.TypeLits
 import Universe
 
@@ -167,6 +168,10 @@ type KnownBuiltinTypeAst uni a = KnownTypeAst uni (ElaborateBuiltin a)
 
 type KnownTypeAst :: forall a. (GHC.Type -> GHC.Type) -> a -> GHC.Constraint
 class KnownTypeAst uni x where
+    -- | Whether @x@ is a built-in type.
+    type IsBuiltin x :: Bool
+    type IsBuiltin x = IsBuiltin (ElaborateBuiltin x)
+
     -- | 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).
@@ -185,24 +190,28 @@ class KnownTypeAst uni x where
     {-# INLINE toTypeAst #-}
 
 instance KnownTypeAst uni a => KnownTypeAst uni (EvaluationResult a) where
+    type IsBuiltin (EvaluationResult a) = 'False
     type ToHoles (EvaluationResult a) = '[TypeHole a]
     type ToBinds (EvaluationResult a) = ToBinds a
     toTypeAst _ = toTypeAst $ Proxy @a
     {-# INLINE toTypeAst #-}
 
 instance KnownTypeAst uni a => KnownTypeAst uni (Emitter a) where
+    type IsBuiltin (Emitter a) = 'False
     type ToHoles (Emitter a) = '[TypeHole a]
     type ToBinds (Emitter a) = ToBinds a
     toTypeAst _ = toTypeAst $ Proxy @a
     {-# INLINE toTypeAst #-}
 
 instance KnownTypeAst uni rep => KnownTypeAst uni (SomeConstant uni rep) where
+    type IsBuiltin (SomeConstant uni rep) = 'False
     type ToHoles (SomeConstant _ rep) = '[RepHole rep]
     type ToBinds (SomeConstant _ rep) = ToBinds rep
     toTypeAst _ = toTypeAst $ Proxy @rep
     {-# INLINE toTypeAst #-}
 
 instance KnownTypeAst uni rep => KnownTypeAst uni (Opaque val rep) where
+    type IsBuiltin (Opaque val rep) = 'False
     type ToHoles (Opaque _ rep) = '[RepHole rep]
     type ToBinds (Opaque _ rep) = ToBinds rep
     toTypeAst _ = toTypeAst $ Proxy @rep
@@ -218,25 +227,29 @@ toTyNameAst _ =
 {-# INLINE toTyNameAst #-}
 
 instance uni `Contains` f => KnownTypeAst uni (BuiltinHead f) where
+    type IsBuiltin (BuiltinHead f) = 'True
     type ToHoles (BuiltinHead f) = '[]
     type ToBinds (BuiltinHead f) = '[]
     toTypeAst _ = mkTyBuiltin @_ @f ()
     {-# INLINE toTypeAst #-}
 
 instance (KnownTypeAst uni a, KnownTypeAst uni b) => KnownTypeAst uni (a -> b) where
+    type IsBuiltin (a -> b) = 'False
     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 (name ~ 'TyNameRep text uniq, KnownSymbol text, KnownNat uniq) =>
             KnownTypeAst uni (TyVarRep name) where
+    type IsBuiltin (TyVarRep name) = 'False
     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 IsBuiltin (TyAppRep fun arg) = IsBuiltin fun && IsBuiltin arg
     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)
@@ -246,6 +259,7 @@ instance
         ( name ~ 'TyNameRep @kind text uniq, KnownSymbol text, KnownNat uniq
         , KnownKind kind, KnownTypeAst uni a
         ) => KnownTypeAst uni (TyForallRep name a) where
+    type IsBuiltin (TyForallRep name a) = 'False
     type ToHoles (TyForallRep name a) = '[RepHole a]
     type ToBinds (TyForallRep name a) = Delete ('GADT.Some name) (ToBinds a)
     toTypeAst _ =

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

@@ -197,8 +197,8 @@ instance
         -- 'Either' is only handled upon full saturation and any evaluation failure is only
         -- registered when the whole builtin application is evaluated, a Haskell exception will
         -- occur the same way as with immediate unlifting. It shouldn't matter though, because a
-        -- builtin is not supposed to throw an exception at any stage, that would be a bug regardless
-        -- of how unlifting is aligned.
+        -- builtin is not supposed to throw an exception at any stage, that would be a bug
+        -- regardless of how unlifting is aligned.
         --
         -- 'pure' signifies that no failure can occur at this point.
         pure . toDeferredF @val @args @res $! getF <*> readKnown arg
@@ -225,6 +225,23 @@ instance (KnownSymbol name, KnownNat uniq, KnownKind kind, KnownPolytype binds v
     knownPolytype = TypeSchemeAll @name @uniq @kind Proxy $ knownPolytype @binds
     knownPolyruntime = RuntimeSchemeAll $ knownPolyruntime @binds @val @args @res
 
+-- | Ensure a built-in function is not nullary and throw a nice error otherwise.
+type ThrowOnBothEmpty :: [Some TyNameRep] -> [GHC.Type] -> Bool -> GHC.Type -> GHC.Constraint
+type family ThrowOnBothEmpty binds args isBuiltin a where
+    ThrowOnBothEmpty '[] '[] 'True a =
+        TypeError (
+            'Text "A built-in function must take at least one type or term argument" ':$$:
+            'Text "‘" ':<>: 'ShowType a ':<>: 'Text "’ is a built-in type" ':<>:
+            'Text " so you can embed any of its values as a constant" ':$$:
+            'Text "If you still want a built-in function, introduce a dummy ‘()’ argument"
+            )
+    ThrowOnBothEmpty '[] '[] 'False a =
+        TypeError (
+            'Text "A built-in function must take at least one type or term argument" ':$$:
+            'Text "To fix this error introduce a dummy ‘()’ argument"
+            )
+    ThrowOnBothEmpty _ _ _ _ = ()
+
 -- See Note [Automatic derivation of type schemes]
 -- | Construct the meaning for a built-in function by automatically deriving its
 -- 'TypeScheme', given
@@ -234,6 +251,7 @@ instance (KnownSymbol name, KnownNat uniq, KnownKind kind, KnownPolytype binds v
 makeBuiltinMeaning
     :: forall a val cost binds args res j.
        ( binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res
+       , ThrowOnBothEmpty binds args (IsBuiltin a) a
        , ElaborateFromTo 0 j val a, KnownPolytype binds val args res a
        )
     => a -> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost