{-# OPTIONS -fno-warn-missing-pattern-synonym-signatures #-}
-- on 9.2.4 this is the flag that suppresses the above warning
{-# OPTIONS -Wno-missing-signatures #-}
-- 9.6 notices that all the constraints on 'TestTypesFromTheUniverseAreAllKnown'
-- are redundant (which they are), but we don't care because it only exists
-- to test that some constraints are solvable
{-# OPTIONS -Wno-redundant-constraints #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
#include "MachDeps.h"

-- effectfully: to the best of my experimentation, -O2 here improves
-- performance, but it's not clear why. This needs to be investigated.
{-# OPTIONS_GHC -O2 #-}

-- | The universe used by default and its instances.
module PlutusCore.Default.Universe
  ( DefaultUni (..)
  , pattern DefaultUniList
  , pattern DefaultUniArray
  , pattern DefaultUniPair
  , noMoreTypeFunctions
  , module Export -- Re-exporting universes infrastructure for convenience.
  ) where

import PlutusPrelude

import PlutusCore.Builtin
import PlutusCore.Core.Type (Type (..))
import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1
import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2
import PlutusCore.Crypto.BLS12_381.Pairing qualified as BLS12_381.Pairing
import PlutusCore.Data (Data)
import PlutusCore.Evaluation.Machine.ExMemoryUsage
  ( DataNodeCount (..)
  , IntegerCostedLiterally (..)
  , NumBytesCostedAsNumWords (..)
  , ValueMaxDepth (..)
  , ValueTotalSize (..)
  )
import PlutusCore.Pretty.Extra (juxtRenderContext)
import PlutusCore.Value (Value)

import Control.Monad.Except (throwError)
import Data.ByteString (ByteString)
import Data.Int
  ( Int16
  , Int32
  , Int64
  , Int8
  )
import Data.Proxy (Proxy (Proxy))
import Data.Text (Text)
import Data.Text qualified as Text
import Data.Typeable (typeRep)
import Data.Vector qualified as Vector
import Data.Vector.Strict qualified as Strict (Vector)
import Data.Word
  ( Word16
  , Word32
  , Word64
  )
import GHC.Exts (inline, oneShot)
import Text.PrettyBy.Fixity
  ( RenderContext
  , inContextM
  , juxtPrettyM
  )
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 necessary 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 ByteString)
  DefaultUniString :: DefaultUni (Esc Text)
  DefaultUniUnit :: DefaultUni (Esc ())
  DefaultUniBool :: DefaultUni (Esc Bool)
  DefaultUniProtoArray :: DefaultUni (Esc Strict.Vector)
  DefaultUniProtoList :: DefaultUni (Esc [])
  DefaultUniProtoPair :: DefaultUni (Esc (,))
  DefaultUniApply :: !(DefaultUni (Esc f)) -> !(DefaultUni (Esc a)) -> DefaultUni (Esc (f a))
  DefaultUniData :: DefaultUni (Esc Data)
  DefaultUniBLS12_381_G1_Element :: DefaultUni (Esc BLS12_381.G1.Element)
  DefaultUniBLS12_381_G2_Element :: DefaultUni (Esc BLS12_381.G2.Element)
  DefaultUniBLS12_381_MlResult :: DefaultUni (Esc BLS12_381.Pairing.MlResult)
  DefaultUniValue :: DefaultUni (Esc Value)

-- GHC infers crazy types for these two and the straightforward ones break pattern matching,
-- so we just leave GHC with its craziness.
pattern $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)
-> ((# #) -> r)
-> r
$bDefaultUniList :: forall {a} {k1} {k2} {f :: k1 -> k2} {a1 :: k1}.
(a ~ Esc (f a1), Esc f ~ Esc []) =>
DefaultUni (Esc a1) -> DefaultUni a
DefaultUniList uniA =
  DefaultUniProtoList `DefaultUniApply` uniA
pattern $mDefaultUniArray :: forall {r} {a}.
DefaultUni a
-> (forall {k1} {k2} {f :: k1 -> k2} {a1 :: k1}.
    (a ~ Esc (f a1), Esc f ~ Esc Vector) =>
    DefaultUni (Esc a1) -> r)
-> ((# #) -> r)
-> r
$bDefaultUniArray :: forall {a} {k1} {k2} {f :: k1 -> k2} {a1 :: k1}.
(a ~ Esc (f a1), Esc f ~ Esc Vector) =>
DefaultUni (Esc a1) -> DefaultUni a
DefaultUniArray uniA =
  DefaultUniProtoArray `DefaultUniApply` uniA
pattern $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)
-> ((# #) -> r)
-> r
$bDefaultUniPair :: forall {a} {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) -> DefaultUni a
DefaultUniPair uniA uniB =
  DefaultUniProtoPair `DefaultUniApply` uniA `DefaultUniApply` uniB

-- Removing 'LoopBreaker' didn't change anything at the time this comment was written, but we kept
-- it, because it hopefully provides some additional assurance that 'geqL' will not get elaborated
-- as a recursive definition.
instance AllBuiltinArgs DefaultUni (GEqL DefaultUni) a => GEqL DefaultUni a where
  geqL :: forall b.
DefaultUni (Esc a)
-> DefaultUni (Esc b) -> EvaluationResult (a :~: b)
geqL DefaultUni (Esc a)
DefaultUniInteger DefaultUni (Esc b)
a2 = do
    DefaultUni (Esc b)
DefaultUniInteger <- DefaultUni (Esc b) -> EvaluationResult (DefaultUni (Esc b))
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc b)
a2
    (a :~: b) -> EvaluationResult (a :~: b)
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geqL DefaultUni (Esc a)
DefaultUniByteString DefaultUni (Esc b)
a2 = do
    DefaultUni (Esc b)
DefaultUniByteString <- DefaultUni (Esc b) -> EvaluationResult (DefaultUni (Esc b))
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc b)
a2
    (a :~: b) -> EvaluationResult (a :~: b)
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geqL DefaultUni (Esc a)
DefaultUniString DefaultUni (Esc b)
a2 = do
    DefaultUni (Esc b)
DefaultUniString <- DefaultUni (Esc b) -> EvaluationResult (DefaultUni (Esc b))
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc b)
a2
    (a :~: b) -> EvaluationResult (a :~: b)
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geqL DefaultUni (Esc a)
DefaultUniUnit DefaultUni (Esc b)
a2 = do
    DefaultUni (Esc b)
DefaultUniUnit <- DefaultUni (Esc b) -> EvaluationResult (DefaultUni (Esc b))
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc b)
a2
    (a :~: b) -> EvaluationResult (a :~: b)
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geqL DefaultUni (Esc a)
DefaultUniBool DefaultUni (Esc b)
a2 = do
    DefaultUni (Esc b)
DefaultUniBool <- DefaultUni (Esc b) -> EvaluationResult (DefaultUni (Esc b))
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc b)
a2
    (a :~: b) -> EvaluationResult (a :~: b)
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geqL (DefaultUni (Esc f)
DefaultUniProtoList `DefaultUniApply` DefaultUni (Esc a)
a1) DefaultUni (Esc b)
listA2 = do
    DefaultUni (Esc f)
DefaultUniProtoList `DefaultUniApply` DefaultUni (Esc a)
a2 <- DefaultUni (Esc b) -> EvaluationResult (DefaultUni (Esc b))
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc b)
listA2
    a :~: a
Refl <- LoopBreaker DefaultUni (Esc a)
-> LoopBreaker DefaultUni (Esc a) -> EvaluationResult (a :~: a)
forall b.
LoopBreaker DefaultUni (Esc a)
-> LoopBreaker DefaultUni (Esc b) -> EvaluationResult (a :~: b)
forall (f :: * -> *) a b.
GEqL f a =>
f (Esc a) -> f (Esc b) -> EvaluationResult (a :~: b)
geqL (DefaultUni (Esc a) -> LoopBreaker DefaultUni (Esc a)
forall (uni :: * -> *) a. uni a -> LoopBreaker uni a
LoopBreaker DefaultUni (Esc a)
DefaultUni (Esc a)
a1) (DefaultUni (Esc a) -> LoopBreaker DefaultUni (Esc a)
forall (uni :: * -> *) a. uni a -> LoopBreaker uni a
LoopBreaker DefaultUni (Esc a)
DefaultUni (Esc a)
a2)
    (a :~: b) -> EvaluationResult (a :~: b)
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geqL (DefaultUni (Esc f)
DefaultUniProtoArray `DefaultUniApply` DefaultUni (Esc a)
a1) DefaultUni (Esc b)
arrayA2 = do
    DefaultUni (Esc f)
DefaultUniProtoArray `DefaultUniApply` DefaultUni (Esc a)
a2 <- DefaultUni (Esc b) -> EvaluationResult (DefaultUni (Esc b))
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc b)
arrayA2
    a :~: a
