{-# LANGUAGE BlockArguments #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE StrictData #-} module PlutusCore.Builtin.KnownType ( BuiltinError , throwBuiltinErrorWithCause , KnownBuiltinTypeIn , KnownBuiltinType , BuiltinResult (..) , ReadKnownM , MakeKnownIn (..) , readKnownConstant , MakeKnown , ReadKnownIn (..) , ReadKnown , makeKnownOrFail , readKnownSelf ) where import PlutusPrelude import PlutusCore.Builtin.HasConstant import PlutusCore.Builtin.Polymorphism import PlutusCore.Builtin.Result import PlutusCore.Core import PlutusCore.Evaluation.ErrorWithCause import PlutusCore.Evaluation.Result import PlutusCore.Pretty import Data.Either.Extras import Data.String import GHC.Exts (inline, oneShot) import GHC.TypeLits import Universe -- | A constraint for \"@a@ is a 'ReadKnownIn' and 'MakeKnownIn' by means of being included -- in @uni@\". type KnownBuiltinTypeIn uni val a = (HasConstantIn uni val, PrettyParens (SomeTypeIn uni), GEq uni, uni `HasTermLevel` a) -- | A constraint for \"@a@ is a 'ReadKnownIn' and 'MakeKnownIn' by means of being included -- in @UniOf term@\". type KnownBuiltinType val a = KnownBuiltinTypeIn (UniOf val) val a {- Note [Performance of ReadKnownIn and MakeKnownIn instances] It's critically important that 'readKnown' runs in the concrete 'Either' rather than a general 'MonadError'. Changing from the latter to the former gave us a speedup of up to 19%, see https://github.com/IntersectMBO/plutus/pull/4307 Replacing the @AsUnliftingError err, AsEvaluationFailure err@ constraints with the dedicated 'BuiltinError' data type gave us a speedup of up to 4%. All the same considerations apply to 'makeKnown': https://github.com/IntersectMBO/plutus/pull/4421 It's beneficial to inline 'readKnown' and 'makeKnown' not only because we use them directly over concrete types once 'toBuiltinsRuntime' is inlined, but also because otherwise GHC compiles each of them to two definitions (one calling the other) for some reason. So always add an @INLINE@ pragma to all definitions of 'makeKnown' and 'readKnown' unless you have a specific reason not to. Neither 'readKnown' nor 'makeKnown' should appear in the generated Core for builtins. In most cases they would slow builtins down, but even if a 'readKnown' only throws an error, it still makes sense to keep it out of Core just not to trigger an investigation on whether it's fine that a call to 'readKnown' is not inlined. Some 'readKnown' implementations require inserting a call to 'oneShot'. E.g. if 'oneShot' is not used in 'readKnownConstant' then 'GHC pulls @gshow uniExp@ out of the 'Nothing' branch, thus allocating a thunk of type 'String' that is completely redundant whenever there's no error, which is the majority of cases. And putting 'oneShot' as the outermost call results in worse Core. Any change to an instance of 'ReadKnownIn' or 'MakeKnownIn', even completely trivial, requires looking into the generated Core, since compilation of these instances is extremely brittle optimization-wise. Things to watch out for are unnecessary sharing (for example, a @let@ appearing outside of a @case@ allocates a thunk and if that thunk is not referenced inside of one of the branches, then it's wasteful, especially when it's not referenced in the most commonly chosen branch) and type class methods not being extracted from the dictionary and used directly instead (i.e. if you see multiple @pure@ and @>>=@ in the code, that's not good). Note that neither @let@ nor @>>=@ are bad in general, we certainly do need to allocate thunks occasionally, it's just that when it comes to builtins this is rarely the case as most of the time we want aggressive inlining and specialization and the "just compute the damn thing" behavior. -} {- Note [Unlifting terminology] This function: f :: Integer -> CkValue DefaultUni fun f = VCon . Some . ValueOf DefaultUniInteger lifts an 'Integer' to 'CkValue'. Unlifting is the opposite: g :: CkValue DefaultUni fun -> Maybe Integer g (VCon (Some (ValueOf uni x))) = case uni of DefaultUniInteger -> Just x _ -> Nothing The following usages of the "unlift" term are grammatical: 1. unlift a 'CkValue' to 'Integer' 2. unlift to 'Integer' 3. unlift a 'CkValue' as an 'Integer' 4. unlift from the 'VCon' constructor (or just 'VCon') to 'Integer' We call the integer that @g@ returns "the unlifted integer". -} {- Note [Unlifting a term as a value of a built-in type] See Note [Unlifting terminology] first. It's trivial to unlift a term to a monomorphic built-in type like 'Integer': just check that the term is a constant, extract the type tag and check it for equality with the type tag of 'Integer'. Things work the same way for a fully monomorphized polymorphic type, i.e. @(Integer, Bool@) is not any different from just 'Integer' unlifting-wise. (TODO: the following explanation needs to be improved, there's PLT-338 for that) However there's no sensible way of unlifting to, say, @[a]@ where @a@ in not a built-in type. So let's say we instantiated @a@ to an @Opaque val rep@ like we do for polymorphic functions that don't deal with polymorphic built-in types (e.g. @id@, @ifThenElse@ etc). That would mean we'd need to write a function from a @[a]@ for some arbitrary built-in @a@ to @[Opaque val a]@. Which is really easy to do: it's just @map makeKnown@. But the problem is, unlifting is supposed to be cheap and that @map@ is O(n), so for example 'MkCons' would become an O(n) operation making perfectly linear algorithms quadratic. See https://github.com/IntersectMBO/plutus/pull/4215 for how that would look like. So the problem is that we can't convert in O(1) time a @[a]@ coming from a constant of statically-unknown type (that @a@ is existential) to @[a']@ where @a'@ is known statically. Thus it's impossible to instantiate @a@ in Haskell's nullList :: [a] -> Bool so that there's a 'TypeScheme' for this function. One non-solution would be to instantiate @a@, then recurse on the type, construct a new function that defers to the original @nullList@ but wraps its argument in a specific way (more on that below) making it possible to assign a 'TypeScheme' to the resulting function. Astonishingly enough, that could actually work and if we ever write a paper on builtins, we should mention that example, but: 1. such a trick requires a generic machinery that knows how to check that the head of the builtin application is a particular built-in type. We used to have that, but it was just way too slow 2. that would only work for functions that don't care about @a@ at all. But for example when elaborating @cons :: a -> [a] -> [a]@ as a Plutus builtin we need to unlift both the arguments and check that their @a@s are equal (See Note [Representable built-in functions over polymorphic built-in types]) and it's either way too complex or even impossible to do that automatically within some generic machinery So what we do is we simply require the user to write nullList :: SomeConstant uni [a] -> Bool and unlift to @[a]@ manually within the definition of the builtin. This works, because the existential @a@ never escapes the definition of the builtin. I.e. it's fine to unpack an existential and use it immediately without ever exposing the existential parts to the outside and it's not fine to try to return a value having an existential inside of it, which is what unlifting to @[a]@ would amount to. Could we somehow align the unlifting machinery so that it does not construct values of particular types, but rather feeds them to a continuation or something, so that the existential parts never try to escape? Maybe, but see point 2 from the above, we do want to get our hands on the particular universes sometimes and point 1 prevents us from doing that generically, so it doesn't seem like we could do that within some automated machinery. Overall, asking the user to manually unlift a @SomeConstant uni [a]@ is just always going to be faster than any kind of fancy encoding. -} {- Note [Alignment of ReadKnownIn and MakeKnownIn] We keep 'ReadKnownIn' and 'MakeKnownIn' separate, because values of some types can only be lifted and not unlifted, for example 'EvaluationResult' and 'Emitter' can't appear in argument position. 'KnownTypeAst' is not a superclass of ReadKnownIn and MakeKnownIn. This is due to the fact that polymorphic built-in types are only liftable/unliftable when they're fully monomorphized, while 'toTypeAst' works for polymorphic built-in types that have type variables in them, and so the constraints are completely different in the two cases and we keep the two concepts apart (there doesn't seem to be any cons to that). -} {- Note [Allowed unlifting and lifting] Read Note [Alignment of ReadKnownIn and MakeKnownIn] first. The following classes of Haskell types represent Plutus types: 1. monomorphic built-in types such as @Bool@ (assuming @Bool@ is in the universe) 2. polymorphic built-in types such as @(a, b)@ for any @a@ and @b@ representing Plutus types (assuming @(,)@ is in the universe) 3. @Opaque val rep@ for any @rep@ representing a Plutus type 4. @SomeConstant uni rep@ for any @rep@ representing a Plutus type 5. @Emitter a@ for any @a@ representing a Plutus type 6. @EvaluationResult a@ for any @a@ representing a Plutus type 7. 'TyVarRep', 'TyAppRep', 'TyForallRep' and all similar types mirroring constructors of @Type@ 8. @a -> b@ for any @a@ and @b@ representing Plutus types (mirrors 'TyFun') 9. anything else that has a 'KnownTypeAst' instance, for example we express the @KnownTypeAst DefaultUni Int@ instance in terms of the @KnownType DefaultUni Integer@ one Unlifting is allowed to the following classes of types: 1. monomorphic built-in types such as @Bool@ 2. monomorphized polymorphic built-in types such as @(Integer, Text)@ 3. @Opaque val rep@ for @rep@ representing a Plutus type 4. @SomeConstant uni rep@ for @rep@ representing a Plutus type 5. anything else that implements 'ReadKnownIn', for example we express the @ReadKnownIn DefaultUni term Int@ instance in terms of the @ReadKnownIn DefaultUni term Integer@ one, and for another example define an instance for 'Void' in tests Lifting is allowed to the following classes of types: 1. monomorphic built-in types such as @Bool@ 2. monomorphized polymorphic built-in types such as @(Integer, Text)@ 3. @Opaque val rep@ for @rep@ representing a Plutus type 4. @SomeConstant uni rep@ for @rep@ representing a Plutus type 5. @Emitter a@ for any @a@ that lifting is allowed to 6. @EvaluationResult a@ for any @a@ that lifting is allowed to 7. anything else that implements 'MakeKnownIn', for example we express the @MakeKnownIn DefaultUni term Int@ instance in terms of the @MakeKnownIn DefaultUni term Integer@ one, and for another example define an instance for 'Void' in tests -} typeMismatchError :: PrettyParens (SomeTypeIn uni) => uni (Esc a) -> uni (Esc b) -> UnliftingEvaluationError typeMismatchError :: forall (uni :: * -> *) a b. PrettyParens (SomeTypeIn uni) => uni (Esc a) -> uni (Esc b) -> UnliftingEvaluationError typeMismatchError uni (Esc a) uniExp uni (Esc b) uniAct = EvaluationError UnliftingError UnliftingError -> UnliftingEvaluationError MkUnliftingEvaluationError (EvaluationError UnliftingError UnliftingError -> UnliftingEvaluationError) -> ([Char] -> EvaluationError UnliftingError UnliftingError) -> [Char] -> UnliftingEvaluationError forall b c a. (b -> c) -> (a -> b) -> a -> c . UnliftingError -> EvaluationError UnliftingError UnliftingError forall operational structural. structural -> EvaluationError operational structural StructuralEvaluationError (UnliftingError -> EvaluationError UnliftingError UnliftingError) -> ([Char] -> UnliftingError) -> [Char] -> EvaluationError UnliftingError UnliftingError forall b c a. (b -> c) -> (a -> b) -> a -> c . [Char] -> UnliftingError forall a. IsString a => [Char] -> a fromString ([Char] -> UnliftingEvaluationError) -> [Char] -> UnliftingEvaluationError forall a b. (a -> b) -> a -> b $ [[Char]] -> [Char] forall (t :: * -> *) a. Foldable t => t [a] -> [a] concat [ [Char] "Type mismatch: " , [Char] "expected: " [Char] -> [Char] -> [Char] forall a. [a] -> [a] -> [a] ++ RenderContext -> SomeTypeIn uni -> [Char] forall str a config. (PrettyBy config a, Render str) => config -> a -> str displayBy RenderContext botRenderContext (uni (Esc a) -> SomeTypeIn uni forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni SomeTypeIn uni (Esc a) uniExp) , [Char] "; actual: " [Char] -> [Char] -> [Char] forall a. [a] -> [a] -> [a] ++ RenderContext -> SomeTypeIn uni -> [Char] forall str a config. (PrettyBy config a, Render str) => config -> a -> str displayBy RenderContext botRenderContext (uni (Esc b) -> SomeTypeIn uni forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni SomeTypeIn uni (Esc b) uniAct) ] -- See Note [INLINE and OPAQUE on error-related definitions]. {-# OPAQUE typeMismatchError #-} -- Normally it's a good idea for an exported abstraction not to be a type synonym, since a @newtype@ -- is cheap, looks good in error messages and clearly emphasize an abstraction barrier. However we -- make 'ReadKnownM' a type synonym for convenience: that way we don't need to derive all the -- instances (and add new ones whenever we need them), wrap and unwrap all the time (including in -- user code), which can be non-trivial for such performance-sensitive code (see e.g. 'coerceVia' -- and 'coerceArg') and there is no abstraction barrier anyway. -- | The monad that 'readKnown' runs in. type ReadKnownM = Either BuiltinError -- See Note [Unlifting a term as a value of a built-in type]. -- | Convert a constant embedded into a PLC term to the corresponding Haskell value. readKnownConstant :: forall val a. KnownBuiltinType val a => val -> ReadKnownM a -- See Note [Performance of ReadKnownIn and MakeKnownIn instances] readKnownConstant :: forall val a. KnownBuiltinType val a => val -> ReadKnownM a readKnownConstant val val = val -> Either BuiltinError (Some (ValueOf (UniOf val))) forall term. HasConstant term => term -> Either BuiltinError (Some (ValueOf (UniOf term))) asConstant val val Either BuiltinError (Some (ValueOf (UniOf val))) -> (Some (ValueOf (UniOf val)) -> Either BuiltinError a) -> Either BuiltinError a forall a b. Either BuiltinError a -> (a -> Either BuiltinError b) -> Either BuiltinError b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= (Some (ValueOf (UniOf val)) -> Either BuiltinError a) -> Some (ValueOf (UniOf val)) -> Either BuiltinError a forall a b. (a -> b) -> a -> b oneShot \case Some (ValueOf UniOf val (Esc a) uniAct a x) -> do let uniExp :: UniOf val (Esc a) uniExp = forall k (uni :: * -> *) (a :: k). Contains uni a => uni (Esc a) knownUni @_ @(UniOf val) @a -- 'geq' matches on its first argument first, so we make the type tag that will be known -- statically (because this function will be inlined) go first in order for GHC to -- optimize some of the matching away. case UniOf val (Esc a) uniExp UniOf val (Esc a) -> UniOf val (Esc a) -> Maybe (Esc a :~: Esc a) forall a b. UniOf val a -> UniOf val b -> Maybe (a :~: b) forall k (f :: k -> *) (a :: k) (b :: k). GEq f => f a -> f b -> Maybe (a :~: b) `geq` UniOf val (Esc a) uniAct of Just Esc a :~: Esc a Refl -> a -> Either BuiltinError a forall a. a -> Either BuiltinError a forall (f :: * -> *) a. Applicative f => a -> f a pure a a x Maybe (Esc a :~: Esc a) Nothing -> AReview BuiltinError UnliftingEvaluationError -> UnliftingEvaluationError -> Either BuiltinError a forall e (m :: * -> *) t x. MonadError e m => AReview e t -> t -> m x throwing AReview BuiltinError UnliftingEvaluationError forall r. AsUnliftingEvaluationError r => Prism' r UnliftingEvaluationError Prism' BuiltinError UnliftingEvaluationError _UnliftingEvaluationError (UnliftingEvaluationError -> Either BuiltinError a) -> UnliftingEvaluationError -> Either BuiltinError a forall a b. (a -> b) -> a -> b $ UniOf val (Esc a) -> UniOf val (Esc a) -> UnliftingEvaluationError forall (uni :: * -> *) a b. PrettyParens (SomeTypeIn uni) => uni (Esc a) -> uni (Esc b) -> UnliftingEvaluationError typeMismatchError UniOf val (Esc a) uniExp UniOf val (Esc a) uniAct {-# INLINE readKnownConstant #-} -- See Note [Performance of ReadKnownIn and MakeKnownIn instances]. class uni ~ UniOf val => MakeKnownIn uni val a where -- | Convert a Haskell value to the corresponding PLC value. -- The inverse of 'readKnown'. makeKnown :: a -> BuiltinResult val default makeKnown :: KnownBuiltinType val a => a -> BuiltinResult val -- Everything on evaluation path has to be strict in production, so in theory we don't need to -- force anything here. In practice however all kinds of weird things happen in tests and @val@ -- can be non-strict enough to cause trouble here, so we're forcing the argument. Looking at the -- generated Core, the forcing amounts to pulling a @case@ out of the 'fromConstant' call, -- which doesn't affect the overall cost and benchmarking results suggest the same. -- -- Note that the value is only forced to WHNF, so care must be taken to ensure that every value -- of a type from the universe gets forced to NF whenever it's forced to WHNF. makeKnown a x = val -> BuiltinResult val forall a. a -> BuiltinResult a forall (f :: * -> *) a. Applicative f => a -> f a pure (val -> BuiltinResult val) -> (a -> val) -> a -> BuiltinResult val forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> val forall a term. (HasConstant term, HasTermLevel (UniOf term) a) => a -> term fromValue (a -> BuiltinResult val) -> a -> BuiltinResult val forall a b. (a -> b) -> a -> b $! a x {-# INLINE makeKnown #-} type MakeKnown val = MakeKnownIn (UniOf val) val -- See Note [Performance of ReadKnownIn and MakeKnownIn instances]. class uni ~ UniOf val => ReadKnownIn uni val a where -- | Convert a PLC value to the corresponding Haskell value. -- The inverse of 'makeKnown'. readKnown :: val -> ReadKnownM a default readKnown :: KnownBuiltinType val a => val -> ReadKnownM a -- If 'inline' is not used, proper inlining does not happen for whatever reason. readKnown = (val -> ReadKnownM a) -> val -> ReadKnownM a forall a. a -> a inline val -> ReadKnownM a forall val a. KnownBuiltinType val a => val -> ReadKnownM a readKnownConstant {-# INLINE readKnown #-} type ReadKnown val = ReadKnownIn (UniOf val) val -- | Same as 'makeKnown', but allows for neither emitting nor storing the cause of a failure. makeKnownOrFail :: MakeKnownIn uni val a => a -> EvaluationResult val makeKnownOrFail :: forall (uni :: * -> *) val a. MakeKnownIn uni val a => a -> EvaluationResult val makeKnownOrFail a x = case a -> BuiltinResult val forall (uni :: * -> *) val a. MakeKnownIn uni val a => a -> BuiltinResult val makeKnown a x of BuiltinSuccess val val -> val -> EvaluationResult val forall a. a -> EvaluationResult a EvaluationSuccess val val BuiltinSuccessWithLogs DList Text _ val val -> val -> EvaluationResult val forall a. a -> EvaluationResult a EvaluationSuccess val val BuiltinFailure DList Text _ BuiltinError _ -> EvaluationResult val forall a. EvaluationResult a EvaluationFailure {-# INLINE makeKnownOrFail #-} -- | Same as 'readKnown', but the cause of a potential failure is the provided term itself. readKnownSelf :: (ReadKnown val a, AsUnliftingEvaluationError err, AsEvaluationFailure err) => val -> Either (ErrorWithCause err val) a readKnownSelf :: forall val a err. (ReadKnown val a, AsUnliftingEvaluationError err, AsEvaluationFailure err) => val -> Either (ErrorWithCause err val) a readKnownSelf val val = (BuiltinError -> Either (ErrorWithCause err val) a) -> Either BuiltinError a -> Either (ErrorWithCause err val) a forall (m :: * -> *) a b. Monad m => (a -> m b) -> Either a b -> m b fromRightM (val -> BuiltinError -> Either (ErrorWithCause err val) a forall err cause (m :: * -> *) void. (MonadError (ErrorWithCause err cause) m, AsUnliftingEvaluationError err, AsEvaluationFailure err) => cause -> BuiltinError -> m void throwBuiltinErrorWithCause val val) (Either BuiltinError a -> Either (ErrorWithCause err val) a) -> Either BuiltinError a -> Either (ErrorWithCause err val) a forall a b. (a -> b) -> a -> b $ val -> Either BuiltinError a forall (uni :: * -> *) val a. ReadKnownIn uni val a => val -> ReadKnownM a readKnown val val {-# INLINE readKnownSelf #-} instance MakeKnownIn uni val a => MakeKnownIn uni val (BuiltinResult a) where makeKnown :: BuiltinResult a -> BuiltinResult val makeKnown BuiltinResult a res = BuiltinResult a res BuiltinResult a -> (a -> BuiltinResult val) -> BuiltinResult val forall a b. BuiltinResult a -> (a -> BuiltinResult b) -> BuiltinResult b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= a -> BuiltinResult val forall (uni :: * -> *) val a. MakeKnownIn uni val a => a -> BuiltinResult val makeKnown {-# INLINE makeKnown #-} -- Catching 'EvaluationFailure' here would allow *not* to short-circuit when 'readKnown' fails -- to read a Haskell value of type @a@. Instead, in the denotation of the builtin function -- the programmer would be given an explicit 'EvaluationResult' value to handle, which means -- that when this value is 'EvaluationFailure', a PLC 'Error' was caught. -- I.e. it would essentially allow us to catch errors and handle them in a programmable way. -- We forbid this, because it complicates code and isn't supported by evaluation engines anyway. instance ( TypeError ('Text "‘BuiltinResult’ cannot appear in the type of an argument") , uni ~ UniOf val ) => ReadKnownIn uni val (BuiltinResult a) where readKnown :: val -> ReadKnownM (BuiltinResult a) readKnown val _ = ReadKnownM (BuiltinResult a) forall (m :: * -> *) void. MonadError BuiltinError m => m void throwUnderTypeError {-# INLINE readKnown #-} instance ( TypeError ('Text "Use ‘BuiltinResult’ instead of ‘EvaluationResult’") , uni ~ UniOf val ) => MakeKnownIn uni val (EvaluationResult a) where makeKnown :: EvaluationResult a -> BuiltinResult val makeKnown EvaluationResult a _ = BuiltinResult val forall (m :: * -> *) void. MonadError BuiltinError m => m void throwUnderTypeError {-# INLINE makeKnown #-} instance ( TypeError ('Text "Use ‘BuiltinResult’ instead of ‘EvaluationResult’") , uni ~ UniOf val ) => ReadKnownIn uni val (EvaluationResult a) where readKnown :: val -> ReadKnownM (EvaluationResult a) readKnown val _ = ReadKnownM (EvaluationResult a) forall (m :: * -> *) void. MonadError BuiltinError m => m void throwUnderTypeError {-# INLINE readKnown #-} instance HasConstantIn uni val => MakeKnownIn uni val (SomeConstant uni rep) where makeKnown :: SomeConstant uni rep -> BuiltinResult val makeKnown = (Some (ValueOf uni) -> BuiltinResult val) -> SomeConstant uni rep -> BuiltinResult val forall a b s. Coercible a b => (a -> s) -> b -> s coerceArg ((Some (ValueOf uni) -> BuiltinResult val) -> SomeConstant uni rep -> BuiltinResult val) -> (Some (ValueOf uni) -> BuiltinResult val) -> SomeConstant uni rep -> BuiltinResult val forall a b. (a -> b) -> a -> b $ val -> BuiltinResult val forall a. a -> BuiltinResult a forall (f :: * -> *) a. Applicative f => a -> f a pure (val -> BuiltinResult val) -> (Some (ValueOf uni) -> val) -> Some (ValueOf uni) -> BuiltinResult val forall b c a. (b -> c) -> (a -> b) -> a -> c . Some (ValueOf uni) -> val Some (ValueOf (UniOf val)) -> val forall term. HasConstant term => Some (ValueOf (UniOf term)) -> term fromConstant {-# INLINE makeKnown #-} instance HasConstantIn uni val => ReadKnownIn uni val (SomeConstant uni rep) where readKnown :: val -> ReadKnownM (SomeConstant uni rep) readKnown = ((val -> Either BuiltinError (Some (ValueOf uni))) -> val -> ReadKnownM (SomeConstant uni rep)) -> (val -> Either BuiltinError (Some (ValueOf uni))) -> val -> ReadKnownM (SomeConstant uni rep) forall a b. Coercible a b => (a -> b) -> a -> b coerceVia ((Some (ValueOf uni) -> SomeConstant uni rep) -> Either BuiltinError (Some (ValueOf uni)) -> ReadKnownM (SomeConstant uni rep) forall a b. (a -> b) -> Either BuiltinError a -> Either BuiltinError b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap Some (ValueOf uni) -> SomeConstant uni rep forall (uni :: * -> *) rep. Some (ValueOf uni) -> SomeConstant uni rep SomeConstant (Either BuiltinError (Some (ValueOf uni)) -> ReadKnownM (SomeConstant uni rep)) -> (val -> Either BuiltinError (Some (ValueOf uni))) -> val -> ReadKnownM (SomeConstant uni rep) forall b c a. (b -> c) -> (a -> b) -> a -> c .) val -> Either BuiltinError (Some (ValueOf uni)) val -> Either BuiltinError (Some (ValueOf (UniOf val))) forall term. HasConstant term => term -> Either BuiltinError (Some (ValueOf (UniOf term))) asConstant {-# INLINE readKnown #-} instance uni ~ UniOf val => MakeKnownIn uni val (Opaque val rep) where makeKnown :: Opaque val rep -> BuiltinResult val makeKnown = (val -> BuiltinResult val) -> Opaque val rep -> BuiltinResult val forall a b s. Coercible a b => (a -> s) -> b -> s coerceArg val -> BuiltinResult val forall a. a -> BuiltinResult a forall (f :: * -> *) a. Applicative f => a -> f a pure {-# INLINE makeKnown #-} instance uni ~ UniOf val => ReadKnownIn uni val (Opaque val rep) where readKnown :: val -> ReadKnownM (Opaque val rep) readKnown = (Opaque val rep -> ReadKnownM (Opaque val rep)) -> val -> ReadKnownM (Opaque val rep) forall a b s. Coercible a b => (a -> s) -> b -> s coerceArg Opaque val rep -> ReadKnownM (Opaque val rep) forall a. a -> Either BuiltinError a forall (f :: * -> *) a. Applicative f => a -> f a pure {-# INLINE readKnown #-}