From f5b44cddac694756430b3696313fb9a2c68706e5 Mon Sep 17 00:00:00 2001 From: effectfully Date: Wed, 27 Apr 2022 03:17:46 +0200 Subject: [PATCH] [Builtins] Throw on nullary builtins --- .../examples/PlutusCore/Examples/Builtins.hs | 1 + .../src/PlutusCore/Builtin/KnownTypeAst.hs | 14 ++++++++++++ .../src/PlutusCore/Builtin/Meaning.hs | 22 +++++++++++++++++-- 3 files changed, 35 insertions(+), 2 deletions(-) diff --git a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs index 607bb440a2c..95a82125e26 100644 --- a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs +++ b/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 diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownTypeAst.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownTypeAst.hs index 75ea748292c..337463cce9e 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownTypeAst.hs +++ b/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,12 +227,14 @@ 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) @@ -231,12 +242,14 @@ instance (KnownTypeAst uni a, KnownTypeAst uni b) => KnownTypeAst uni (a -> b) w 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 _ = diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs index 54150af70cc..b57915d6eca 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs +++ b/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