[Builtins] Polish handling of integral types

plutus-core/changelog.d/20240529_153319_effectfully_polish_handling_of_integral_types.md

@@ -0,0 +1,7 @@
+### Added
+
+- Missing `KnownTypeAst`, `ReadKnownIn` and `MakeKnownIn` for integral types (`Int8`, `Word16` etc) in #6036
+
+### Changed
+
+- Made unlifting errors a bit more flexible by allowing operational unlifting errors in #6036

plutus-core/plutus-core.cabal

@@ -116,6 +116,7 @@ library
     PlutusCore.Default
     PlutusCore.Default.Builtins
     PlutusCore.Error
+    PlutusCore.Evaluation.Error
     PlutusCore.Evaluation.ErrorWithCause
     PlutusCore.Evaluation.Machine.BuiltinCostModel
     PlutusCore.Evaluation.Machine.Ck

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

@@ -174,7 +174,7 @@ instance
     type IsBuiltin _ (MetaForall name a) = 'False
     type ToHoles _ (MetaForall name a) = '[TypeHole a]
     type ToBinds uni acc (MetaForall name a) = ToBinds uni (Insert ('GADT.Some name) acc) a
-    toTypeAst _ = toTypeAst $ Proxy @a
+    typeAst = toTypeAst $ Proxy @a
 instance MakeKnownIn DefaultUni term a => MakeKnownIn DefaultUni term (MetaForall name a) where
     makeKnown (MetaForall x) = makeKnown x
 -- 'ReadKnownIn' doesn't make sense for 'MetaForall'.
@@ -185,16 +185,19 @@ instance (tyname ~ TyName, KnownTypeAst tyname uni a) =>
     type IsBuiltin _ (PlcListRep a) = 'False
     type ToHoles _ (PlcListRep a) = '[RepHole a]
     type ToBinds uni acc (PlcListRep a) = ToBinds uni acc a
-    toTypeAst _ = TyApp () Plc.listTy . toTypeAst $ Proxy @a
+    typeAst = TyApp () Plc.listTy . toTypeAst $ Proxy @a
 
 instance tyname ~ TyName => KnownTypeAst tyname DefaultUni Void where
-    toTypeAst _ = runQuote $ do
+    type IsBuiltin _ _ = 'False
+    type ToHoles _ _ = '[]
+    type ToBinds _ acc _ = acc
+    typeAst = runQuote $ do
         a <- freshTyName "a"
         pure $ TyForall () a (Type ()) $ TyVar () a
 instance UniOf term ~ DefaultUni => MakeKnownIn DefaultUni term Void where
     makeKnown = absurd
 instance UniOf term ~ DefaultUni => ReadKnownIn DefaultUni term Void where
-    readKnown _ = throwing _UnliftingError "Can't unlift to 'Void'"
+    readKnown _ = throwing _StructuralUnliftingError "Can't unlift to 'Void'"
 
 data BuiltinErrorCall = BuiltinErrorCall
     deriving stock (Show, Eq)

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

@@ -43,7 +43,6 @@ import PlutusCore.Evaluation.ErrorWithCause
 import PlutusCore.Evaluation.Result
 import PlutusCore.Pretty
 
-import Control.Monad.Except
 import Data.Either.Extras
 import Data.String
 import GHC.Exts (inline, oneShot)
@@ -239,27 +238,17 @@ Lifting is allowed to the following classes of types:
    one, and for another example define an instance for 'Void' in tests
 -}
 
--- | Attach a @cause@ to a 'BuiltinError' and throw that.
--- Note that an evaluator might require the cause to be computed lazily for best performance on the
--- happy path, hence this function must not force its first argument.
--- TODO: wrap @cause@ in 'Lazy' once we have it.
-throwBuiltinErrorWithCause
-    :: (MonadError (ErrorWithCause err cause) m, AsUnliftingError err, AsEvaluationFailure err)
-    => cause -> BuiltinError -> m void
-throwBuiltinErrorWithCause cause = \case
-    BuiltinUnliftingError unlErr -> throwingWithCause _UnliftingError unlErr $ Just cause
-    BuiltinEvaluationFailure     -> throwingWithCause _EvaluationFailure () $ Just cause
-
 typeMismatchError
     :: PrettyParens (SomeTypeIn uni)
     => uni (Esc a)
     -> uni (Esc b)
-    -> UnliftingError
-typeMismatchError uniExp uniAct = fromString $ concat
-    [ "Type mismatch: "
-    , "expected: " ++ render (prettyBy botRenderContext $ SomeTypeIn uniExp)
-    , "; actual: " ++ render (prettyBy botRenderContext $ SomeTypeIn uniAct)
-    ]
+    -> UnliftingEvaluationError
+typeMismatchError uniExp uniAct =
+    MkUnliftingEvaluationError . StructuralEvaluationError . fromString $ concat
+        [ "Type mismatch: "
+        , "expected: " ++ displayBy botRenderContext (SomeTypeIn uniExp)
+        , "; actual: " ++ displayBy botRenderContext (SomeTypeIn uniAct)
+        ]
 -- Just for tidier Core to get generated, we don't care about performance here, since it's just a
 -- failure message and evaluation is about to be shut anyway.
 {-# NOINLINE typeMismatchError #-}
@@ -291,7 +280,7 @@ readKnownConstant val = asConstant val >>= oneShot \case
         -- optimize some of the matching away.
         case uniExp `geq` uniAct of
             Just Refl -> pure x
-            Nothing   -> throwing _UnliftingError $ typeMismatchError uniExp uniAct
+            Nothing   -> throwing _UnliftingEvaluationError $ typeMismatchError uniExp uniAct
 {-# INLINE readKnownConstant #-}
 
 -- See Note [Performance of ReadKnownIn and MakeKnownIn instances].
@@ -335,9 +324,7 @@ makeKnownOrFail x = case makeKnown x of
 
 -- | Same as 'readKnown', but the cause of a potential failure is the provided term itself.
 readKnownSelf
-    :: ( ReadKnown val a
-       , AsUnliftingError err, AsEvaluationFailure err
-       )
+    :: (ReadKnown val a, AsUnliftingEvaluationError err, AsEvaluationFailure err)
     => val -> Either (ErrorWithCause err val) a
 readKnownSelf val = fromRightM (throwBuiltinErrorWithCause val) $ readKnown val
 {-# INLINE readKnownSelf #-}
@@ -361,7 +348,7 @@ instance
         ( TypeError ('Text "‘EvaluationResult’ cannot appear in the type of an argument")
         , uni ~ UniOf val
         ) => ReadKnownIn uni val (EvaluationResult a) where
-    readKnown _ = throwing _UnliftingError "Panic: 'TypeError' was bypassed"
+    readKnown _ = throwing _StructuralUnliftingError "Panic: 'TypeError' was bypassed"
     -- Just for 'readKnown' not to appear in the generated Core.
     {-# INLINE readKnown #-}
 
@@ -374,7 +361,7 @@ instance
         ( TypeError ('Text "‘Emitter’ cannot appear in the type of an argument")
         , uni ~ UniOf val
         ) => ReadKnownIn uni val (Emitter a) where
-    readKnown _ = throwing _UnliftingError "Panic: 'TypeError' was bypassed"
+    readKnown _ = throwing _StructuralUnliftingError "Panic: 'TypeError' was bypassed"
     -- Just for 'readKnown' not to appear in the generated Core.
     {-# INLINE readKnown #-}
 

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

@@ -26,6 +26,7 @@ module PlutusCore.Builtin.KnownTypeAst
     , TypeHole
     , KnownBuiltinTypeAst
     , KnownTypeAst (..)
+    , toTypeAst
     , Insert
     , Delete
     ) where
@@ -210,47 +211,54 @@ class KnownTypeAst tyname uni x where
     type ToBinds uni (acc :: [GADT.Some TyNameRep]) x :: [GADT.Some TyNameRep]
     type ToBinds uni acc x = ToBinds uni acc (ElaborateBuiltin uni x)
 
-    -- | Return the Plutus counterpart of the @x@ type.
-    toTypeAst :: proxy x -> Type tyname uni ()
-    default toTypeAst
-        :: KnownTypeAst tyname uni (ElaborateBuiltin uni x) => proxy x -> Type tyname uni ()
-    toTypeAst _ = toTypeAst (Proxy @(ElaborateBuiltin uni x))
-    {-# INLINE toTypeAst #-}
+    -- Doesn't take a @proxy@, so that newtype- and via-deriving are available.
+    -- | The Plutus counterpart of the @x@ type.
+    typeAst :: Type tyname uni ()
+    default typeAst :: KnownTypeAst tyname uni (ElaborateBuiltin uni x) => Type tyname uni ()
+    typeAst = toTypeAst $ Proxy @(ElaborateBuiltin uni x)
+    {-# INLINE typeAst #-}
 
 instance KnownTypeAst tyname uni a => KnownTypeAst tyname uni (EvaluationResult a) where
     type IsBuiltin _ (EvaluationResult a) = 'False
     type ToHoles _ (EvaluationResult a) = '[TypeHole a]
     type ToBinds uni acc (EvaluationResult a) = ToBinds uni acc a
-    toTypeAst _ = toTypeAst $ Proxy @a
-    {-# INLINE toTypeAst #-}
+    typeAst = toTypeAst $ Proxy @a
+    {-# INLINE typeAst #-}
 
 instance KnownTypeAst tyname uni a => KnownTypeAst tyname uni (BuiltinResult a) where
     type IsBuiltin _ (BuiltinResult a) = 'False
     type ToHoles _ (BuiltinResult a) = '[TypeHole a]
     type ToBinds uni acc (BuiltinResult a) = ToBinds uni acc a
-    toTypeAst _ = toTypeAst $ Proxy @a
-    {-# INLINE toTypeAst #-}
+    typeAst = toTypeAst $ Proxy @a
+    {-# INLINE typeAst #-}
 
 instance KnownTypeAst tyname uni a => KnownTypeAst tyname uni (Emitter a) where
     type IsBuiltin _ (Emitter a) = 'False
     type ToHoles _ (Emitter a) = '[TypeHole a]
     type ToBinds uni acc (Emitter a) = ToBinds uni acc a
-    toTypeAst _ = toTypeAst $ Proxy @a
-    {-# INLINE toTypeAst #-}
+    typeAst = toTypeAst $ Proxy @a
+    {-# INLINE typeAst #-}
 
 instance KnownTypeAst tyname uni rep => KnownTypeAst tyname uni (SomeConstant uni rep) where
     type IsBuiltin _ (SomeConstant uni rep) = 'False
     type ToHoles _ (SomeConstant _ rep) = '[RepHole rep]
     type ToBinds uni acc (SomeConstant _ rep) = ToBinds uni acc rep
-    toTypeAst _ = toTypeAst $ Proxy @rep
-    {-# INLINE toTypeAst #-}
+    typeAst = toTypeAst $ Proxy @rep
+    {-# INLINE typeAst #-}
 
 instance KnownTypeAst tyname uni rep => KnownTypeAst tyname uni (Opaque val rep) where
     type IsBuiltin _ (Opaque val rep) = 'False
     type ToHoles _ (Opaque _ rep) = '[RepHole rep]
     type ToBinds uni acc (Opaque _ rep) = ToBinds uni acc rep
-    toTypeAst _ = toTypeAst $ Proxy @rep
-    {-# INLINE toTypeAst #-}
+    typeAst = toTypeAst $ Proxy @rep
+    {-# INLINE typeAst #-}
+
+-- | Return the Plutus counterpart of the @x@ type.
+toTypeAst
+    :: forall a tyname uni (x :: a) proxy. KnownTypeAst tyname uni x
+    => proxy x -> Type tyname uni ()
+toTypeAst _ = typeAst @_ @tyname @uni @x
+{-# INLINE toTypeAst #-}
 
 toTyNameAst
     :: forall text uniq. (KnownSymbol text, KnownNat uniq)
@@ -265,32 +273,32 @@ instance uni `Contains` f => KnownTypeAst tyname uni (BuiltinHead f) where
     type IsBuiltin _ (BuiltinHead f) = 'True
     type ToHoles _ (BuiltinHead f) = '[]
     type ToBinds _ acc (BuiltinHead f) = acc
-    toTypeAst _ = TyBuiltin () $ someType @_ @f
-    {-# INLINE toTypeAst #-}
+    typeAst = TyBuiltin () $ someType @_ @f
+    {-# INLINE typeAst #-}
 
 instance (KnownTypeAst tyname uni a, KnownTypeAst tyname uni b) =>
         KnownTypeAst tyname uni (a -> b) where
     type IsBuiltin _ (a -> b) = 'False
     type ToHoles _ (a -> b) = '[TypeHole a, TypeHole b]
     type ToBinds uni acc (a -> b) = ToBinds uni (ToBinds uni acc a) b
-    toTypeAst _ = TyFun () (toTypeAst $ Proxy @a) (toTypeAst $ Proxy @b)
-    {-# INLINE toTypeAst #-}
+    typeAst = TyFun () (toTypeAst $ Proxy @a) (toTypeAst $ Proxy @b)
+    {-# INLINE typeAst #-}
 
 instance (tyname ~ TyName, name ~ 'TyNameRep text uniq, KnownSymbol text, KnownNat uniq) =>
             KnownTypeAst tyname uni (TyVarRep name) where
     type IsBuiltin _ (TyVarRep name) = 'False
     type ToHoles _ (TyVarRep name) = '[]
     type ToBinds _ acc (TyVarRep name) = Insert ('GADT.Some name) acc
-    toTypeAst _ = TyVar () . toTyNameAst $ Proxy @('TyNameRep text uniq)
-    {-# INLINE toTypeAst #-}
+    typeAst = TyVar () . toTyNameAst $ Proxy @('TyNameRep text uniq)
+    {-# INLINE typeAst #-}
 
 instance (KnownTypeAst tyname uni fun, KnownTypeAst tyname uni arg) =>
         KnownTypeAst tyname uni (TyAppRep fun arg) where
     type IsBuiltin uni (TyAppRep fun arg) = IsBuiltin uni fun && IsBuiltin uni arg
     type ToHoles _ (TyAppRep fun arg) = '[RepHole fun, RepHole arg]
     type ToBinds uni acc (TyAppRep fun arg) = ToBinds uni (ToBinds uni acc fun) arg
-    toTypeAst _ = TyApp () (toTypeAst $ Proxy @fun) (toTypeAst $ Proxy @arg)
-    {-# INLINE toTypeAst #-}
+    typeAst = TyApp () (toTypeAst $ Proxy @fun) (toTypeAst $ Proxy @arg)
+    {-# INLINE typeAst #-}
 
 instance
         ( tyname ~ TyName, name ~ 'TyNameRep @kind text uniq, KnownSymbol text, KnownNat uniq
@@ -299,12 +307,12 @@ instance
     type IsBuiltin _ (TyForallRep name a) = 'False
     type ToHoles _ (TyForallRep name a) = '[RepHole a]
     type ToBinds uni acc (TyForallRep name a) = Delete ('GADT.Some name) (ToBinds uni acc a)
-    toTypeAst _ =
+    typeAst =
         TyForall ()
             (toTyNameAst $ Proxy @('TyNameRep text uniq))
             (demoteKind $ knownKind @kind)
             (toTypeAst $ Proxy @a)
-    {-# INLINE toTypeAst #-}
+    {-# INLINE typeAst #-}
 
 -- Utils