Refl <- LoopBreaker DefaultUni (Esc a)
-> LoopBreaker DefaultUni (Esc a) -> EvaluationResult (a :~: a)
forall b.
LoopBreaker DefaultUni (Esc a)
-> LoopBreaker DefaultUni (Esc b) -> EvaluationResult (a :~: b)
forall (f :: * -> *) a b.
GEqL f a =>
f (Esc a) -> f (Esc b) -> EvaluationResult (a :~: b)
geqL (DefaultUni (Esc a) -> LoopBreaker DefaultUni (Esc a)
forall (uni :: * -> *) a. uni a -> LoopBreaker uni a
LoopBreaker DefaultUni (Esc a)
DefaultUni (Esc a)
a1) (DefaultUni (Esc a) -> LoopBreaker DefaultUni (Esc a)
forall (uni :: * -> *) a. uni a -> LoopBreaker uni a
LoopBreaker DefaultUni (Esc a)
DefaultUni (Esc a)
a2)
    (a :~: b) -> EvaluationResult (a :~: b)
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geqL (DefaultUni (Esc f)
DefaultUniProtoPair `DefaultUniApply` DefaultUni (Esc a)
a1 `DefaultUniApply` DefaultUni (Esc a)
b1) DefaultUni (Esc b)
pairA2 = do
    DefaultUni (Esc f)
DefaultUniProtoPair `DefaultUniApply` DefaultUni (Esc a)
a2 `DefaultUniApply` DefaultUni (Esc a)
b2 <- DefaultUni (Esc b) -> EvaluationResult (DefaultUni (Esc b))
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc b)
pairA2
    a :~: a
Refl <- LoopBreaker DefaultUni (Esc a)
-> LoopBreaker DefaultUni (Esc a) -> EvaluationResult (a :~: a)
forall b.
LoopBreaker DefaultUni (Esc a)
-> LoopBreaker DefaultUni (Esc b) -> EvaluationResult (a :~: b)
forall (f :: * -> *) a b.
GEqL f a =>
f (Esc a) -> f (Esc b) -> EvaluationResult (a :~: b)
geqL (DefaultUni (Esc a) -> LoopBreaker DefaultUni (Esc a)
forall (uni :: * -> *) a. uni a -> LoopBreaker uni a
LoopBreaker DefaultUni (Esc a)
DefaultUni (Esc a)
a1) (DefaultUni (Esc a) -> LoopBreaker DefaultUni (Esc a)
forall (uni :: * -> *) a. uni a -> LoopBreaker uni a
LoopBreaker DefaultUni (Esc a)
DefaultUni (Esc a)
a2)
    a :~: a
Refl <- LoopBreaker DefaultUni (Esc a)
-> LoopBreaker DefaultUni (Esc a) -> EvaluationResult (a :~: a)
forall b.
LoopBreaker DefaultUni (Esc a)
-> LoopBreaker DefaultUni (Esc b) -> EvaluationResult (a :~: b)
forall (f :: * -> *) a b.
GEqL f a =>
f (Esc a) -> f (Esc b) -> EvaluationResult (a :~: b)
geqL (DefaultUni (Esc a) -> LoopBreaker DefaultUni (Esc a)
forall (uni :: * -> *) a. uni a -> LoopBreaker uni a
LoopBreaker DefaultUni (Esc a)
DefaultUni (Esc a)
b1) (DefaultUni (Esc a) -> LoopBreaker DefaultUni (Esc a)
forall (uni :: * -> *) a. uni a -> LoopBreaker uni a
LoopBreaker DefaultUni (Esc a)
DefaultUni (Esc a)
b2)
    (a :~: b) -> EvaluationResult (a :~: b)
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geqL (DefaultUni (Esc f)
f `DefaultUniApply` DefaultUni (Esc a)
_ `DefaultUniApply` DefaultUni (Esc a)
_ `DefaultUniApply` DefaultUni (Esc a)
_) DefaultUni (Esc b)
_ =
    DefaultUni (Esc f) -> EvaluationResult (a :~: b)
forall a b c d (f :: a -> b -> c -> d) any.
DefaultUni (Esc f) -> any
noMoreTypeFunctions DefaultUni (Esc f)
DefaultUni (Esc f)
f
  geqL DefaultUni (Esc a)
DefaultUniData DefaultUni (Esc b)
a2 = do
    DefaultUni (Esc b)
DefaultUniData <- DefaultUni (Esc b) -> EvaluationResult (DefaultUni (Esc b))
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc b)
a2
    (a :~: b) -> EvaluationResult (a :~: b)
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geqL DefaultUni (Esc a)
DefaultUniBLS12_381_G1_Element DefaultUni (Esc b)
a2 = do
    DefaultUni (Esc b)
DefaultUniBLS12_381_G1_Element <- DefaultUni (Esc b) -> EvaluationResult (DefaultUni (Esc b))
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc b)
a2
    (a :~: b) -> EvaluationResult (a :~: b)
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geqL DefaultUni (Esc a)
DefaultUniBLS12_381_G2_Element DefaultUni (Esc b)
a2 = do
    DefaultUni (Esc b)
DefaultUniBLS12_381_G2_Element <- DefaultUni (Esc b) -> EvaluationResult (DefaultUni (Esc b))
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc b)
a2
    (a :~: b) -> EvaluationResult (a :~: b)
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geqL DefaultUni (Esc a)
DefaultUniBLS12_381_MlResult DefaultUni (Esc b)
a2 = do
    DefaultUni (Esc b)
DefaultUniBLS12_381_MlResult <- DefaultUni (Esc b) -> EvaluationResult (DefaultUni (Esc b))
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc b)
a2
    (a :~: b) -> EvaluationResult (a :~: b)
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geqL DefaultUni (Esc a)
DefaultUniValue DefaultUni (Esc b)
a2 = do
    DefaultUni (Esc b)
DefaultUniValue <- DefaultUni (Esc b) -> EvaluationResult (DefaultUni (Esc b))
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc b)
a2
    (a :~: b) -> EvaluationResult (a :~: b)
