{-# 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 structural operational.
structural -> EvaluationError structural operational
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 #-}