-- | The universe used by default and its instances.

{-# OPTIONS -fno-warn-missing-pattern-synonym-signatures #-}

{-# LANGUAGE BlockArguments        #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

-- effectfully: to the best of my experimentation, -O2 here improves performance, however by
-- inspecting GHC Core I was only able to see a difference in how the 'KnownTypeIn' instance for
-- 'Int' is compiled (one more call is inlined with -O2). This needs to be investigated.
{-# OPTIONS_GHC -O2 #-}

module PlutusCore.Default.Universe
    ( DefaultUni (..)
    , pattern DefaultUniList
    , pattern DefaultUniPair
    , module Export  -- Re-exporting universes infrastructure for convenience.
    ) where

import PlutusCore.Builtin
import PlutusCore.Data
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Result

import Control.Applicative
import Data.ByteString qualified as BS
import Data.Int
import Data.IntCast (intCastEq)
import Data.Proxy
import Data.Text qualified as Text
import GHC.Exts (inline, oneShot)
import Universe as Export

{- Note [PLC types and universes]
We encode built-in types in PLC as tags for Haskell types (the latter are also called meta-types),
see Note [Universes]. A built-in type in PLC is an inhabitant of

    Some (TypeIn uni)

where @uni@ is some universe, i.e. a collection of tags that have meta-types associated with them.

A value of a built-in type is a regular Haskell value stored in

    Some (ValueOf uni)

(together with the tag associated with its type) and such a value is also called a meta-constant.

The default universe has the following constructor (pattern synonym actually):

    DefaultUniList :: !(DefaultUni a) -> DefaultUni [a]

But note that this doesn't directly lead to interop between Plutus Core and Haskell, i.e. you can't
have a meta-list whose elements are of a PLC type. You can only have a meta-list constant with
elements of a meta-type (i.e. a type from the universe).

However it is possible to apply a built-in type to an arbitrary PLC/PIR type, since we can embed
a type of an arbitrary kind into 'Type' and then apply it via 'TyApp'. But we only use it to
get polymorphic built-in functions over polymorphic built-in types, since it's not possible
to juggle values of polymorphic built-in types instantiated with non-built-in types at runtime
(it's not even possible to represent such a value in the AST, even though it's possible to represent
such a 'Type').

Finally, it is not necessarily the case that we need to allow embedding PLC terms into meta-constants.
We already allow built-in functions with polymorphic types. There might be a way to utilize this
feature and have meta-constructors as built-in functions.
-}

-- See Note [Representing polymorphism].
-- | The universe used by default.
data DefaultUni a where
    DefaultUniInteger    :: DefaultUni (Esc Integer)
    DefaultUniByteString :: DefaultUni (Esc BS.ByteString)
    DefaultUniString     :: DefaultUni (Esc Text.Text)
    DefaultUniUnit       :: DefaultUni (Esc ())
    DefaultUniBool       :: DefaultUni (Esc Bool)
    DefaultUniProtoList  :: DefaultUni (Esc [])
    DefaultUniProtoPair  :: DefaultUni (Esc (,))
    DefaultUniApply      :: !(DefaultUni (Esc f)) -> !(DefaultUni (Esc a)) -> DefaultUni (Esc (f a))
    DefaultUniData       :: DefaultUni (Esc Data)

-- GHC infers crazy types for these two and the straightforward ones break pattern matching,
-- so we just leave GHC with its craziness.
pattern $bDefaultUniList :: DefaultUni (Esc a1) -> DefaultUni a
$mDefaultUniList :: forall r a.
DefaultUni a
-> (forall k1 k2 (f :: k1 -> k2) (a1 :: k1).
    (a ~ Esc (f a1), Esc f ~ Esc []) =>
    DefaultUni (Esc a1) -> r)
-> (Void# -> r)
-> r
DefaultUniList uniA =
    DefaultUniProtoList `DefaultUniApply` uniA
pattern $bDefaultUniPair :: DefaultUni (Esc a2) -> DefaultUni (Esc a1) -> DefaultUni a
$mDefaultUniPair :: forall r a.
DefaultUni a
-> (forall k1 k2 (f1 :: k1 -> k2) (a1 :: k1) k3 k4 (f2 :: k3 -> k4)
           (a2 :: k3).
    (a ~ Esc (f1 a1), Esc f1 ~ Esc (f2 a2), Esc f2 ~ Esc (,)) =>
    DefaultUni (Esc a2) -> DefaultUni (Esc a1) -> r)
-> (Void# -> r)
-> r
DefaultUniPair uniA uniB =
    DefaultUniProtoPair `DefaultUniApply` uniA `DefaultUniApply` uniB

deriveGEq ''DefaultUni
deriveGCompare ''DefaultUni

-- | For pleasing the coverage checker.
noMoreTypeFunctions :: DefaultUni (Esc (f :: a -> b -> c -> d)) -> any
noMoreTypeFunctions :: DefaultUni (Esc f) -> any
noMoreTypeFunctions (DefaultUni (Esc f)
f `DefaultUniApply` DefaultUni (Esc a)
_) = DefaultUni (Esc f) -> any
forall a b c d (f :: a -> b -> c -> d) any.
DefaultUni (Esc f) -> any
noMoreTypeFunctions DefaultUni (Esc f)
DefaultUni (Esc f)
f

instance ToKind DefaultUni where
    toSingKind :: DefaultUni (Esc a) -> SingKind k
toSingKind DefaultUni (Esc a)
DefaultUniInteger        = SingKind k
forall k. KnownKind k => SingKind k
knownKind
    toSingKind DefaultUni (Esc a)
DefaultUniByteString     = SingKind k
forall k. KnownKind k => SingKind k
knownKind
    toSingKind DefaultUni (Esc a)
DefaultUniString         = SingKind k
forall k. KnownKind k => SingKind k
knownKind
    toSingKind DefaultUni (Esc a)
DefaultUniUnit           = SingKind k
forall k. KnownKind k => SingKind k
knownKind
    toSingKind DefaultUni (Esc a)
DefaultUniBool           = SingKind k
forall k. KnownKind k => SingKind k
knownKind
    toSingKind DefaultUni (Esc a)
DefaultUniProtoList      = SingKind k
forall k. KnownKind k => SingKind k
knownKind
    toSingKind DefaultUni (Esc a)
DefaultUniProtoPair      = SingKind k
forall k. KnownKind k => SingKind k
knownKind
    toSingKind (DefaultUniApply DefaultUni (Esc f)
uniF DefaultUni (Esc a)
_) = case DefaultUni (Esc f) -> SingKind (k -> k)
forall (uni :: * -> *) k (a :: k).
ToKind uni =>
uni (Esc a) -> SingKind k
toSingKind DefaultUni (Esc f)
uniF of SingKind k
_ `SingKindArrow` SingKind l
cod -> SingKind k
SingKind l
cod
    toSingKind DefaultUni (Esc a)
DefaultUniData           = SingKind k
forall k. KnownKind k => SingKind k
knownKind

instance HasUniApply DefaultUni where
    matchUniApply :: DefaultUni tb
-> r
-> (forall k l (f :: k -> l) (a :: k).
    (tb ~ Esc (f a)) =>
    DefaultUni (Esc f) -> DefaultUni (Esc a) -> r)
-> r
matchUniApply (DefaultUniApply DefaultUni (Esc f)
f DefaultUni (Esc a)
a) r
_ forall k l (f :: k -> l) (a :: k).
(tb ~ Esc (f a)) =>
DefaultUni (Esc f) -> DefaultUni (Esc a) -> r
h = DefaultUni (Esc f) -> DefaultUni (Esc a) -> r
forall k l (f :: k -> l) (a :: k).
(tb ~ Esc (f a)) =>
DefaultUni (Esc f) -> DefaultUni (Esc a) -> r
h DefaultUni (Esc f)
f DefaultUni (Esc a)
a
    matchUniApply DefaultUni tb
_                     r
z forall k l (f :: k -> l) (a :: k).
(tb ~ Esc (f a)) =>
DefaultUni (Esc f) -> DefaultUni (Esc a) -> r
_ = r
z

instance GShow DefaultUni where gshowsPrec :: Int -> DefaultUni a -> ShowS
gshowsPrec = Int -> DefaultUni a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec
instance Show (DefaultUni a) where
    show :: DefaultUni a -> String
show DefaultUni a
DefaultUniInteger             = String
"integer"
    show DefaultUni a
DefaultUniByteString          = String
"bytestring"
    show DefaultUni a
DefaultUniString              = String
"string"
    show DefaultUni a
DefaultUniUnit                = String
"unit"
    show DefaultUni a
DefaultUniBool                = String
"bool"
    show DefaultUni a
DefaultUniProtoList           = String
"list"
    show DefaultUni a
DefaultUniProtoPair           = String
"pair"
    show (DefaultUni (Esc f)
uniF `DefaultUniApply` DefaultUni (Esc a)
uniB) = case DefaultUni (Esc f)
uniF of
        DefaultUni (Esc f)
DefaultUniProtoList                          -> [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"list (", DefaultUni (Esc a) -> String
forall a. Show a => a -> String
show DefaultUni (Esc a)
uniB, String
")"]
        DefaultUni (Esc f)
DefaultUniProtoPair                          -> [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"pair (", DefaultUni (Esc a) -> String
forall a. Show a => a -> String
show DefaultUni (Esc a)
uniB, String
")"]
        DefaultUni (Esc f)
DefaultUniProtoPair `DefaultUniApply` DefaultUni (Esc a)
uniA   -> [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"pair (", DefaultUni (Esc a) -> String
forall a. Show a => a -> String
show DefaultUni (Esc a)
uniA, String
") (", DefaultUni (Esc a) -> String
forall a. Show a => a -> String
show DefaultUni (Esc a)
uniB, String
")"]
        DefaultUni (Esc f)
uniG `DefaultUniApply` DefaultUni (Esc a)
_ `DefaultUniApply` DefaultUni (Esc a)
_ -> DefaultUni (Esc f) -> String
forall a b c d (f :: a -> b -> c -> d) any.
DefaultUni (Esc f) -> any
noMoreTypeFunctions DefaultUni (Esc f)
DefaultUni (Esc f)
uniG
    show DefaultUni a
DefaultUniData = String
"data"

instance DefaultUni `Contains` Integer       where knownUni :: DefaultUni (Esc Integer)
knownUni = DefaultUni (Esc Integer)
DefaultUniInteger
instance DefaultUni `Contains` BS.ByteString where knownUni :: DefaultUni (Esc ByteString)
knownUni = DefaultUni (Esc ByteString)
DefaultUniByteString
instance DefaultUni `Contains` Text.Text     where knownUni :: DefaultUni (Esc Text)
knownUni = DefaultUni (Esc Text)
DefaultUniString
instance DefaultUni `Contains` ()            where knownUni :: DefaultUni (Esc ())
knownUni = DefaultUni (Esc ())
DefaultUniUnit
instance DefaultUni `Contains` Bool          where knownUni :: DefaultUni (Esc Bool)
knownUni = DefaultUni (Esc Bool)
DefaultUniBool
instance DefaultUni `Contains` []            where knownUni :: DefaultUni (Esc [])
knownUni = DefaultUni (Esc [])
DefaultUniProtoList
instance DefaultUni `Contains` (,)           where knownUni :: DefaultUni (Esc (,))
knownUni = DefaultUni (Esc (,))
DefaultUniProtoPair
instance DefaultUni `Contains` Data          where knownUni :: DefaultUni (Esc Data)
knownUni = DefaultUni (Esc Data)
DefaultUniData

instance (DefaultUni `Contains` f, DefaultUni `Contains` a) => DefaultUni `Contains` f a where
    knownUni :: DefaultUni (Esc (f a))
knownUni = DefaultUni (Esc f)
forall k (uni :: * -> *) (a :: k). Contains uni a => uni (Esc a)
knownUni DefaultUni (Esc f) -> DefaultUni (Esc a) -> DefaultUni (Esc (f a))
forall k k (f :: k -> k) (a :: k).
DefaultUni (Esc f) -> DefaultUni (Esc a) -> DefaultUni (Esc (f a))
`DefaultUniApply` DefaultUni (Esc a)
forall k (uni :: * -> *) (a :: k). Contains uni a => uni (Esc a)
knownUni

instance KnownBuiltinTypeAst DefaultUni Integer       => KnownTypeAst DefaultUni Integer
instance KnownBuiltinTypeAst DefaultUni BS.ByteString => KnownTypeAst DefaultUni BS.ByteString
instance KnownBuiltinTypeAst DefaultUni Text.Text     => KnownTypeAst DefaultUni Text.Text
instance KnownBuiltinTypeAst DefaultUni ()            => KnownTypeAst DefaultUni ()
instance KnownBuiltinTypeAst DefaultUni Bool          => KnownTypeAst DefaultUni Bool
instance KnownBuiltinTypeAst DefaultUni [a]           => KnownTypeAst DefaultUni [a]
instance KnownBuiltinTypeAst DefaultUni (a, b)        => KnownTypeAst DefaultUni (a, b)
instance KnownBuiltinTypeAst DefaultUni Data          => KnownTypeAst DefaultUni Data

{- Note [Constraints of ReadKnownIn and MakeKnownIn instances]
For a monomorphic data type @X@ one only needs to add a @HasConstantIn DefaultUni term@ constraint
in order to be able to provide a @ReadTypeIn DefaultUni term X@ instance and the same applies to
'MakeKnownIn'.

For a polymorphic data type @Y@ in addition to the same @HasConstantIn DefaultUni term@ constraint
one also needs to add @DefaultUni `Contains` Y@, where @Y@ contains all of its type variables.

See the reference site of this Note for examples.

The difference is due to the fact that for any monomorphic type @X@ the @DefaultUni `Contains` X@
constraint can be discharged statically, so we don't need it to provide the instance, while in
the polymorphic case whether @Y@ is in the universe or not depends on whether its type arguments are
in the universe or not, so the @DefaultUni `Contains` Y@ constraint can't be discharged statically.

Could we still provide @DefaultUni `Contains` X@ even though it's redundant? That works, but then
GHC does not attempt to discharge it statically and takes the type tag needed for unlifting from
the provided constraint rather than the global scope, which makes the code measurably slower.

Could we at least hide the discrepancy behind a type family? Unfortunately, that generates worse
Core as some things don't get inlined properly. Somehow GHC is not able to see through the type
family that it fully reduces anyway.

Finally, instead of writing @DefaultUni `Contains` Y@ we could write @DefaultUni `Contains` a@
for each argument type @a@ in @Y@ (because that implies @DefaultUni `Contains` Y@), however GHC
creates a redundant @let@ in that case (@-fno-cse@ or some other technique for preventing GHC from
doing CSE may solve that problem). For now we do the simplest thing and just write
@DefaultUni `Contains` Y@.

A call to 'geq' does not get inlined due to 'geq' being recursive. It's an obvious inefficiency and
one that can be fixed, see https://github.com/input-output-hk/plutus/pull/4462
It's some pretty annoying boilerplate and for now we've decided it's not worth it.
-}

-- See Note [Constraints of ReadKnownIn and MakeKnownIn instances].
instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term Integer
instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term BS.ByteString
instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term Text.Text
instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term ()
instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term Bool
instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term Data
instance (HasConstantIn DefaultUni term, DefaultUni `Contains` [a]) =>
    MakeKnownIn DefaultUni term [a]
instance (HasConstantIn DefaultUni term, DefaultUni `Contains` (a, b)) =>
    MakeKnownIn DefaultUni term (a, b)

-- See Note [Constraints of ReadKnownIn and MakeKnownIn instances].
instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term Integer
instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term BS.ByteString
instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term Text.Text
instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term ()
instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term Bool
instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term Data
instance (HasConstantIn DefaultUni term, DefaultUni `Contains` [a]) =>
    ReadKnownIn DefaultUni term [a]
instance (HasConstantIn DefaultUni term, DefaultUni `Contains` (a, b)) =>
    ReadKnownIn DefaultUni term (a, b)

-- If this tells you an instance is missing, add it right above, following the pattern.
instance TestTypesFromTheUniverseAreAllKnown DefaultUni

{- Note [Int as Integer]
Technically our universe only contains 'Integer', but many of the builtin functions that we would
like to use work over 'Int'.

This is inconvenient and also error-prone: dealing with a function that takes an 'Int' means carefully
downcasting the 'Integer', running the function, potentially upcasting at the end. And it's easy to get
wrong by e.g. blindly using 'fromInteger'.

Moreover, there is a latent risk here: if we *were* to build on a 32-bit platform, then programs which
use arguments between @maxBound :: Int32@ and @maxBound :: Int64@ would behave differently!

So, what to do? We adopt the following strategy:
- We allow lifting/unlifting 'Int64' via 'Integer', including a safe downcast in 'readKnown'.
- We allow lifting/unlifting 'Int' via 'Int64', converting between them using 'intCastEq'.

This has the effect of allowing the use of 'Int64' always, and 'Int' iff it is provably equal to
'Int64'. So we can use 'Int' conveniently, but only if it has predictable behaviour.

(An alternative would be to just add 'Int', but add 'IntCastEq Int Int64' as an instance constraint.
That would also work, this way just seemed a little more explicit, and avoids adding constraints,
which can sometimes interfere with optimization and inling.)

Doing this effectively bans builds on 32-bit systems, but that's fine, since we don't care about
supporting 32-bit systems anyway, and this way any attempts to build on them will fail fast.

Note: we couldn't fail the bounds check with 'AsUnliftingError', because an out-of-bounds error is not an
internal one -- it's a normal evaluation failure, but unlifting errors have this connotation of
being "internal".
-}

instance KnownTypeAst DefaultUni Int64 where
    toTypeAst :: proxy Int64 -> Type TyName DefaultUni ()
toTypeAst proxy Int64
_ = Proxy Integer -> Type TyName DefaultUni ()
forall a (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst uni x =>
proxy x -> Type TyName uni ()
toTypeAst (Proxy Integer -> Type TyName DefaultUni ())
-> Proxy Integer -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ Proxy Integer
forall k (t :: k). Proxy t
Proxy @Integer

-- See Note [Int as Integer].
instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term Int64 where
    makeKnown :: Maybe cause -> Int64 -> MakeKnownM cause term
makeKnown Maybe cause
mayCause = Maybe cause -> Integer -> MakeKnownM cause term
forall (uni :: * -> *) val a cause.
MakeKnownIn uni val a =>
Maybe cause -> a -> MakeKnownM cause val
makeKnown Maybe cause
mayCause (Integer -> MakeKnownM cause term)
-> (Int64 -> Integer) -> Int64 -> MakeKnownM cause term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger
    {-# INLINE makeKnown #-}

instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term Int64 where
    readKnown :: Maybe cause -> term -> ReadKnownM cause Int64
readKnown Maybe cause
mayCause term
term =
        -- See Note [Performance of KnownTypeIn instances].
        -- Funnily, we don't need 'inline' here, unlike in the default implementation of 'readKnown'
        -- (go figure why).
        (Maybe cause -> term -> ReadKnownM cause Integer)
-> Maybe cause -> term -> ReadKnownM cause Integer
forall a. a -> a
inline Maybe cause -> term -> ReadKnownM cause Integer
forall val a cause.
KnownBuiltinType val a =>
Maybe cause -> val -> ReadKnownM cause a
readKnownConstant Maybe cause
mayCause term
term ReadKnownM cause Integer
-> (Integer -> ReadKnownM cause Int64) -> ReadKnownM cause Int64
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Integer -> ReadKnownM cause Int64)
-> Integer -> ReadKnownM cause Int64
oneShot \(Integer
i :: Integer) ->
            if Int64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int64
forall a. Bounded a => a
minBound :: Int64) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
i Bool -> Bool -> Bool
&& Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Int64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int64
forall a. Bounded a => a
maxBound :: Int64)
                then Int64 -> ReadKnownM cause Int64
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int64 -> ReadKnownM cause Int64)
-> Int64 -> ReadKnownM cause Int64
forall a b. (a -> b) -> a -> b
$ Integer -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i
                else AReview KnownTypeError ()
-> () -> Maybe cause -> ReadKnownM cause Int64
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview KnownTypeError ()
forall err. AsEvaluationFailure err => Prism' err ()
_EvaluationFailure () Maybe cause
mayCause
    {-# INLINE readKnown #-}

instance KnownTypeAst DefaultUni Int where
    toTypeAst :: proxy Int -> Type TyName DefaultUni ()
toTypeAst proxy Int
_ = Proxy Integer -> Type TyName DefaultUni ()
forall a (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst uni x =>
proxy x -> Type TyName uni ()
toTypeAst (Proxy Integer -> Type TyName DefaultUni ())
-> Proxy Integer -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ Proxy Integer
forall k (t :: k). Proxy t
Proxy @Integer

-- See Note [Int as Integer].
instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term Int where
    -- This could safely just be toInteger, but this way is more explicit and it'll
    -- turn into the same thing anyway.
    makeKnown :: Maybe cause -> Int -> MakeKnownM cause term
makeKnown Maybe cause
mayCause = Maybe cause -> Int64 -> MakeKnownM cause term
forall (uni :: * -> *) val a cause.
MakeKnownIn uni val a =>
Maybe cause -> a -> MakeKnownM cause val
makeKnown Maybe cause
mayCause (Int64 -> MakeKnownM cause term)
-> (Int -> Int64) -> Int -> MakeKnownM cause term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integral Int, Integral Int64, IsIntTypeEq Int Int64 ~ 'True) =>
Int -> Int64
forall a b.
(Integral a, Integral b, IsIntTypeEq a b ~ 'True) =>
a -> b
intCastEq @Int @Int64
    {-# INLINE makeKnown #-}

instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term Int where
    readKnown :: Maybe cause -> term -> ReadKnownM cause Int
readKnown Maybe cause
mayCause term
term = (Integral Int64, Integral Int, IsIntTypeEq Int64 Int ~ 'True) =>
Int64 -> Int
forall a b.
(Integral a, Integral b, IsIntTypeEq a b ~ 'True) =>
a -> b
intCastEq @Int64 @Int (Int64 -> Int)
-> Either (ErrorWithCause KnownTypeError cause) Int64
-> ReadKnownM cause Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe cause
-> term -> Either (ErrorWithCause KnownTypeError cause) Int64
forall (uni :: * -> *) val a cause.
ReadKnownIn uni val a =>
Maybe cause -> val -> ReadKnownM cause a
readKnown Maybe cause
mayCause term
term
    {-# INLINE readKnown #-}

{- Note [Stable encoding of tags]
'encodeUni' and 'decodeUni' are used for serialisation and deserialisation of types from the
universe and we need serialised things to be extremely stable, hence the definitions of 'encodeUni'
and 'decodeUni' must be amended only in a backwards compatible manner.

See Note [Stable encoding of PLC]
-}

instance Closed DefaultUni where
    type DefaultUni `Everywhere` constr =
        ( constr `Permits` Integer
        , constr `Permits` BS.ByteString
        , constr `Permits` Text.Text
        , constr `Permits` ()
        , constr `Permits` Bool
        , constr `Permits` []
        , constr `Permits` (,)
        , constr `Permits` Data
        )

    -- See Note [Stable encoding of tags].
    -- IF YOU'RE GETTING A WARNING HERE, DON'T FORGET TO AMEND 'withDecodedUni' RIGHT BELOW.
    encodeUni :: DefaultUni a -> [Int]
encodeUni DefaultUni a
DefaultUniInteger           = [Int
0]
    encodeUni DefaultUni a
DefaultUniByteString        = [Int
1]
    encodeUni DefaultUni a
DefaultUniString            = [Int
2]
    encodeUni DefaultUni a
DefaultUniUnit              = [Int
3]
    encodeUni DefaultUni a
DefaultUniBool              = [Int
4]
    encodeUni DefaultUni a
DefaultUniProtoList         = [Int
5]
    encodeUni DefaultUni a
DefaultUniProtoPair         = [Int
6]
    encodeUni (DefaultUniApply DefaultUni (Esc f)
uniF DefaultUni (Esc a)
uniA) = Int
7 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: DefaultUni (Esc f) -> [Int]
forall (uni :: * -> *) a. Closed uni => uni a -> [Int]
encodeUni DefaultUni (Esc f)
uniF [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ DefaultUni (Esc a) -> [Int]
forall (uni :: * -> *) a. Closed uni => uni a -> [Int]
encodeUni DefaultUni (Esc a)
uniA
    encodeUni DefaultUni a
DefaultUniData              = [Int
8]

    -- See Note [Decoding universes].
    -- See Note [Stable encoding of tags].
    withDecodedUni :: (forall k (a :: k).
 Typeable k =>
 DefaultUni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
withDecodedUni forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k = DecodeUniM Int
peelUniTag DecodeUniM Int -> (Int -> DecodeUniM r) -> DecodeUniM r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Int
0 -> DefaultUni (Esc Integer) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc Integer)
DefaultUniInteger
        Int
1 -> DefaultUni (Esc ByteString) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc ByteString)
DefaultUniByteString
        Int
2 -> DefaultUni (Esc Text) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc Text)
DefaultUniString
        Int
3 -> DefaultUni (Esc ()) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc ())
DefaultUniUnit
        Int
4 -> DefaultUni (Esc Bool) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc Bool)
DefaultUniBool
        Int
5 -> DefaultUni (Esc []) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc [])
DefaultUniProtoList
        Int
6 -> DefaultUni (Esc (,)) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc (,))
DefaultUniProtoPair
        Int
7 ->
            forall r.
Closed DefaultUni =>
(forall k (a :: k).
 Typeable k =>
 DefaultUni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
forall (uni :: * -> *) r.
Closed uni =>
(forall k (a :: k). Typeable k => uni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
withDecodedUni @DefaultUni ((forall k (a :: k).
  Typeable k =>
  DefaultUni (Esc a) -> DecodeUniM r)
 -> DecodeUniM r)
-> (forall k (a :: k).
    Typeable k =>
    DefaultUni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
forall a b. (a -> b) -> a -> b
$ \DefaultUni (Esc a)
uniF ->
                forall r.
Closed DefaultUni =>
(forall k (a :: k).
 Typeable k =>
 DefaultUni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
forall (uni :: * -> *) r.
Closed uni =>
(forall k (a :: k). Typeable k => uni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
withDecodedUni @DefaultUni ((forall k (a :: k).
  Typeable k =>
  DefaultUni (Esc a) -> DecodeUniM r)
 -> DecodeUniM r)
-> (forall k (a :: k).
    Typeable k =>
    DefaultUni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
forall a b. (a -> b) -> a -> b
$ \DefaultUni (Esc a)
uniA ->
                    DefaultUni (Esc a)
-> DefaultUni (Esc a)
-> (forall b. (Typeable b, k ~ (k -> b)) => DecodeUniM r)
-> DecodeUniM r
forall a ab (f :: ab) (x :: a) (uni :: * -> *) (m :: * -> *) r.
(Typeable ab, Typeable a, MonadPlus m) =>
uni (Esc f)
-> uni (Esc x)
-> (forall b. (Typeable b, ab ~ (a -> b)) => m r)
-> m r
withApplicable DefaultUni (Esc a)
uniF DefaultUni (Esc a)
uniA ((forall b. (Typeable b, k ~ (k -> b)) => DecodeUniM r)
 -> DecodeUniM r)
-> (forall b. (Typeable b, k ~ (k -> b)) => DecodeUniM r)
-> DecodeUniM r
forall a b. (a -> b) -> a -> b
$
                        DefaultUni (Esc (a a)) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k (DefaultUni (Esc (a a)) -> DecodeUniM r)
-> DefaultUni (Esc (a a)) -> DecodeUniM r
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc a)
DefaultUni (Esc a)
uniF DefaultUni (Esc a) -> DefaultUni (Esc a) -> DefaultUni (Esc (a a))
forall k k (f :: k -> k) (a :: k).
DefaultUni (Esc f) -> DefaultUni (Esc a) -> DefaultUni (Esc (f a))
`DefaultUniApply` DefaultUni (Esc a)
uniA
        Int
8 -> DefaultUni (Esc Data) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc Data)
DefaultUniData
        Int
_ -> DecodeUniM r
forall (f :: * -> *) a. Alternative f => f a
empty

    bring
        :: forall constr a r proxy. DefaultUni `Everywhere` constr
        => proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
    bring :: proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
bring proxy constr
_ DefaultUni (Esc a)
DefaultUniInteger    constr a => r
r = r
constr a => r
r
    bring proxy constr
_ DefaultUni (Esc a)
DefaultUniByteString constr a => r
r = r
constr a => r
r
    bring proxy constr
_ DefaultUni (Esc a)
DefaultUniString     constr a => r
r = r
constr a => r
r
    bring proxy constr
_ DefaultUni (Esc a)
DefaultUniUnit       constr a => r
r = r
constr a => r
r
    bring proxy constr
_ DefaultUni (Esc a)
DefaultUniBool       constr a => r
r = r
constr a => r
r
    bring proxy constr
p (DefaultUni (Esc f)
DefaultUniProtoList `DefaultUniApply` DefaultUni (Esc a)
uniA) constr a => r
r =
        proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
forall (uni :: * -> *) (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
bring proxy constr
p DefaultUni (Esc a)
DefaultUni (Esc a)
uniA constr a => r
constr a => r
r
    bring proxy constr
p (DefaultUni (Esc f)
DefaultUniProtoPair `DefaultUniApply` DefaultUni (Esc a)
uniA `DefaultUniApply` DefaultUni (Esc a)
uniB) constr a => r
r =
        proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
forall (uni :: * -> *) (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
bring proxy constr
p DefaultUni (Esc a)
DefaultUni (Esc a)
uniA ((constr a => r) -> r) -> (constr a => r) -> r
forall a b. (a -> b) -> a -> b
$ proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
forall (uni :: * -> *) (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
bring proxy constr
p DefaultUni (Esc a)
DefaultUni (Esc a)
uniB constr a => r
constr a => r
r
    bring proxy constr
_ (DefaultUni (Esc f)
f `DefaultUniApply` DefaultUni (Esc a)
_ `DefaultUniApply` DefaultUni (Esc a)
_ `DefaultUniApply` DefaultUni (Esc a)
_) constr a => r
_ =
        DefaultUni (Esc f) -> r
forall a b c d (f :: a -> b -> c -> d) any.
DefaultUni (Esc f) -> any
noMoreTypeFunctions DefaultUni (Esc f)
DefaultUni (Esc f)
f
    bring proxy constr
_ DefaultUni (Esc a)
DefaultUniData constr a => r
r = r
constr a => r
r