forall a. a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  {-# INLINE geqL #-}

instance GEq DefaultUni where
  -- We define 'geq' manually instead of using 'deriveGEq', because the latter creates a single
  -- recursive definition and we want two instead. The reason why we want two is because this
  -- allows GHC to inline the initial step that appears non-recursive to GHC, because recursion
  -- is hidden in the other function that is marked as @OPAQUE@ and is chosen by GHC as a
  -- loop-breaker, see https://wiki.haskell.org/Inlining_and_Specialisation#What_is_a_loop-breaker
  -- (we're not really sure if this is a reliable solution, but if it stops working, we won't miss
  -- very much and we've failed to settle on any other approach).
  --
  -- On the critical path this definition should only be used for builtins that perform equality
  -- checking of statically unknown runtime type tags ('MkCons' is one such builtin for
  -- example). All other builtins should use 'geqL' (the latter is internal to 'readKnownConstant'
  -- and is therefore hidden from the person adding a new builtin).
  --
  -- We use @NOINLINE@ instead of @OPAQUE@, because we don't actually care about the recursive
  -- definition not being inlined, we just want it to be chosen as the loop breaker.
  geq :: forall a b. DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
geq = DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
forall a b. DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
goStep
    where
      goStep, goRec :: DefaultUni a1 -> DefaultUni a2 -> Maybe (a1 :~: a2)
      goStep :: forall a b. DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
goStep DefaultUni a1
DefaultUniInteger DefaultUni a2
a2 = do
        DefaultUni a2
DefaultUniInteger <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni a2
a2
        (a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
      goStep DefaultUni a1
DefaultUniByteString DefaultUni a2
a2 = do
        DefaultUni a2
DefaultUniByteString <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni a2
a2
        (a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
      goStep DefaultUni a1
DefaultUniString DefaultUni a2
a2 = do
        DefaultUni a2
DefaultUniString <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni a2
a2
        (a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
      goStep DefaultUni a1
DefaultUniUnit DefaultUni a2
a2 = do
        DefaultUni a2
DefaultUniUnit <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni a2
a2
        (a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
      goStep DefaultUni a1
DefaultUniBool DefaultUni a2
a2 = do
        DefaultUni a2
DefaultUniBool <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni a2
a2
        (a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
      goStep DefaultUni a1
DefaultUniProtoList DefaultUni a2
a2 = do
        DefaultUni a2
DefaultUniProtoList <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni a2
a2
        (a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
      goStep DefaultUni a1
DefaultUniProtoArray DefaultUni a2
a2 = do
        DefaultUni a2
DefaultUniProtoArray <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni a2
a2
        (a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
      goStep DefaultUni a1
DefaultUniProtoPair DefaultUni a2
a2 = do
        DefaultUni a2
DefaultUniProtoPair <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni a2
a2
        (a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
      goStep (DefaultUniApply DefaultUni (Esc f)
f1 DefaultUni (Esc a)
x1) DefaultUni a2
a2 = do
        DefaultUniApply DefaultUni (Esc f)
f2 DefaultUni (Esc a)
x2 <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni a2
a2
        Esc f :~: Esc f
Refl <- DefaultUni (Esc f) -> DefaultUni (Esc f) -> Maybe (Esc f :~: Esc f)
forall a b. DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
goRec DefaultUni (Esc f)
f1 DefaultUni (Esc f)
f2
        Esc a :~: Esc a
Refl <- DefaultUni (Esc a) -> DefaultUni (Esc a) -> Maybe (Esc a :~: Esc a)
forall a b. DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
goRec DefaultUni (Esc a)
x1 DefaultUni (Esc a)
x2
        (a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
      goStep DefaultUni a1
DefaultUniData DefaultUni a2
a2 = do
        DefaultUni a2
DefaultUniData <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni a2
a2
        (a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
      goStep DefaultUni a1
DefaultUniBLS12_381_G1_Element DefaultUni a2
a2 = do
        DefaultUni a2
DefaultUniBLS12_381_G1_Element <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni a2
a2
        (a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
      goStep DefaultUni a1
DefaultUniBLS12_381_G2_Element DefaultUni a2
a2 = do
        DefaultUni a2
DefaultUniBLS12_381_G2_Element <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni a2
a2
        (a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
      goStep DefaultUni a1
DefaultUniBLS12_381_MlResult DefaultUni a2
a2 = do
        DefaultUni a2
DefaultUniBLS12_381_MlResult <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni a2
a2
        (a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
      goStep DefaultUni a1
DefaultUniValue DefaultUni a2
a2 = do
        DefaultUni a2
DefaultUniValue <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni a2
a2
        (a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
      {-# INLINE goStep #-}

      goRec :: forall a b. DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
goRec = DefaultUni a1 -> DefaultUni a2 -> Maybe (a1 :~: a2)
forall a b. DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
goStep
      {-# NOINLINE goRec #-}

-- | For pleasing the coverage checker.
noMoreTypeFunctions :: DefaultUni (Esc (f :: a -> b -> c -> d)) -> any
noMoreTypeFunctions :: forall a b c d (f :: a -> b -> c -> d) any.
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 :: forall k (a :: k). 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)
DefaultUniProtoArray = 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 k (a :: k). DefaultUni (Esc a) -> SingKind k
forall (uni :: * -> *) k (a :: k).
ToKind uni =>
uni (Esc a) -> SingKind k
toSingKind DefaultUni (Esc f)
uniF of SingKind k1
_ `SingKindArrow` SingKind l
cod -> SingKind k
SingKind l
cod
  toSingKind DefaultUni (Esc a)
DefaultUniData = SingKind k
forall k. KnownKind k => SingKind k
knownKind
  toSingKind DefaultUni (Esc a)
DefaultUniBLS12_381_G1_Element = SingKind k
forall k. KnownKind k => SingKind k
knownKind
  toSingKind DefaultUni (Esc a)
DefaultUniBLS12_381_G2_Element = SingKind k
forall k. KnownKind k => SingKind k
knownKind
  toSingKind DefaultUni (Esc a)
DefaultUniBLS12_381_MlResult = SingKind k
forall k. KnownKind k => SingKind k
knownKind
  toSingKind DefaultUni (Esc a)
DefaultUniValue = SingKind k
forall k. KnownKind k => SingKind k
knownKind

instance HasUniApply DefaultUni where
  uniApply :: forall {k} {k} (f :: k -> k) (a :: k).
DefaultUni (Esc f) -> DefaultUni (Esc a) -> DefaultUni (Esc (f a))
uniApply = 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

  matchUniApply :: forall tb r.
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

deriving stock instance Show (DefaultUni a)
instance GShow DefaultUni where gshowsPrec :: forall a. Int -> DefaultUni a -> ShowS
gshowsPrec = Int -> DefaultUni a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

instance PrettyBy RenderContext (DefaultUni a) where
  prettyBy :: forall ann. RenderContext -> DefaultUni a -> Doc ann
prettyBy = (DefaultUni a -> InContextM RenderContext (Doc ann))
-> RenderContext -> DefaultUni a -> Doc ann
forall a config ann.
(a -> InContextM config (Doc ann)) -> config -> a -> Doc ann
inContextM ((DefaultUni a -> InContextM RenderContext (Doc ann))
 -> RenderContext -> DefaultUni a -> Doc ann)
-> (DefaultUni a -> InContextM RenderContext (Doc ann))
-> RenderContext
-> DefaultUni a
-> Doc ann
forall a b. (a -> b) -> a -> b
$ \case
    DefaultUni a
DefaultUniInteger -> InContextM RenderContext (Doc ann)
"integer"
    DefaultUni a
DefaultUniByteString -> InContextM RenderContext (Doc ann)
"bytestring"
    DefaultUni a
DefaultUniString -> InContextM RenderContext (Doc ann)
"string"
    DefaultUni a
DefaultUniUnit -> InContextM RenderContext (Doc ann)
"unit"
    DefaultUni a
DefaultUniBool -> InContextM RenderContext (Doc ann)
"bool"
    DefaultUni a
DefaultUniProtoList -> InContextM RenderContext (Doc ann)
"list"
    DefaultUni a
DefaultUniProtoArray -> InContextM RenderContext (Doc ann)
"array"
    DefaultUni a
DefaultUniProtoPair -> InContextM RenderContext (Doc ann)
"pair"
    DefaultUniApply DefaultUni (Esc f)
uniF DefaultUni (Esc a)
uniA -> DefaultUni (Esc f)
uniF DefaultUni (Esc f)
-> DefaultUni (Esc a) -> InContextM RenderContext (Doc ann)
forall config env (m :: * -> *) a b ann.
(MonadPrettyContext config env m, PrettyBy config a,
 PrettyBy config b) =>
a -> b -> m (Doc ann)
`juxtPrettyM` DefaultUni (Esc a)
uniA
    DefaultUni a
DefaultUniData -> InContextM RenderContext (Doc ann)
"data"
    DefaultUni a
DefaultUniBLS12_381_G1_Element -> InContextM RenderContext (Doc ann)
"bls12_381_G1_element"
    DefaultUni a
DefaultUniBLS12_381_G2_Element -> InContextM RenderContext (Doc ann)
"bls12_381_G2_element"
    DefaultUni a
DefaultUniBLS12_381_MlResult -> InContextM RenderContext (Doc ann)
"bls12_381_mlresult"
    DefaultUni a
DefaultUniValue -> InContextM RenderContext (Doc ann)
"value"

instance PrettyBy RenderContext (SomeTypeIn DefaultUni) where
  prettyBy :: forall ann. RenderContext -> SomeTypeIn DefaultUni -> Doc ann
prettyBy RenderContext
config (SomeTypeIn DefaultUni (Esc a)
uni) = RenderContext -> DefaultUni (Esc a) -> Doc ann
forall ann. RenderContext -> DefaultUni (Esc a) -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy RenderContext
config DefaultUni (Esc a)
uni

{-| This always pretty-prints parens around type applications (e.g. @(list bool)@) and
doesn't pretty-print them otherwise (e.g. @integer@). -}
instance Pretty (DefaultUni a) where
  pretty :: forall ann. DefaultUni a -> Doc ann
pretty = RenderContext -> DefaultUni a -> Doc ann
forall ann. RenderContext -> DefaultUni a -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy RenderContext
juxtRenderContext

instance Pretty (SomeTypeIn DefaultUni) where
  pretty :: forall ann. SomeTypeIn DefaultUni -> Doc ann
pretty (SomeTypeIn DefaultUni (Esc a)
uni) = DefaultUni (Esc a) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. DefaultUni (Esc a) -> Doc ann
pretty DefaultUni (Esc a)
uni

-- | Elaborate a built-in type (see 'ElaborateBuiltin') from 'DefaultUni'.
type ElaborateBuiltinDefaultUni :: forall a. a -> a
type family ElaborateBuiltinDefaultUni x where
  ElaborateBuiltinDefaultUni (f x) = ElaborateBuiltinDefaultUni f `TyAppRep` x
  ElaborateBuiltinDefaultUni x = BuiltinHead x

type instance ElaborateBuiltin DefaultUni x = ElaborateBuiltinDefaultUni x

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 DefaultUni `Contains` Integer where
  knownUni :: DefaultUni (Esc Integer)
knownUni = DefaultUni (Esc Integer)
DefaultUniInteger
instance DefaultUni `Contains` ByteString where
  knownUni :: DefaultUni (Esc ByteString)
knownUni = DefaultUni (Esc ByteString)
DefaultUniByteString
instance DefaultUni `Contains` 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` Value where
  knownUni :: DefaultUni (Esc Value)
knownUni = DefaultUni (Esc Value)
DefaultUniValue
instance DefaultUni `Contains` [] where
  knownUni :: DefaultUni (Esc [])
knownUni = DefaultUni (Esc [])
DefaultUniProtoList
instance DefaultUni `Contains` Strict.Vector where
  knownUni :: DefaultUni (Esc Vector)
knownUni = DefaultUni (Esc Vector)
DefaultUniProtoArray
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` BLS12_381.G1.Element where
  knownUni :: DefaultUni (Esc Element)
knownUni = DefaultUni (Esc Element)
DefaultUniBLS12_381_G1_Element
instance DefaultUni `Contains` BLS12_381.G2.Element where
  knownUni :: DefaultUni (Esc Element)
knownUni = DefaultUni (Esc Element)
DefaultUniBLS12_381_G2_Element
instance DefaultUni `Contains` BLS12_381.Pairing.MlResult where
  knownUni :: DefaultUni (Esc MlResult)
knownUni = DefaultUni (Esc MlResult)
DefaultUniBLS12_381_MlResult

instance
  KnownBuiltinTypeAst tyname DefaultUni Integer
  => KnownTypeAst tyname DefaultUni Integer
instance
  KnownBuiltinTypeAst tyname DefaultUni ByteString
  => KnownTypeAst tyname DefaultUni ByteString
instance
  KnownBuiltinTypeAst tyname DefaultUni Text
  => KnownTypeAst tyname DefaultUni Text
instance
  KnownBuiltinTypeAst tyname DefaultUni ()
  => KnownTypeAst tyname DefaultUni ()
instance
  KnownBuiltinTypeAst tyname DefaultUni Bool
  => KnownTypeAst tyname DefaultUni Bool
instance
  KnownBuiltinTypeAst tyname DefaultUni [a]
  => KnownTypeAst tyname DefaultUni [a]
instance
  KnownBuiltinTypeAst tyname DefaultUni (Strict.Vector a)
  => KnownTypeAst tyname DefaultUni (Strict.Vector a)
instance
  KnownBuiltinTypeAst tyname DefaultUni (a, b)
  => KnownTypeAst tyname DefaultUni (a, b)
instance
  KnownBuiltinTypeAst tyname DefaultUni Data
  => KnownTypeAst tyname DefaultUni Data
instance
  KnownBuiltinTypeAst tyname DefaultUni BLS12_381.G1.Element
  => KnownTypeAst tyname DefaultUni BLS12_381.G1.Element
instance
  KnownBuiltinTypeAst tyname DefaultUni BLS12_381.G2.Element
  => KnownTypeAst tyname DefaultUni BLS12_381.G2.Element
instance
  KnownBuiltinTypeAst tyname DefaultUni BLS12_381.Pairing.MlResult
  => KnownTypeAst tyname DefaultUni BLS12_381.Pairing.MlResult
instance
  KnownBuiltinTypeAst tyname DefaultUni Value
  => KnownTypeAst tyname DefaultUni Value

instance
  KnownBuiltinTypeIn DefaultUni term Integer
  => ReadKnownIn DefaultUni term Integer
instance
  KnownBuiltinTypeIn DefaultUni term ByteString
  => ReadKnownIn DefaultUni term ByteString
instance
  KnownBuiltinTypeIn DefaultUni term Text
  => ReadKnownIn DefaultUni term Text
instance
  KnownBuiltinTypeIn DefaultUni term ()
  => ReadKnownIn DefaultUni term ()
instance
  KnownBuiltinTypeIn DefaultUni term Bool
  => ReadKnownIn DefaultUni term Bool
instance
  KnownBuiltinTypeIn DefaultUni term Data
  => ReadKnownIn DefaultUni term Data
instance
  KnownBuiltinTypeIn DefaultUni term [a]
  => ReadKnownIn DefaultUni term [a]
instance
  KnownBuiltinTypeIn DefaultUni term (Strict.Vector a)
  => ReadKnownIn DefaultUni term (Strict.Vector a)
instance
  KnownBuiltinTypeIn DefaultUni term (a, b)
  => ReadKnownIn DefaultUni term (a, b)
instance
  KnownBuiltinTypeIn DefaultUni term BLS12_381.G1.Element
  => ReadKnownIn DefaultUni term BLS12_381.G1.Element
instance
  KnownBuiltinTypeIn DefaultUni term BLS12_381.G2.Element
  => ReadKnownIn DefaultUni term BLS12_381.G2.Element
instance
  KnownBuiltinTypeIn DefaultUni term BLS12_381.Pairing.MlResult
  => ReadKnownIn DefaultUni term BLS12_381.Pairing.MlResult
instance
  KnownBuiltinTypeIn DefaultUni term Value
  => ReadKnownIn DefaultUni term Value

instance
  KnownBuiltinTypeIn DefaultUni term Integer
  => MakeKnownIn DefaultUni term Integer
instance
  KnownBuiltinTypeIn DefaultUni term ByteString
  => MakeKnownIn DefaultUni term ByteString
instance
  KnownBuiltinTypeIn DefaultUni term Text
  => MakeKnownIn DefaultUni term Text
instance
  KnownBuiltinTypeIn DefaultUni term ()
  => MakeKnownIn DefaultUni term ()
instance
  KnownBuiltinTypeIn DefaultUni term Bool
  => MakeKnownIn DefaultUni term Bool
instance
  KnownBuiltinTypeIn DefaultUni term Data
  => MakeKnownIn DefaultUni term Data
instance
  KnownBuiltinTypeIn DefaultUni term [a]
  => MakeKnownIn DefaultUni term [a]
instance
  KnownBuiltinTypeIn DefaultUni term (Strict.Vector a)
  => MakeKnownIn DefaultUni term (Strict.Vector a)
instance
  KnownBuiltinTypeIn DefaultUni term (a, b)
  => MakeKnownIn DefaultUni term (a, b)
instance
  KnownBuiltinTypeIn DefaultUni term BLS12_381.G1.Element
  => MakeKnownIn DefaultUni term BLS12_381.G1.Element
instance
  KnownBuiltinTypeIn DefaultUni term BLS12_381.G2.Element
  => MakeKnownIn DefaultUni term BLS12_381.G2.Element
instance
  KnownBuiltinTypeIn DefaultUni term BLS12_381.Pairing.MlResult
  => MakeKnownIn DefaultUni term BLS12_381.Pairing.MlResult
instance
  KnownBuiltinTypeIn DefaultUni term Value
  => MakeKnownIn DefaultUni term Value

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

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

This is inconvenient and also error-prone: dealing with a function that takes an 'Int' or 'Word8'
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' or 'fromIntegral'.

Moreover, there is a latent risk here: if we *were* to build on a 32-bit architecture, 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 bounded integral types such as 'Word8' or 'Int64' via 'Integer',
  including a safe upcast in 'makeKnown' (which we could have on any architecture, but we only add
  it for 64-bit for uniformity) and a safe checked downcast in 'readKnown'.
- We allow lifting/unlifting 'Int' via 'Int64' and 'Word' via 'Word64', constraining the conversion
  between them to 64-bit architectures where this conversion is safe.

Doing this effectively bans builds on all non-64-bit systems, which is acceptable since 64-bit
systems are required for node deployment, and this way any attempts to build on them will fail fast.

We used to use newtype- and via-deriving for implementations of relevant instances, but at some
point GHC stopped attaching @INLINE@ annotations to those causing the GHC Core for builtins to have
multiple 'readKnown' and 'makeKnown' calls, so now we don't rely on deriving and implement instances
manually.
-}

-- | 'coerce' the argument, then call 'makeKnown'.
makeKnownCoerce
  :: forall b term a
   . (MakeKnownIn DefaultUni term b, Coercible a b)
  => a -> BuiltinResult term
makeKnownCoerce :: forall b term a.
(MakeKnownIn DefaultUni term b, Coercible a b) =>
a -> BuiltinResult term
makeKnownCoerce = (b -> BuiltinResult term) -> a -> BuiltinResult term
forall a b s. Coercible a b => (a -> s) -> b -> s
coerceArg ((b -> BuiltinResult term) -> a -> BuiltinResult term)
-> (b -> BuiltinResult term) -> a -> BuiltinResult term
forall a b. (a -> b) -> a -> b
$ forall (uni :: * -> *) val a.
MakeKnownIn uni val a =>
a -> BuiltinResult val
makeKnown @_ @_ @b
{-# INLINE makeKnownCoerce #-}

-- | Call 'readKnown', then 'coerce' the argument.
readKnownCoerce
  :: forall b term a
   . (ReadKnownIn DefaultUni term b, Coercible b a)
  => term -> ReadKnownM a
readKnownCoerce :: forall b term a.
(ReadKnownIn DefaultUni term b, Coercible b a) =>
term -> ReadKnownM a
readKnownCoerce = (b -> a) -> Either BuiltinError b -> ReadKnownM a
forall a b.
(a -> b) -> Either BuiltinError a -> Either BuiltinError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> a
forall a b. Coercible a b => a -> b
coerce (Either BuiltinError b -> ReadKnownM a)
-> (term -> Either BuiltinError b) -> term -> ReadKnownM a
forall b c a. Coercible b c => (b -> c) -> (a -> b) -> a -> c
#. forall (uni :: * -> *) val a.
ReadKnownIn uni val a =>
val -> ReadKnownM a
readKnown @_ @_ @b
{-# INLINE readKnownCoerce #-}

{-| For deriving 'KnownTypeAst' instances via 'Integer' (no constructor, because we don't need any
for 'KnownTypeAst'). -}
data AsInteger a

instance KnownTypeAst tyname DefaultUni (AsInteger a) where
  type IsBuiltin _ _ = 'False
  type ToHoles _ _ _ = '[]
  type ToBinds _ acc _ = acc
  typeAst :: Type tyname DefaultUni ()
typeAst = Proxy Integer -> Type tyname DefaultUni ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname 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
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Integer

makeKnownAsInteger
  :: forall term a
   . (KnownBuiltinTypeIn DefaultUni term Integer, Integral a)
  => a -> BuiltinResult term
makeKnownAsInteger :: forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a) =>
a -> BuiltinResult term
makeKnownAsInteger = Integer -> BuiltinResult term
forall (uni :: * -> *) val a.
MakeKnownIn uni val a =>
a -> BuiltinResult val
makeKnown (Integer -> BuiltinResult term)
-> (a -> Integer) -> a -> BuiltinResult term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Integer
forall a. Integral a => a -> Integer
toInteger
{-# INLINE makeKnownAsInteger #-}

readKnownAsInteger
  :: forall term a
   . (KnownBuiltinTypeIn DefaultUni term Integer, Integral a, Bounded a, Typeable a)
  => term -> ReadKnownM a
readKnownAsInteger :: forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a, Bounded a,
 Typeable a) =>
term -> ReadKnownM a
readKnownAsInteger term
term =
  -- See Note [Performance of ReadKnownIn and MakeKnownIn instances].
  -- Funnily, we don't need 'inline' here, unlike in the default implementation of 'readKnown'
  -- (go figure why).
  (term -> ReadKnownM Integer) -> term -> ReadKnownM Integer
forall a. a -> a
inline term -> ReadKnownM Integer
forall val a. KnownBuiltinType val a => val -> ReadKnownM a
readKnownConstant term
term ReadKnownM Integer
-> (Integer -> 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
>>= (Integer -> Either BuiltinError a)
-> Integer -> Either BuiltinError a
forall a b. (a -> b) -> a -> b
oneShot \(Integer
i :: Integer) ->
    -- We don't make use here of 'toIntegralSized' because of performance considerations,
    -- see: https://gitlab.haskell.org/ghc/ghc/-/issues/19641
    -- TODO: benchmark an alternative 'integerToIntMaybe', modified from @ghc-bignum@
    if a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a
forall a. Bounded a => a
minBound :: a) 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
<= a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a
forall a. Bounded a => a
maxBound :: a)
      then a -> Either BuiltinError a
forall a. a -> Either BuiltinError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Either BuiltinError a) -> a -> Either BuiltinError a
forall a b. (a -> b) -> a -> b
$ Integer -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i
      else
        BuiltinError -> Either BuiltinError a
forall a. BuiltinError -> Either BuiltinError a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (BuiltinError -> Either BuiltinError a)
-> (Text -> BuiltinError) -> Text -> Either BuiltinError a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> BuiltinError
operationalUnliftingError (Text -> Either BuiltinError a) -> Text -> Either BuiltinError a
forall a b. (a -> b) -> a -> b
$
          [Text] -> Text
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
            [ String -> Text
Text.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Integer -> String
forall a. Show a => a -> String
show Integer
i
            , Text
" is not within the bounds of "
            , String -> Text
Text.pack (String -> Text) -> (Proxy a -> String) -> Proxy a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeRep -> String
forall a. Show a => a -> String
show (TypeRep -> String) -> (Proxy a -> TypeRep) -> Proxy a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy a -> Text) -> Proxy a -> Text
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a
            ]
{-# INLINE readKnownAsInteger #-}

#if WORD_SIZE_IN_BITS == 64
-- See Note [Integral types as Integer].
deriving via AsInteger Int instance
        KnownTypeAst tyname DefaultUni Int
instance KnownBuiltinTypeIn DefaultUni term Integer => MakeKnownIn DefaultUni term Int where
    makeKnown :: Int -> BuiltinResult term
makeKnown = Int -> BuiltinResult term
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a) =>
a -> BuiltinResult term
makeKnownAsInteger
    {-# INLINE makeKnown #-}
instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni term Int where
    readKnown :: term -> ReadKnownM Int
readKnown term
term = forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int64 @Int (Int64 -> Int) -> Either BuiltinError Int64 -> ReadKnownM Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> term -> Either BuiltinError Int64
forall (uni :: * -> *) val a.
ReadKnownIn uni val a =>
val -> ReadKnownM a
readKnown term
term
    {-# INLINE readKnown #-}

deriving via AsInteger Word instance
        KnownTypeAst tyname DefaultUni Word
instance KnownBuiltinTypeIn DefaultUni term Integer => MakeKnownIn DefaultUni term Word where
    makeKnown :: Word -> BuiltinResult term
makeKnown = Word -> BuiltinResult term
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a) =>
a -> BuiltinResult term
makeKnownAsInteger
    {-# INLINE makeKnown #-}
instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni term Word where
    readKnown :: term -> ReadKnownM Word
readKnown term
term = forall a b. (Integral a, Num b) => a -> b
fromIntegral @Word64 @Word (Word64 -> Word) -> Either BuiltinError Word64 -> ReadKnownM Word
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> term -> Either BuiltinError Word64
forall (uni :: * -> *) val a.
ReadKnownIn uni val a =>
val -> ReadKnownM a
readKnown term
term
    {-# INLINE readKnown #-}
#endif

deriving via
  AsInteger Int8
  instance
    KnownTypeAst tyname DefaultUni Int8
instance KnownBuiltinTypeIn DefaultUni term Integer => MakeKnownIn DefaultUni term Int8 where
  makeKnown :: Int8 -> BuiltinResult term
makeKnown = Int8 -> BuiltinResult term
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a) =>
a -> BuiltinResult term
makeKnownAsInteger
  {-# INLINE makeKnown #-}
instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni term Int8 where
  readKnown :: term -> ReadKnownM Int8
readKnown = term -> ReadKnownM Int8
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a, Bounded a,
 Typeable a) =>
term -> ReadKnownM a
readKnownAsInteger
  {-# INLINE readKnown #-}

deriving via
  AsInteger Int16
  instance
    KnownTypeAst tyname DefaultUni Int16
instance KnownBuiltinTypeIn DefaultUni term Integer => MakeKnownIn DefaultUni term Int16 where
  makeKnown :: Int16 -> BuiltinResult term
makeKnown = Int16 -> BuiltinResult term
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a) =>
a -> BuiltinResult term
makeKnownAsInteger
  {-# INLINE makeKnown #-}
instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni term Int16 where
  readKnown :: term -> ReadKnownM Int16
readKnown = term -> ReadKnownM Int16
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a, Bounded a,
 Typeable a) =>
term -> ReadKnownM a
readKnownAsInteger
  {-# INLINE readKnown #-}

deriving via
  AsInteger Int32
  instance
    KnownTypeAst tyname DefaultUni Int32
instance KnownBuiltinTypeIn DefaultUni term Integer => MakeKnownIn DefaultUni term Int32 where
  makeKnown :: Int32 -> BuiltinResult term
makeKnown = Int32 -> BuiltinResult term
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a) =>
a -> BuiltinResult term
makeKnownAsInteger
  {-# INLINE makeKnown #-}
instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni term Int32 where
  readKnown :: term -> ReadKnownM Int32
readKnown = term -> ReadKnownM Int32
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a, Bounded a,
 Typeable a) =>
term -> ReadKnownM a
readKnownAsInteger
  {-# INLINE readKnown #-}

deriving via
  AsInteger Int64
  instance
    KnownTypeAst tyname DefaultUni Int64
instance KnownBuiltinTypeIn DefaultUni term Integer => MakeKnownIn DefaultUni term Int64 where
  makeKnown :: Int64 -> BuiltinResult term
makeKnown = Int64 -> BuiltinResult term
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a) =>
a -> BuiltinResult term
makeKnownAsInteger
  {-# INLINE makeKnown #-}
instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni term Int64 where
  readKnown :: term -> Either BuiltinError Int64
readKnown = term -> Either BuiltinError Int64
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a, Bounded a,
 Typeable a) =>
term -> ReadKnownM a
readKnownAsInteger
  {-# INLINE readKnown #-}

deriving via
  AsInteger Word8
  instance
    KnownTypeAst tyname DefaultUni Word8
instance KnownBuiltinTypeIn DefaultUni term Integer => MakeKnownIn DefaultUni term Word8 where
  makeKnown :: Word8 -> BuiltinResult term
makeKnown = Word8 -> BuiltinResult term
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a) =>
a -> BuiltinResult term
makeKnownAsInteger
  {-# INLINE makeKnown #-}
instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni term Word8 where
  readKnown :: term -> ReadKnownM Word8
readKnown = term -> ReadKnownM Word8
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a, Bounded a,
 Typeable a) =>
term -> ReadKnownM a
readKnownAsInteger
  {-# INLINE readKnown #-}

deriving via
  AsInteger Word16
  instance
    KnownTypeAst tyname DefaultUni Word16
instance KnownBuiltinTypeIn DefaultUni term Integer => MakeKnownIn DefaultUni term Word16 where
  makeKnown :: Word16 -> BuiltinResult term
makeKnown = Word16 -> BuiltinResult term
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a) =>
a -> BuiltinResult term
makeKnownAsInteger
  {-# INLINE makeKnown #-}
instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni term Word16 where
  readKnown :: term -> ReadKnownM Word16
readKnown = term -> ReadKnownM Word16
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a, Bounded a,
 Typeable a) =>
term -> ReadKnownM a
readKnownAsInteger
  {-# INLINE readKnown #-}

deriving via
  AsInteger Word32
  instance
    KnownTypeAst tyname DefaultUni Word32
instance KnownBuiltinTypeIn DefaultUni term Integer => MakeKnownIn DefaultUni term Word32 where
  makeKnown :: Word32 -> BuiltinResult term
makeKnown = Word32 -> BuiltinResult term
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a) =>
a -> BuiltinResult term
makeKnownAsInteger
  {-# INLINE makeKnown #-}
instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni term Word32 where
  readKnown :: term -> ReadKnownM Word32
readKnown = term -> ReadKnownM Word32
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a, Bounded a,
 Typeable a) =>
term -> ReadKnownM a
readKnownAsInteger
  {-# INLINE readKnown #-}

deriving via
  AsInteger Word64
  instance
    KnownTypeAst tyname DefaultUni Word64
instance KnownBuiltinTypeIn DefaultUni term Integer => MakeKnownIn DefaultUni term Word64 where
  makeKnown :: Word64 -> BuiltinResult term
makeKnown = Word64 -> BuiltinResult term
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a) =>
a -> BuiltinResult term
makeKnownAsInteger
  {-# INLINE makeKnown #-}
instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni term Word64 where
  readKnown :: term -> Either BuiltinError Word64
readKnown = term -> Either BuiltinError Word64
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a, Bounded a,
 Typeable a) =>
term -> ReadKnownM a
readKnownAsInteger
  {-# INLINE readKnown #-}

deriving newtype instance
  KnownTypeAst tyname DefaultUni NumBytesCostedAsNumWords
instance
  KnownBuiltinTypeIn DefaultUni term Integer
  => MakeKnownIn DefaultUni term NumBytesCostedAsNumWords
  where
  makeKnown :: NumBytesCostedAsNumWords -> BuiltinResult term
makeKnown = forall b term a.
(MakeKnownIn DefaultUni term b, Coercible a b) =>
a -> BuiltinResult term
makeKnownCoerce @Integer
  {-# INLINE makeKnown #-}

instance
  KnownBuiltinTypeIn DefaultUni term Integer
  => ReadKnownIn DefaultUni term NumBytesCostedAsNumWords
  where
  readKnown :: term -> ReadKnownM NumBytesCostedAsNumWords
readKnown = forall b term a.
(ReadKnownIn DefaultUni term b, Coercible b a) =>
term -> ReadKnownM a
readKnownCoerce @Integer
  {-# INLINE readKnown #-}

deriving newtype instance
  KnownTypeAst tyname DefaultUni IntegerCostedLiterally
instance
  KnownBuiltinTypeIn DefaultUni term Integer
  => MakeKnownIn DefaultUni term IntegerCostedLiterally
  where
  makeKnown :: IntegerCostedLiterally -> BuiltinResult term
makeKnown = forall b term a.
(MakeKnownIn DefaultUni term b, Coercible a b) =>
a -> BuiltinResult term
makeKnownCoerce @Integer
  {-# INLINE makeKnown #-}
instance
  KnownBuiltinTypeIn DefaultUni term Integer
  => ReadKnownIn DefaultUni term IntegerCostedLiterally
  where
  readKnown :: term -> ReadKnownM IntegerCostedLiterally
readKnown = forall b term a.
(ReadKnownIn DefaultUni term b, Coercible b a) =>
term -> ReadKnownM a
readKnownCoerce @Integer
  {-# INLINE readKnown #-}

deriving newtype instance
  KnownTypeAst tyname DefaultUni ValueTotalSize
instance
  KnownBuiltinTypeIn DefaultUni term Value
  => MakeKnownIn DefaultUni term ValueTotalSize
  where
  makeKnown :: ValueTotalSize -> BuiltinResult term
makeKnown = forall b term a.
(MakeKnownIn DefaultUni term b, Coercible a b) =>
a -> BuiltinResult term
makeKnownCoerce @Value
  {-# INLINE makeKnown #-}
instance
  KnownBuiltinTypeIn DefaultUni term Value
  => ReadKnownIn DefaultUni term ValueTotalSize
  where
  readKnown :: term -> ReadKnownM ValueTotalSize
readKnown = forall b term a.
(ReadKnownIn DefaultUni term b, Coercible b a) =>
term -> ReadKnownM a
readKnownCoerce @Value
  {-# INLINE readKnown #-}

deriving newtype instance
  KnownTypeAst tyname DefaultUni ValueMaxDepth
instance
  KnownBuiltinTypeIn DefaultUni term Value
  => MakeKnownIn DefaultUni term ValueMaxDepth
  where
  makeKnown :: ValueMaxDepth -> BuiltinResult term
makeKnown = forall b term a.
(MakeKnownIn DefaultUni term b, Coercible a b) =>
a -> BuiltinResult term
makeKnownCoerce @Value
  {-# INLINE makeKnown #-}
instance
  KnownBuiltinTypeIn DefaultUni term Value
  => ReadKnownIn DefaultUni term ValueMaxDepth
  where
  readKnown :: term -> ReadKnownM ValueMaxDepth
readKnown = forall b term a.
(ReadKnownIn DefaultUni term b, Coercible b a) =>
term -> ReadKnownM a
readKnownCoerce @Value
  {-# INLINE readKnown #-}

deriving newtype instance
  KnownTypeAst tyname DefaultUni DataNodeCount
instance
  KnownBuiltinTypeIn DefaultUni term Value
  => MakeKnownIn DefaultUni term DataNodeCount
  where
  makeKnown :: DataNodeCount -> BuiltinResult term
makeKnown = forall b term a.
(MakeKnownIn DefaultUni term b, Coercible a b) =>
a -> BuiltinResult term
makeKnownCoerce @Data
  {-# INLINE makeKnown #-}
instance
  KnownBuiltinTypeIn DefaultUni term Value
  => ReadKnownIn DefaultUni term DataNodeCount
  where
  readKnown :: term -> ReadKnownM DataNodeCount
readKnown = forall b term a.
(ReadKnownIn DefaultUni term b, Coercible b a) =>
term -> ReadKnownM a
readKnownCoerce @Data
  {-# INLINE readKnown #-}

deriving via
  AsInteger Natural
  instance
    KnownTypeAst tyname DefaultUni Natural
instance
  KnownBuiltinTypeIn DefaultUni term Integer
  => MakeKnownIn DefaultUni term Natural
  where
  makeKnown :: Natural -> BuiltinResult term
makeKnown = Natural -> BuiltinResult term
forall term a.
(KnownBuiltinTypeIn DefaultUni term Integer, Integral a) =>
a -> BuiltinResult term
makeKnownAsInteger
  {-# INLINE makeKnown #-}
instance
  KnownBuiltinTypeIn DefaultUni term Integer
  => ReadKnownIn DefaultUni term Natural
  where
  readKnown :: term -> ReadKnownM Natural
readKnown term
term =
    -- See Note [Performance of ReadKnownIn and MakeKnownIn instances].
    -- Funnily, we don't really need 'inline' here, unlike in the default implementation of
    -- 'readKnown' (go figure why), but we still use it just to be sure.
    (term -> ReadKnownM Integer) -> term -> ReadKnownM Integer
forall a. a -> a
inline term -> ReadKnownM Integer
forall val a. KnownBuiltinType val a => val -> ReadKnownM a
readKnownConstant term
term ReadKnownM Integer
-> (Integer -> ReadKnownM Natural) -> ReadKnownM Natural
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
>>= (Integer -> ReadKnownM Natural) -> Integer -> ReadKnownM Natural
forall a b. (a -> b) -> a -> b
oneShot \(Integer
i :: Integer) ->
      -- TODO: benchmark alternatives:signumInteger,integerIsNegative,integerToNaturalThrow
      if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
        -- TODO: benchmark alternatives: ghc>=9 integerToNatural
        then Natural -> ReadKnownM Natural
forall a. a -> Either BuiltinError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Natural -> ReadKnownM Natural) -> Natural -> ReadKnownM Natural
forall a b. (a -> b) -> a -> b
$ Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i
        else
          BuiltinError -> ReadKnownM Natural
forall a. BuiltinError -> Either BuiltinError a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (BuiltinError -> ReadKnownM Natural)
-> (Text -> BuiltinError) -> Text -> ReadKnownM Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> BuiltinError
operationalUnliftingError (Text -> ReadKnownM Natural) -> Text -> ReadKnownM Natural
forall a b. (a -> b) -> a -> b
$
            [Text] -> Text
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
              [ String -> Text
Text.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Integer -> String
forall a. Show a => a -> String
show Integer
i
              , Text
" is not within the bounds of Natural"
              ]
  {-# INLINE readKnown #-}

outOfBoundsErr :: Pretty a => a -> Vector.Vector term -> Text
outOfBoundsErr :: forall a term. Pretty a => a -> Vector term -> Text
outOfBoundsErr a
x Vector term
branches =
  [Text] -> Text
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
    [ Text
"'case "
    , a -> Text
forall str a. (Pretty a, Render str) => a -> str
display a
x
    , Text
"' is out of bounds for the given number of branches: "
    , Int -> Text
forall str a. (Pretty a, Render str) => a -> str
display (Int -> Text) -> Int -> Text
forall a b. (a -> b) -> a -> b
$ Vector term -> Int
forall a. Vector a -> Int
Vector.length Vector term
branches
    ]

instance AnnotateCaseBuiltin DefaultUni where
  annotateCaseBuiltin :: forall term ann.
(UniOf term ~ DefaultUni) =>
Type TyName DefaultUni ann
-> [term] -> Either Text [(term, [Type TyName DefaultUni ann])]
annotateCaseBuiltin Type TyName DefaultUni ann
ty [term]
branches = case Type TyName DefaultUni ann
ty of
    TyBuiltin ann
_ (SomeTypeIn DefaultUni (Esc a)
DefaultUniUnit) ->
      case [term]
branches of
        [term
x] -> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. b -> Either a b
Right [(term
x, [])]
        [term]
_ -> Text -> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. a -> Either a b
Left Text
"Casing on unit only allows exactly one branch"
    TyBuiltin ann
_ (SomeTypeIn DefaultUni (Esc a)
DefaultUniBool) ->
      case [term]
branches of
        [term
f] -> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. b -> Either a b
Right [(term
f, [])]
        [term
f, term
t] -> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. b -> Either a b
Right [(term
f, []), (term
t, [])]
        [term]
_ -> Text -> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. a -> Either a b
Left Text
"Casing on bool requires exactly one branch or two branches"
    TyBuiltin ann
_ (SomeTypeIn DefaultUni (Esc a)
DefaultUniInteger) ->
      [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. b -> Either a b
Right ([(term, [Type TyName DefaultUni ann])]
 -> Either Text [(term, [Type TyName DefaultUni ann])])
-> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. (a -> b) -> a -> b
$ (term -> (term, [Type TyName DefaultUni ann]))
-> [term] -> [(term, [Type TyName DefaultUni ann])]
forall a b. (a -> b) -> [a] -> [b]
map (,[]) [term]
branches
    listTy :: Type TyName DefaultUni ann
listTy@(TyApp ann
_ (TyBuiltin ann
_ (SomeTypeIn DefaultUni (Esc a)
DefaultUniProtoList)) Type TyName DefaultUni ann
argTy) ->
      case [term]
branches of
        [term
cons] -> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. b -> Either a b
Right [(term
cons, [Type TyName DefaultUni ann
argTy, Type TyName DefaultUni ann
listTy])]
        [term
cons, term
nil] -> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. b -> Either a b
Right [(term
cons, [Type TyName DefaultUni ann
argTy, Type TyName DefaultUni ann
listTy]), (term
nil, [])]
        [term]
_ -> Text -> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. a -> Either a b
Left Text
"Casing on list requires exactly one branch or two branches"
    (TyApp ann
_ (TyApp ann
_ (TyBuiltin ann
_ (SomeTypeIn DefaultUni (Esc a)
DefaultUniProtoPair)) Type TyName DefaultUni ann
lTyArg) Type TyName DefaultUni ann
rTyArg) ->
      case [term]
branches of
        [term
f] -> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. b -> Either a b
Right [(term
f, [Type TyName DefaultUni ann
lTyArg, Type TyName DefaultUni ann
rTyArg])]
        [term]
_ -> Text -> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. a -> Either a b
Left Text
"Casing on pair requires exactly one branch"
    Type TyName DefaultUni ann
_ -> Text -> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. a -> Either a b
Left (Text -> Either Text [(term, [Type TyName DefaultUni ann])])
-> Text -> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. (a -> b) -> a -> b
$ Type TyName DefaultUni () -> Text
forall str a. (Pretty a, Render str) => a -> str
display (Type TyName DefaultUni ann -> Type TyName DefaultUni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName DefaultUni ann
ty) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" isn't supported in 'case'"

instance CaseBuiltin DefaultUni where
  caseBuiltin :: forall term.
(UniOf term ~ DefaultUni) =>
Some (ValueOf DefaultUni)
-> Vector term -> HeadSpine Text term (Some (ValueOf DefaultUni))
caseBuiltin someVal :: Some (ValueOf DefaultUni)
someVal@(Some (ValueOf DefaultUni (Esc a)
uni a
x)) Vector term
branches = case DefaultUni (Esc a)
uni of
    DefaultUni (Esc a)
DefaultUniUnit
      | Int
1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
len -> term -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall err a b. a -> HeadSpine err a b
HeadOnly (term -> HeadSpine Text term (Some (ValueOf DefaultUni)))
-> term -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Int
0
      | Bool
otherwise -> Text -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall err a b. err -> HeadSpine err a b
HeadError (Text -> HeadSpine Text term (Some (ValueOf DefaultUni)))
-> Text -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ Some (ValueOf DefaultUni) -> Vector term -> Text
forall a term. Pretty a => a -> Vector term -> Text
outOfBoundsErr Some (ValueOf DefaultUni)
someVal Vector term
branches
    DefaultUni (Esc a)
DefaultUniBool -> case a
x of
      -- We allow there to be only one branch as long as the scrutinee is 'False'.
      -- This is strictly to save size by not having the 'True' branch if it was gonna be
      -- 'Error' anyway.
      a
Bool
False | Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
|| Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 -> term -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall err a b. a -> HeadSpine err a b
HeadOnly (term -> HeadSpine Text term (Some (ValueOf DefaultUni)))
-> term -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Int
0
      a
Bool
True | Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 -> term -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall err a b. a -> HeadSpine err a b
HeadOnly (term -> HeadSpine Text term (Some (ValueOf DefaultUni)))
-> term -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Int
1
      a
_ -> Text -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall err a b. err -> HeadSpine err a b
HeadError (Text -> HeadSpine Text term (Some (ValueOf DefaultUni)))
-> Text -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ Some (ValueOf DefaultUni) -> Vector term -> Text
forall a term. Pretty a => a -> Vector term -> Text
outOfBoundsErr Some (ValueOf DefaultUni)
someVal Vector term
branches
    DefaultUni (Esc a)
DefaultUniInteger
      | a
0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
x Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
len -> term -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall err a b. a -> HeadSpine err a b
HeadOnly (term -> HeadSpine Text term (Some (ValueOf DefaultUni)))
-> term -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Integer -> Int
forall a. Num a => Integer -> a
fromInteger a
Integer
x
      | Bool
otherwise -> Text -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall err a b. err -> HeadSpine err a b
HeadError (Text -> HeadSpine Text term (Some (ValueOf DefaultUni)))
-> Text -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ Some (ValueOf DefaultUni) -> Vector term -> Text
forall a term. Pretty a => a -> Vector term -> Text
outOfBoundsErr Some (ValueOf DefaultUni)
someVal Vector term
branches
    DefaultUniList DefaultUni (Esc a1)
ty
      | Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 ->
          case a
x of
            [] -> Text -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall err a b. err -> HeadSpine err a b
HeadError Text
"Expected non-empty list, got empty list for casing list"
            (a1
y : [a1]
ys) -> term
-> [Some (ValueOf DefaultUni)]
-> HeadSpine Text term (Some (ValueOf DefaultUni))
forall a b err. a -> [b] -> HeadSpine err a b
headSpine (Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Int
0) [DefaultUni (Esc a1) -> a1 -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a1)
DefaultUni (Esc a1)
ty a1
y, DefaultUni (Esc a) -> a -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a)
uni a
[a1]
ys]
      | Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 ->
          case a
x of
            [] -> term -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall err a b. a -> HeadSpine err a b
HeadOnly (term -> HeadSpine Text term (Some (ValueOf DefaultUni)))
-> term -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Int
1
            (a1
y : [a1]
ys) -> term
-> [Some (ValueOf DefaultUni)]
-> HeadSpine Text term (Some (ValueOf DefaultUni))
forall a b err. a -> [b] -> HeadSpine err a b
headSpine (Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Int
0) [DefaultUni (Esc a1) -> a1 -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a1)
DefaultUni (Esc a1)
ty a1
y, DefaultUni (Esc a) -> a -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a)
uni a
[a1]
ys]
      | Bool
otherwise -> Text -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall err a b. err -> HeadSpine err a b
HeadError (Text -> HeadSpine Text term (Some (ValueOf DefaultUni)))
-> Text -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ Some (ValueOf DefaultUni) -> Vector term -> Text
forall a term. Pretty a => a -> Vector term -> Text
outOfBoundsErr Some (ValueOf DefaultUni)
someVal Vector term
branches
    DefaultUniPair DefaultUni (Esc a2)
tyL DefaultUni (Esc a1)
tyR
      | Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 ->
          case a
x of
            (a2
l, a1
r) -> term
-> [Some (ValueOf DefaultUni)]
-> HeadSpine Text term (Some (ValueOf DefaultUni))
forall a b err. a -> [b] -> HeadSpine err a b
headSpine (Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Int
0) [DefaultUni (Esc a2) -> a2 -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a2)
DefaultUni (Esc a2)
tyL a2
l, DefaultUni (Esc a1) -> a1 -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a1)
DefaultUni (Esc a1)
tyR a1
r]
      | Bool
otherwise -> Text -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall err a b. err -> HeadSpine err a b
HeadError (Text -> HeadSpine Text term (Some (ValueOf DefaultUni)))
-> Text -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ Some (ValueOf DefaultUni) -> Vector term -> Text
forall a term. Pretty a => a -> Vector term -> Text
outOfBoundsErr Some (ValueOf DefaultUni)
someVal Vector term
branches
    DefaultUni (Esc a)
_ -> Text -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall err a b. err -> HeadSpine err a b
HeadError (Text -> HeadSpine Text term (Some (ValueOf DefaultUni)))
-> Text -> HeadSpine Text term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc a) -> Text
forall str a. (Pretty a, Render str) => a -> str
display DefaultUni (Esc a)
uni Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" isn't supported in 'case'"
    where
      !len :: Int
len = Vector term -> Int
forall a. Vector a -> Int
Vector.length Vector term
branches
  {-# INLINE caseBuiltin #-}

{- 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 TPLC]
-}

instance Closed DefaultUni where
  type
    DefaultUni `Everywhere` constr =
      ( constr `Permits` Integer
      , constr `Permits` ByteString
      , constr `Permits` Text
      , constr `Permits` ()
      , constr `Permits` Bool
      , constr `Permits` Value
      , constr `Permits` []
      , constr `Permits` Strict.Vector
      , constr `Permits` (,)
      , constr `Permits` Data
      , constr `Permits` BLS12_381.G1.Element
      , constr `Permits` BLS12_381.G2.Element
      , constr `Permits` BLS12_381.Pairing.MlResult
      )

  -- See Note [Stable encoding of tags].
  -- IF YOU'RE GETTING A WARNING HERE, DON'T FORGET TO AMEND 'withDecodedUni' RIGHT BELOW.
  encodeUni :: forall a. 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 a. DefaultUni a -> [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 a. DefaultUni a -> [Int]
forall (uni :: * -> *) a. Closed uni => uni a -> [Int]
encodeUni DefaultUni (Esc a)
uniA
  encodeUni DefaultUni a
DefaultUniData = [Int
8]
  encodeUni DefaultUni a
DefaultUniBLS12_381_G1_Element = [Int
9]
  encodeUni DefaultUni a
DefaultUniBLS12_381_G2_Element = [Int
10]
  encodeUni DefaultUni a
DefaultUniBLS12_381_MlResult = [Int
11]
  encodeUni DefaultUni a
DefaultUniProtoArray = [Int
12]
  encodeUni DefaultUni a
DefaultUniValue = [Int
13]

  -- See Note [Decoding universes].
  -- See Note [Stable encoding of tags].
  withDecodedUni :: forall r.
(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 a b. DecodeUniM a -> (a -> DecodeUniM b) -> DecodeUniM b
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 (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 (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
9 -> DefaultUni (Esc Element) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc Element)
DefaultUniBLS12_381_G1_Element
      Int
10 -> DefaultUni (Esc Element) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc Element)
DefaultUniBLS12_381_G2_Element
      Int
11 -> DefaultUni (Esc MlResult) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc MlResult)
DefaultUniBLS12_381_MlResult
      Int
12 -> DefaultUni (Esc Vector) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc Vector)
DefaultUniProtoArray
      Int
13 -> DefaultUni (Esc Value) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc Value)
DefaultUniValue
      Int
_ -> DecodeUniM r
forall a. DecodeUniM a
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 :: forall (constr :: * -> Constraint) a r
       (proxy :: (* -> Constraint) -> *).
Everywhere DefaultUni constr =>
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
forall (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
Everywhere DefaultUni constr =>
proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
bring proxy constr
p DefaultUni (Esc a)
DefaultUni (Esc a)
uniA r
constr a => r
constr a => r
r
  bring proxy constr
p (DefaultUni (Esc f)
DefaultUniProtoArray `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
forall (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
Everywhere DefaultUni constr =>
proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
bring proxy constr
p DefaultUni (Esc a)
DefaultUni (Esc a)
uniA r
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
forall (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
Everywhere DefaultUni constr =>
proxy constr -> DefaultUni (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
forall (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
Everywhere DefaultUni constr =>
proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
bring proxy constr
p DefaultUni (Esc a)
DefaultUni (Esc a)
uniB r
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
  bring proxy constr
_ DefaultUni (Esc a)
DefaultUniBLS12_381_G1_Element constr a => r
r = r
constr a => r
r
  bring proxy constr
_ DefaultUni (Esc a)
DefaultUniBLS12_381_G2_Element constr a => r
r = r
constr a => r
r
  bring proxy constr
_ DefaultUni (Esc a)
DefaultUniBLS12_381_MlResult constr a => r
r = r
constr a => r
r
  bring proxy constr
_ DefaultUni (Esc a)
DefaultUniValue constr a => r
r = r
constr a => r
r