[Builtins] Polish handling of integral types (#6036)

This

- adds support for throwing operational unlifting errors in the builtins machinery, which allows us to attach a message to an unlifting failure. Unfortunately this is still not enough to propagate proper error messages to the user, because they get erased by the evaluation machinery down the line, this is our 2018's legacy of the stupid idea to have raw evaluation failures that don't carry any content
- makes handling of integral types in `PlutusCore.Default.Universe` uniform (it was a mess before with a weird partial set of instances and morally the same instances being implemented differently)

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

@@ -119,6 +119,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