-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

{- | Module, containing restrictions imposed by instruction or value scope.

Michelson have multiple restrictions on values, examples:

* @operation@ type cannot appear in parameter.
* @big_map@ type cannot appear in @PUSH@-able constants.
* @contract@ type cannot appear in type we @UNPACK@ to.

Thus we declare multiple "scopes" - constraints applied in corresponding
situations, for instance

* 'ParameterScope';
* 'StorageScope';
* 'ConstantScope'.

Also we separate multiple "classes" of scope-related constraints.

* 'ParameterScope' and similar ones are used within Michelson engine,
they are understandable by GHC but produce not very clarifying errors.

* 'ProperParameterBetterErrors' and similar ones are middle-layer constraints,
they produce human-readable errors but GHC cannot make conclusions from them.
They are supposed to be used only by eDSLs to define their own high-level
constraints.

* Lorentz and other eDSLs may declare their own constraints, in most cases
you should use them. For example see @Lorentz.Constraints@ module.

-}

module Morley.Michelson.Typed.Scope
  ( -- * Scopes
    ConstantScope
  , DupableScope
  , StorageScope
  , PackedValScope
  , ParameterScope
  , UntypedValScope
  , UnpackedValScope
  , ViewableScope
  , ComparabilityScope

  , ProperParameterBetterErrors
  , ProperStorageBetterErrors
  , ProperConstantBetterErrors
  , ProperDupableBetterErrors
  , ProperPackedValBetterErrors
  , ProperUnpackedValBetterErrors
  , ProperUntypedValBetterErrors
  , ProperViewableBetterErrors
  , ProperNonComparableValBetterErrors

  , IsDupableScope

  , properParameterEvi
  , properStorageEvi
  , properConstantEvi
  , properDupableEvi
  , properPackedValEvi
  , properUnpackedValEvi
  , properViewableEvi
  , properUntypedValEvi
  , (:-)(..)

  , BadTypeForScope (..)
  , CheckScope (..)
  , WithDeMorganScope (..)
  , Comparable (..)
  , WellTyped (..)
  , NotWellTyped (..)

    -- * Implementation internals
  , HasNoBigMap
  , HasNoNestedBigMaps
  , HasNoOp
  , HasNoContract
  , HasNoTicket
  , ContainsBigMap
  , ContainsContract
  , ContainsNestedBigMaps
  , ContainsOp
  , ContainsTicket
  , IsComparable

  , ForbidOp
  , ForbidContract
  , ForbidTicket
  , ForbidBigMap
  , ForbidNestedBigMaps
  , ForbidNonComparable
  , FailOnBigMapFound
  , FailOnContractFound
  , FailOnNestedBigMapsFound
  , FailOnOperationFound
  , FailOnTicketFound
  , FailOnNonComparableFound

  , OpPresence (..)
  , ContractPresence (..)
  , TicketPresence (..)
  , BigMapPresence (..)
  , NestedBigMapsPresence (..)
  , checkOpPresence
  , checkContractTypePresence
  , checkTicketPresence
  , checkBigMapPresence
  , checkNestedBigMapsPresence
  , comparabilityPresence
  , opAbsense
  , contractTypeAbsense
  , bigMapAbsense
  , nestedBigMapsAbsense
  , forbiddenOp
  , forbiddenContractType
  , forbiddenBigMap
  , forbiddenNestedBigMaps

  , Comparability(..)
  , checkComparability
  , getComparableProofS

  , getWTP
  , getWTP'
    -- * Re-exports
  , withDict
  , SingI (..)
  ) where

import Data.Bool.Singletons (SBool(..))
import Data.Constraint (Dict(..), withDict, (:-)(..))
import Data.Singletons
  (SLambda(..), Sing, SingI(..), fromSing, type (@@), type (~>), type Apply, withSingI, (@@))
import Data.Type.Bool (Not, type (&&), type (||))
import Fmt (Buildable(..))
import GHC.TypeLits (ErrorMessage(..), TypeError)

import Data.Type.Equality ((:~:)(..))
import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDoc)
import Morley.Michelson.Typed.Sing (SingT(..))
import Morley.Michelson.Typed.T (T(..))
import Morley.Util.Type (FailUnless, FailWhen)
import Unsafe.Coerce (unsafeCoerce)

----------------------------------------------------------------------------
-- Constraints
----------------------------------------------------------------------------
-- | Whether a value of this type _may_ contain an operation.
--
-- In some scopes (constants, parameters, storage) appearing for operation type
-- is prohibited.
-- Operations in input/output of lambdas are allowed without limits though.
type family ContainsOp (t :: T) :: Bool where
  ContainsOp 'TKey = 'False
  ContainsOp 'TUnit = 'False
  ContainsOp 'TSignature = 'False
  ContainsOp 'TChainId = 'False
  ContainsOp ('TOption t) = ContainsOp t
  ContainsOp ('TList t) = ContainsOp t
  ContainsOp ('TSet t) = ContainsOp t
  ContainsOp 'TOperation = 'True
  ContainsOp ('TContract _) = 'False
  ContainsOp ('TTicket t) = ContainsOp t
  ContainsOp ('TPair a b) = ContainsOp a || ContainsOp b
  ContainsOp ('TOr a b) = ContainsOp a || ContainsOp b
  ContainsOp ('TLambda _ _) = 'False
  ContainsOp ('TMap k v) = ContainsOp k || ContainsOp v
  ContainsOp ('TBigMap k v) = ContainsOp k || ContainsOp v
  ContainsOp _ = 'False

-- | Whether a value of this type _may_ contain a @contract@ value.
--
-- In some scopes (constants, storage) appearing for contract type
-- is prohibited.
-- Contracts in input/output of lambdas are allowed without limits though.
type family ContainsContract (t :: T) :: Bool where
  ContainsContract 'TKey = 'False
  ContainsContract 'TUnit = 'False
  ContainsContract 'TSignature = 'False
  ContainsContract 'TChainId = 'False
  ContainsContract ('TOption t) = ContainsContract t
  ContainsContract ('TList t) = ContainsContract t
  ContainsContract ('TSet _) = 'False
  ContainsContract 'TOperation = 'False
  ContainsContract ('TContract _) = 'True
  ContainsContract ('TPair a b) = ContainsContract a || ContainsContract b
  ContainsContract ('TOr a b) = ContainsContract a || ContainsContract b
  ContainsContract ('TLambda _ _) = 'False
  ContainsContract ('TMap _ v) = ContainsContract v
  ContainsContract ('TBigMap _ v) = ContainsContract v
  ContainsContract _ = 'False

-- | Whether a value of this type _may_ contain a @ticket@ value.
type family ContainsTicket (t :: T) :: Bool where
  ContainsTicket ('TOption t) = ContainsTicket t
  ContainsTicket ('TList t) = ContainsTicket t
  ContainsTicket ('TSet _) = 'False
  ContainsTicket ('TTicket _) = 'True
  ContainsTicket ('TPair a b) = ContainsTicket a || ContainsTicket b
  ContainsTicket ('TOr a b) = ContainsTicket a || ContainsTicket b
  ContainsTicket ('TLambda _ _) = 'False
  ContainsTicket ('TMap _ v) = ContainsTicket v
  ContainsTicket ('TBigMap _ v) = ContainsTicket v
  ContainsTicket _ = 'False

-- | Whether a value of this type _may_ contain a @big_map@ value.
type family ContainsBigMap (t :: T) :: Bool where
  ContainsBigMap 'TKey = 'False
  ContainsBigMap 'TUnit = 'False
  ContainsBigMap 'TSignature = 'False
  ContainsBigMap 'TChainId = 'False
  ContainsBigMap ('TOption t) = ContainsBigMap t
  ContainsBigMap ('TList t) = ContainsBigMap t
  ContainsBigMap ('TSet _) = 'False
  ContainsBigMap 'TOperation = 'False
  ContainsBigMap ('TContract _) = 'False
  ContainsBigMap ('TPair a b) = ContainsBigMap a || ContainsBigMap b
  ContainsBigMap ('TOr a b) = ContainsBigMap a || ContainsBigMap b
  ContainsBigMap ('TLambda _ _) = 'False
  ContainsBigMap ('TMap _ v) = ContainsBigMap v
  ContainsBigMap ('TBigMap _ _) = 'True
  ContainsBigMap _ = 'False

-- | Whether a value of this type _may_ contain nested @big_map@s.
--
-- Nested big_maps (i.e. big_map which contains another big_map inside of it's value type) are
-- prohibited in all contexts. Some context such as PUSH, APPLY, PACK/UNPACK instructions are more
-- strict because they don't work with big_map at all.
type family ContainsNestedBigMaps (t :: T) :: Bool where
  ContainsNestedBigMaps 'TKey = 'False
  ContainsNestedBigMaps 'TUnit = 'False
  ContainsNestedBigMaps 'TSignature = 'False
  ContainsNestedBigMaps 'TChainId = 'False
  ContainsNestedBigMaps ('TOption t) = ContainsNestedBigMaps t
  ContainsNestedBigMaps ('TList t) = ContainsNestedBigMaps t
  ContainsNestedBigMaps ('TSet _) = 'False
  ContainsNestedBigMaps 'TOperation = 'False
  ContainsNestedBigMaps ('TContract _) = 'False
  ContainsNestedBigMaps ('TPair a b) = ContainsNestedBigMaps a || ContainsNestedBigMaps b
  ContainsNestedBigMaps ('TOr a b) = ContainsNestedBigMaps a || ContainsNestedBigMaps b
  ContainsNestedBigMaps ('TLambda _ _) = 'False
  ContainsNestedBigMaps ('TMap _ v) = ContainsNestedBigMaps v
  ContainsNestedBigMaps ('TBigMap _ v) = ContainsBigMap v
  ContainsNestedBigMaps _ = 'False

-- | Whether a value of this type _may_ contain a @samping_state@ value.
type family ContainsSaplingState (t :: T) :: Bool where
  ContainsSaplingState ('TOption t) = ContainsSaplingState t
  ContainsSaplingState ('TList t) = ContainsSaplingState t
  ContainsSaplingState ('TPair a b) = ContainsSaplingState a || ContainsSaplingState b
  ContainsSaplingState ('TOr a b) = ContainsSaplingState a || ContainsSaplingState b
  ContainsSaplingState ('TMap _ v) = ContainsSaplingState v
  ContainsSaplingState ('TBigMap _ v) = ContainsSaplingState v
  ContainsSaplingState ('TSaplingState _) = 'True
  ContainsSaplingState _ = 'False

-- | Constraint which ensures that type is comparable.
type family IsComparable (t :: T) :: Bool where
  IsComparable ('TPair a b) =  IsComparable a && IsComparable b
  IsComparable ('TOption t) = IsComparable t
  IsComparable 'TBls12381Fr = 'False
  IsComparable 'TBls12381G1 = 'False
  IsComparable 'TBls12381G2 = 'False
  IsComparable ('TList _) = 'False
  IsComparable ('TSet _) = 'False
  IsComparable 'TOperation = 'False
  IsComparable ('TContract _) = 'False
  IsComparable ('TTicket _) = 'False
  IsComparable ('TOr a b) = IsComparable a && IsComparable b
  IsComparable ('TLambda _ _) = 'False
  IsComparable ('TMap _ _) = 'False
  IsComparable ('TBigMap _ _) = 'False
  IsComparable 'TChest = 'False
  IsComparable 'TChestKey = 'False
  IsComparable ('TSaplingState _) = 'False
  IsComparable ('TSaplingTransaction _) = 'False
  IsComparable _            = 'True

-- | Constraint which ensures that a value of type @t@ does not contain operations.
--
-- Not just a type alias in order to be able to partially apply it
-- (e.g. in 'Each').
class (ContainsOp t ~ 'False) => HasNoOp t
instance (ContainsOp t ~ 'False) => HasNoOp t

-- | Constraint which ensures that a value of type @t@ does not contain @contract@ values.
class (ContainsContract t ~ 'False) => HasNoContract t
instance (ContainsContract t ~ 'False) => HasNoContract t

-- | Constraint which ensures that a value of type @t@ does not contain @ticket@ values.
class (ContainsTicket t ~ 'False) => HasNoTicket t
instance (ContainsTicket t ~ 'False) => HasNoTicket t

-- | Constraint which ensures that a value of type @t@ does not contain @big_map@ values.
class (ContainsBigMap t ~ 'False) => HasNoBigMap t
instance (ContainsBigMap t ~ 'False) => HasNoBigMap t

-- | Constraint which ensures that a value of type @t@ does not contain @sapling_state@ values.
class (ContainsSaplingState t ~ 'False) => HasNoSaplingState t
instance (ContainsSaplingState t ~ 'False) => HasNoSaplingState t

-- | Constraint which ensures that there are no nested bigmaps.
class (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t
instance (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t

{-# DEPRECATED
   FailOnOperationFound
 , FailOnContractFound
 , FailOnTicketFound
 , FailOnBigMapFound
 , FailOnNestedBigMapsFound
 , FailOnNonComparableFound
 "Use a Forbid* constraint instead"
 #-}
-- | Report a human-readable error about 'TOperation' at a wrong place.
type family FailOnOperationFound (enabled :: Bool) :: Constraint where
  FailOnOperationFound 'True =
    TypeError ('Text "Operations are not allowed in this scope")
  FailOnOperationFound 'False = ()

-- | Report a human-readable error about 'TContract' at a wrong place.
type family FailOnContractFound (enabled :: Bool) :: Constraint where
  FailOnContractFound 'True =
    TypeError ('Text "Type `contract` is not allowed in this scope")
  FailOnContractFound 'False = ()

-- | Report a human-readable error about 'TTicket' at a wrong place.
type family FailOnTicketFound (enabled :: Bool) :: Constraint where
  FailOnTicketFound 'True =
    TypeError ('Text "Type `ticket` is not allowed in this scope")
  FailOnTicketFound 'False = ()

-- | Report a human-readable error about 'TBigMap' at a wrong place.
type family FailOnBigMapFound (enabled :: Bool) :: Constraint where
  FailOnBigMapFound 'True =
    TypeError ('Text "BigMaps are not allowed in this scope")
  FailOnBigMapFound 'False = ()

-- | Report a human-readable error that 'TBigMap' contains another 'TBigMap'
type family FailOnNestedBigMapsFound (enabled :: Bool) :: Constraint where
  FailOnNestedBigMapsFound 'True =
    TypeError ('Text "Nested BigMaps are not allowed")
  FailOnNestedBigMapsFound 'False = ()

-- | Report a human-readable error that given value is not comparable
type family FailOnNonComparableFound (comparable :: Bool) :: Constraint where
  FailOnNonComparableFound 'True = ()
  FailOnNonComparableFound 'False =
    TypeError ('Text "Only comparable types are allowed here")

-- | This is like 'HasNoOp', it raises a more human-readable error
-- when @t@ type is concrete, and also imposes an equality constraint.
--
-- Use this constraint in our eDSL.
type ForbidOp t =
  FailWhen
    (ContainsOp t)
    ('Text "Operations are not allowed in this scope")

type ForbidContract t =
  FailWhen
    (ContainsContract t)
    ('Text "Type `contract` is not allowed in this scope")

type ForbidTicket t =
  FailWhen
    (ContainsTicket t)
    ('Text "Type `ticket` is not allowed in this scope")

type ForbidSaplingState t =
  FailWhen
    (ContainsSaplingState t)
    ('Text "Type `sapling_state` is not allowed in this scope")

type ForbidBigMap t =
  FailWhen
    (ContainsBigMap t)
    ('Text "BigMaps are not allowed in this scope")

type ForbidNestedBigMaps t =
  FailWhen
    (ContainsNestedBigMaps t)
    ('Text "Nested BigMaps are not allowed")

-- | Constraint that rises human-readable error message, in case given value
-- can't be compared
type ForbidNonComparable t =
  FailUnless
    (IsComparable t)
    ('Text "Only comparable types are allowed here")

{-# DEPRECATED forbiddenOp, forbiddenBigMap, forbiddenNestedBigMaps, forbiddenContractType
 "Simply delete this function wherever it occurs. It is no longer needed."
 #-}

-- | Deprecated and unused
forbiddenOp
  :: forall t a.
     ForbidOp t
  => (HasNoOp t => a)
  -> a
forbiddenOp :: forall (t :: T) a. ForbidOp t => (HasNoOp t => a) -> a
forbiddenOp HasNoOp t => a
a = a
HasNoOp t => a
a

-- | Deprecated and unused
forbiddenBigMap
  :: forall t a.
     ForbidBigMap t
  => (HasNoBigMap t => a)
  -> a
forbiddenBigMap :: forall (t :: T) a. ForbidBigMap t => (HasNoBigMap t => a) -> a
forbiddenBigMap HasNoBigMap t => a
a = a
HasNoBigMap t => a
a

-- | Deprecated and unused
forbiddenNestedBigMaps
  :: forall t a.
     ForbidNestedBigMaps t
  => (HasNoNestedBigMaps t => a)
  -> a
forbiddenNestedBigMaps :: forall (t :: T) a.
ForbidNestedBigMaps t =>
(HasNoNestedBigMaps t => a) -> a
forbiddenNestedBigMaps HasNoNestedBigMaps t => a
a = a
HasNoNestedBigMaps t => a
a

-- | Deprecated and unused
forbiddenContractType
  :: forall t a.
     ForbidContract t
  => (HasNoContract t => a)
  -> a
forbiddenContractType :: forall (t :: T) a. ForbidContract t => (HasNoContract t => a) -> a
forbiddenContractType HasNoContract t => a
a = a
HasNoContract t => a
a

-- | Whether a value of this type _may_ contain an operation.
data OpPresence (t :: T)
  = ContainsOp t ~ 'True => OpPresent
    -- ^ A value of type @t@ may or may not contain an operation.
  | ContainsOp t ~ 'False => OpAbsent
    -- ^ A value of type @t@ cannot contain @big_map@ values.

-- | Whether a value of this type _may_ contain a @contract@ value.
data ContractPresence (t :: T)
  = ContainsContract t ~ 'True => ContractPresent
    -- ^ A value of type @t@ may or may not contain a @contract@ value.
  | ContainsContract t ~ 'False => ContractAbsent
    -- ^ A value of type @t@ cannot contain @contract@ values.

-- | Whether a value of this type _may_ contain a @ticket@ value.
data TicketPresence (t :: T)
  = ContainsTicket t ~ 'True => TicketPresent
    -- ^ A value of type @t@ may or may not contain a @ticket@ value.
  | ContainsTicket t ~ 'False => TicketAbsent
    -- ^ A value of type @t@ cannot contain @ticket@ values.

-- | Whether a value of this type _may_ contain a @big_map@ value.
data BigMapPresence (t :: T)
  = ContainsBigMap t ~ 'True => BigMapPresent
    -- ^ A value of type @t@ may or may not contain a @big_map@ value.
  | ContainsBigMap t ~ 'False => BigMapAbsent
    -- ^ A value of type @t@ cannot contain @big_map@ values.

-- | Whether a value of this type _may_ contain nested @big_map@s.
data NestedBigMapsPresence (t :: T)
  = ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresent
    -- ^ A value of type @t@ may or may not contain nested @big_map@s.
  | ContainsNestedBigMaps t ~ 'False => NestedBigMapsAbsent
    -- ^ A value of type @t@ cannot contain nested @big_map@s.

-- | Whether a value of this type _may_ contain a @sapling_state@ value.
data SaplingStatePresence (t :: T)
  = ContainsSaplingState t ~ 'True => SaplingStatePresent
    -- ^ A value of type @t@ may or may not contain a @sapling_state@ value.
  | ContainsSaplingState t ~ 'False => SaplingStateAbsent
    -- ^ A value of type @t@ cannot contain @sapling_state@ values.

-- @rvem: IMO, generalization of OpPresence and BigMapPresence to
-- TPresence is not worth it, due to the fact that
-- it will require more boilerplate in checkTPresence implementation
-- than it is already done in checkOpPresence and checkBigMapPresence

-- | Check at runtime whether a value of the given type _may_ contain an operation.
checkOpPresence :: Sing (ty :: T) -> OpPresence ty
checkOpPresence :: forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence = \case
  -- This is a sad amount of boilerplate, but at least
  -- there is no chance to make a mistake in it.
  -- We can't do in a simpler way while requiring only @Sing ty@ / @SingI ty@,
  -- and a more complex constraint would be too unpleasant and confusing to
  -- propagate everywhere.
  Sing ty
SingT ty
STKey -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STSignature -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STChainId -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STUnit -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STOption Sing n
t -> case Sing n -> OpPresence n
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n
t of
    OpPresence n
OpPresent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    OpPresence n
OpAbsent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STList Sing n
t -> case Sing n -> OpPresence n
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n
t of
    OpPresence n
OpPresent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    OpPresence n
OpAbsent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STSet Sing n
a -> case Sing n -> OpPresence n
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n
a of
    OpPresence n
OpPresent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    OpPresence n
OpAbsent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STOperation -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
  STContract Sing n
_ -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STTicket Sing n
t -> case Sing n -> OpPresence n
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n
t of
    OpPresence n
OpPresent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    OpPresence n
OpAbsent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STPair Sing n1
a Sing n2
b -> case (Sing n1 -> OpPresence n1
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n1
a, Sing n2 -> OpPresence n2
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n2
b) of
    (OpPresence n1
OpPresent, OpPresence n2
_) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    (OpPresence n1
_, OpPresence n2
OpPresent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    (OpPresence n1
OpAbsent, OpPresence n2
OpAbsent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STOr Sing n1
a Sing n2
b -> case (Sing n1 -> OpPresence n1
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n1
a, Sing n2 -> OpPresence n2
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n2
b) of
    (OpPresence n1
OpPresent, OpPresence n2
_) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    (OpPresence n1
_, OpPresence n2
OpPresent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    (OpPresence n1
OpAbsent, OpPresence n2
OpAbsent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STLambda Sing n1
_ Sing n2
_ -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STMap Sing n1
k Sing n2
v -> case (Sing n1 -> OpPresence n1
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n1
k, Sing n2 -> OpPresence n2
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n2
v) of
    (OpPresence n1
OpAbsent, OpPresence n2
OpAbsent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
    (OpPresence n1
OpPresent, OpPresence n2
_) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    (OpPresence n1
_, OpPresence n2
OpPresent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
  STBigMap Sing n1
k Sing n2
v -> case (Sing n1 -> OpPresence n1
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n1
k, Sing n2 -> OpPresence n2
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n2
v) of
    (OpPresence n1
OpAbsent, OpPresence n2
OpAbsent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
    (OpPresence n1
OpPresent, OpPresence n2
_) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    (OpPresence n1
_, OpPresence n2
OpPresent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
  Sing ty
SingT ty
STInt -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STNat -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STString -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STBytes -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STMutez -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STBool -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STKeyHash -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STBls12381Fr -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STBls12381G1 -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STBls12381G2 -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STTimestamp -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STAddress -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STChest -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STChestKey -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STTxRollupL2Address -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  Sing ty
SingT ty
STNever -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STSaplingState Sing n
_ -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STSaplingTransaction Sing n
_ -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent

-- | Check at runtime whether a value of the given type _may_ contain a @contract@ value.
checkContractTypePresence :: Sing (ty :: T) -> ContractPresence ty
checkContractTypePresence :: forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence = \case
  Sing ty
SingT ty
STKey -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STSignature -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STChainId -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STUnit -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STOption Sing n
t -> case Sing n -> ContractPresence n
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n
t of
    ContractPresence n
ContractPresent -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    ContractPresence n
ContractAbsent -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STList Sing n
t -> case Sing n -> ContractPresence n
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n
t of
    ContractPresence n
ContractPresent -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    ContractPresence n
ContractAbsent -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STSet Sing n
_ -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STOperation -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STContract Sing n
_ -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
  STTicket Sing n
_ -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent  -- contract type is not allowed in tickets at all
  STPair Sing n1
a Sing n2
b -> case (Sing n1 -> ContractPresence n1
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n1
a, Sing n2 -> ContractPresence n2
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n2
b) of
    (ContractPresence n1
ContractPresent, ContractPresence n2
_) -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    (ContractPresence n1
_, ContractPresence n2
ContractPresent) -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    (ContractPresence n1
ContractAbsent, ContractPresence n2
ContractAbsent) -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STOr Sing n1
a Sing n2
b -> case (Sing n1 -> ContractPresence n1
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n1
a, Sing n2 -> ContractPresence n2
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n2
b) of
    (ContractPresence n1
ContractPresent, ContractPresence n2
_) -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    (ContractPresence n1
_, ContractPresence n2
ContractPresent) -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    (ContractPresence n1
ContractAbsent, ContractPresence n2
ContractAbsent) -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STLambda Sing n1
_ Sing n2
_ -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STMap Sing n1
_ Sing n2
v -> case Sing n2 -> ContractPresence n2
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n2
v of
    ContractPresence n2
ContractPresent -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    ContractPresence n2
ContractAbsent -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STBigMap Sing n1
_ Sing n2
v -> case Sing n2 -> ContractPresence n2
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n2
v of
    ContractPresence n2
ContractPresent -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    ContractPresence n2
ContractAbsent -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STInt -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STNat -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STString -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STBytes -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STMutez -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STBool -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STKeyHash -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STBls12381Fr -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STBls12381G1 -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STBls12381G2 -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STTimestamp -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STAddress -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STChest -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STChestKey -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STTxRollupL2Address -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  Sing ty
SingT ty
STNever -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STSaplingState Sing n
_ -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STSaplingTransaction Sing n
_ -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent

-- | Check at runtime whether a value of the given type _may_ contain a @ticket@ value.
checkTicketPresence :: Sing (ty :: T) -> TicketPresence ty
checkTicketPresence :: forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence = \case
  Sing ty
SingT ty
STKey -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STSignature -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STChainId -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STUnit -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  STOption Sing n
t -> case Sing n -> TicketPresence n
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing n
t of
    TicketPresence n
TicketPresent -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'True) => TicketPresence t
TicketPresent
    TicketPresence n
TicketAbsent -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  STList Sing n
t -> case Sing n -> TicketPresence n
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing n
t of
    TicketPresence n
TicketPresent -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'True) => TicketPresence t
TicketPresent
    TicketPresence n
TicketAbsent -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  STSet Sing n
_ -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STOperation -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  STContract Sing n
_ -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  STTicket Sing n
_ -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'True) => TicketPresence t
TicketPresent
  STPair Sing n1
a Sing n2
b -> case (Sing n1 -> TicketPresence n1
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing n1
a, Sing n2 -> TicketPresence n2
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing n2
b) of
    (TicketPresence n1
TicketPresent, TicketPresence n2
_) -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'True) => TicketPresence t
TicketPresent
    (TicketPresence n1
_, TicketPresence n2
TicketPresent) -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'True) => TicketPresence t
TicketPresent
    (TicketPresence n1
TicketAbsent, TicketPresence n2
TicketAbsent) -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  STOr Sing n1
a Sing n2
b -> case (Sing n1 -> TicketPresence n1
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing n1
a, Sing n2 -> TicketPresence n2
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing n2
b) of
    (TicketPresence n1
TicketPresent, TicketPresence n2
_) -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'True) => TicketPresence t
TicketPresent
    (TicketPresence n1
_, TicketPresence n2
TicketPresent) -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'True) => TicketPresence t
TicketPresent
    (TicketPresence n1
TicketAbsent, TicketPresence n2
TicketAbsent) -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  STLambda Sing n1
_ Sing n2
_ -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  STMap Sing n1
_ Sing n2
v -> case Sing n2 -> TicketPresence n2
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing n2
v of
    TicketPresence n2
TicketPresent -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'True) => TicketPresence t
TicketPresent
    TicketPresence n2
TicketAbsent -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  STBigMap Sing n1
_ Sing n2
v -> case Sing n2 -> TicketPresence n2
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing n2
v of
    TicketPresence n2
TicketPresent -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'True) => TicketPresence t
TicketPresent
    TicketPresence n2
TicketAbsent -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STInt -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STNat -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STString -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STBytes -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STMutez -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STBool -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STKeyHash -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STBls12381Fr -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STBls12381G1 -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STBls12381G2 -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STTimestamp -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STAddress -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STChest -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STChestKey -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STTxRollupL2Address -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  Sing ty
SingT ty
STNever -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  STSaplingState Sing n
_ -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
  STSaplingTransaction Sing n
_ -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent

-- | Check at runtime whether a value of the given type _may_ contain a @big_map@ value.
checkBigMapPresence :: Sing (ty :: T) -> BigMapPresence ty
checkBigMapPresence :: forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence = \case
  -- More boilerplate to boilerplate god.
  Sing ty
SingT ty
STKey -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STSignature -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STChainId -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STUnit -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STOption Sing n
t -> case Sing n -> BigMapPresence n
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing n
t of
    BigMapPresence n
BigMapPresent -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
    BigMapPresence n
BigMapAbsent -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STList Sing n
t -> case Sing n -> BigMapPresence n
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing n
t of
    BigMapPresence n
BigMapPresent -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
    BigMapPresence n
BigMapAbsent -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STSet Sing n
_ -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STOperation -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STContract Sing n
_ -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STTicket Sing n
_ -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent  -- big_maps are not allowed in tickets at all
  STPair Sing n1
a Sing n2
b -> case (Sing n1 -> BigMapPresence n1
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing n1
a, Sing n2 -> BigMapPresence n2
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing n2
b) of
    (BigMapPresence n1
BigMapPresent, BigMapPresence n2
_) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
    (BigMapPresence n1
_, BigMapPresence n2
BigMapPresent) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
    (BigMapPresence n1
BigMapAbsent, BigMapPresence n2
BigMapAbsent) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STOr Sing n1
a Sing n2
b -> case (Sing n1 -> BigMapPresence n1
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing n1
a, Sing n2 -> BigMapPresence n2
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing n2
b) of
    (BigMapPresence n1
BigMapPresent, BigMapPresence n2
_) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
    (BigMapPresence n1
_, BigMapPresence n2
BigMapPresent) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
    (BigMapPresence n1
BigMapAbsent, BigMapPresence n2
BigMapAbsent) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STLambda Sing n1
_ Sing n2
_ -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STMap Sing n1
_ Sing n2
v -> case Sing n2 -> BigMapPresence n2
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing n2
v of
    BigMapPresence n2
BigMapPresent -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
    BigMapPresence n2
BigMapAbsent -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STBigMap Sing n1
_ Sing n2
_ ->
    BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
  Sing ty
SingT ty
STInt -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STNat -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STString -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STBytes -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STMutez -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STBool -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STKeyHash -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STBls12381Fr -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STBls12381G1 -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STBls12381G2 -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STTimestamp -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STAddress -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STChest -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STChestKey -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STTxRollupL2Address -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  Sing ty
SingT ty
STNever -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STSaplingState Sing n
_ -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STSaplingTransaction Sing n
_ -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent

-- | Check at runtime whether a value of the given type _may_ contain nested @big_map@s.
checkNestedBigMapsPresence :: Sing (ty :: T) -> NestedBigMapsPresence ty
checkNestedBigMapsPresence :: forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence = \case
  -- More boilerplate to boilerplate god.
  Sing ty
SingT ty
STKey -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STSignature -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STChainId -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STUnit -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STOption Sing n
t -> case Sing n -> NestedBigMapsPresence n
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing n
t of
    NestedBigMapsPresence n
NestedBigMapsPresent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    NestedBigMapsPresence n
NestedBigMapsAbsent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STList                   Sing n
t -> case Sing n -> NestedBigMapsPresence n
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing n
t of
    NestedBigMapsPresence n
NestedBigMapsPresent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    NestedBigMapsPresence n
NestedBigMapsAbsent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STSet Sing n
_ -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STOperation -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STContract Sing n
_ -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STTicket Sing n
_ -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STPair Sing n1
a Sing n2
b -> case (Sing n1 -> NestedBigMapsPresence n1
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing n1
a, Sing n2 -> NestedBigMapsPresence n2
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing n2
b) of
    (NestedBigMapsPresence n1
NestedBigMapsPresent, NestedBigMapsPresence n2
_) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    (NestedBigMapsPresence n1
_, NestedBigMapsPresence n2
NestedBigMapsPresent) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    (NestedBigMapsPresence n1
NestedBigMapsAbsent, NestedBigMapsPresence n2
NestedBigMapsAbsent) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STOr Sing n1
a Sing n2
b -> case (Sing n1 -> NestedBigMapsPresence n1
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing n1
a, Sing n2 -> NestedBigMapsPresence n2
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing n2
b) of
    (NestedBigMapsPresence n1
NestedBigMapsPresent, NestedBigMapsPresence n2
_) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    (NestedBigMapsPresence n1
_, NestedBigMapsPresence n2
NestedBigMapsPresent) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    (NestedBigMapsPresence n1
NestedBigMapsAbsent, NestedBigMapsPresence n2
NestedBigMapsAbsent) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STLambda Sing n1
_ Sing n2
_ -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STMap Sing n1
_ Sing n2
v -> case Sing n2 -> NestedBigMapsPresence n2
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing n2
v of
    NestedBigMapsPresence n2
NestedBigMapsPresent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    NestedBigMapsPresence n2
NestedBigMapsAbsent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STBigMap Sing n1
_ Sing n2
v -> case Sing n2 -> BigMapPresence n2
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing n2
v of
    BigMapPresence n2
BigMapPresent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    BigMapPresence n2
BigMapAbsent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STInt -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STNat -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STString -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STBytes -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STMutez -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STBool -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STKeyHash -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STBls12381Fr -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STBls12381G1 -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STBls12381G2 -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STTimestamp -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STAddress -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STChest -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STChestKey -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STTxRollupL2Address -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  Sing ty
SingT ty
STNever -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STSaplingState Sing n
_ -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STSaplingTransaction Sing n
_ -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent


-- | Check at runtime whether a value of the given type _may_ contain a @sapling_state@ value.
checkSaplingStatePresence :: Sing (ty :: T) -> SaplingStatePresence ty
checkSaplingStatePresence :: forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence = \case
  Sing ty
SingT ty
STKey -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STSignature -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STChainId -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STUnit -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  STOption Sing n
t -> case Sing n -> SaplingStatePresence n
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence Sing n
t of
    SaplingStatePresence n
SaplingStatePresent -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'True) =>
SaplingStatePresence t
SaplingStatePresent
    SaplingStatePresence n
SaplingStateAbsent -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  STList Sing n
t -> case Sing n -> SaplingStatePresence n
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence Sing n
t of
    SaplingStatePresence n
SaplingStatePresent -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'True) =>
SaplingStatePresence t
SaplingStatePresent
    SaplingStatePresence n
SaplingStateAbsent -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  STSet Sing n
_ -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STOperation -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  STContract Sing n
_ -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  STTicket Sing n
_ -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  STPair Sing n1
a Sing n2
b -> case (Sing n1 -> SaplingStatePresence n1
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence Sing n1
a, Sing n2 -> SaplingStatePresence n2
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence Sing n2
b) of
    (SaplingStatePresence n1
SaplingStatePresent, SaplingStatePresence n2
_) -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'True) =>
SaplingStatePresence t
SaplingStatePresent
    (SaplingStatePresence n1
_, SaplingStatePresence n2
SaplingStatePresent) -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'True) =>
SaplingStatePresence t
SaplingStatePresent
    (SaplingStatePresence n1
SaplingStateAbsent, SaplingStatePresence n2
SaplingStateAbsent) -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  STOr Sing n1
a Sing n2
b -> case (Sing n1 -> SaplingStatePresence n1
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence Sing n1
a, Sing n2 -> SaplingStatePresence n2
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence Sing n2
b) of
    (SaplingStatePresence n1
SaplingStatePresent, SaplingStatePresence n2
_) -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'True) =>
SaplingStatePresence t
SaplingStatePresent
    (SaplingStatePresence n1
_, SaplingStatePresence n2
SaplingStatePresent) -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'True) =>
SaplingStatePresence t
SaplingStatePresent
    (SaplingStatePresence n1
SaplingStateAbsent, SaplingStatePresence n2
SaplingStateAbsent) -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  STLambda Sing n1
_ Sing n2
_ -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  STMap Sing n1
_ Sing n2
v -> case Sing n2 -> SaplingStatePresence n2
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence Sing n2
v of
    SaplingStatePresence n2
SaplingStatePresent -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'True) =>
SaplingStatePresence t
SaplingStatePresent
    SaplingStatePresence n2
SaplingStateAbsent -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  STBigMap Sing n1
_ Sing n2
v -> case Sing n2 -> SaplingStatePresence n2
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence Sing n2
v of
    SaplingStatePresence n2
SaplingStatePresent -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'True) =>
SaplingStatePresence t
SaplingStatePresent
    SaplingStatePresence n2
SaplingStateAbsent -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STInt -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STNat -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STString -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STBytes -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STMutez -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STBool -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STKeyHash -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STBls12381Fr -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STBls12381G1 -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STBls12381G2 -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STTimestamp -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STAddress -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STChest -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STChestKey -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STTxRollupL2Address -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  Sing ty
SingT ty
STNever -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
  STSaplingState Sing n
_ -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'True) =>
SaplingStatePresence t
SaplingStatePresent
  STSaplingTransaction Sing n
_ -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent

-- | Check at runtime that a value of the given type cannot contain operations.
opAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoOp t)
opAbsense :: forall (t :: T). Sing t -> Maybe (Dict $ HasNoOp t)
opAbsense Sing t
s = case Sing t -> OpPresence t
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing t
s of
  OpPresence t
OpPresent -> Maybe (Dict $ HasNoOp t)
forall a. Maybe a
Nothing
  OpPresence t
OpAbsent -> (Dict $ HasNoOp t) -> Maybe (Dict $ HasNoOp t)
forall a. a -> Maybe a
Just Dict $ HasNoOp t
forall (a :: Constraint). a => Dict a
Dict

-- | Check at runtime that a value of the given type cannot contain @contract@ values.
contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoContract t)
contractTypeAbsense :: forall (t :: T). Sing t -> Maybe (Dict $ HasNoContract t)
contractTypeAbsense Sing t
s = case Sing t -> ContractPresence t
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing t
s of
  ContractPresence t
ContractPresent -> Maybe (Dict $ HasNoContract t)
forall a. Maybe a
Nothing
  ContractPresence t
ContractAbsent -> (Dict $ HasNoContract t) -> Maybe (Dict $ HasNoContract t)
forall a. a -> Maybe a
Just Dict $ HasNoContract t
forall (a :: Constraint). a => Dict a
Dict

-- | Check at runtime that a value of the given type cannot contain @ticket@ values.
ticketAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoTicket t)
ticketAbsense :: forall (t :: T). Sing t -> Maybe (Dict $ HasNoTicket t)
ticketAbsense Sing t
s = case Sing t -> TicketPresence t
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing t
s of
  TicketPresence t
TicketPresent -> Maybe (Dict $ HasNoTicket t)
forall a. Maybe a
Nothing
  TicketPresence t
TicketAbsent -> (Dict $ HasNoTicket t) -> Maybe (Dict $ HasNoTicket t)
forall a. a -> Maybe a
Just Dict $ HasNoTicket t
forall (a :: Constraint). a => Dict a
Dict

-- | Check at runtime that a value of the given type cannot containt @big_map@ values
bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoBigMap t)
bigMapAbsense :: forall (t :: T). Sing t -> Maybe (Dict $ HasNoBigMap t)
bigMapAbsense Sing t
s = case Sing t -> BigMapPresence t
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing t
s of
  BigMapPresence t
BigMapPresent -> Maybe (Dict $ HasNoBigMap t)
forall a. Maybe a
Nothing
  BigMapPresence t
BigMapAbsent -> (Dict $ HasNoBigMap t) -> Maybe (Dict $ HasNoBigMap t)
forall a. a -> Maybe a
Just Dict $ HasNoBigMap t
forall (a :: Constraint). a => Dict a
Dict

-- | Check at runtime that a value of the given type cannot containt @sapling_state@ values
saplingStateAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoSaplingState t)
saplingStateAbsense :: forall (t :: T). Sing t -> Maybe (Dict $ HasNoSaplingState t)
saplingStateAbsense Sing t
s = case Sing t -> SaplingStatePresence t
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence Sing t
s of
  SaplingStatePresence t
SaplingStatePresent -> Maybe (Dict $ HasNoSaplingState t)
forall a. Maybe a
Nothing
  SaplingStatePresence t
SaplingStateAbsent -> (Dict $ HasNoSaplingState t) -> Maybe (Dict $ HasNoSaplingState t)
forall a. a -> Maybe a
Just Dict $ HasNoSaplingState t
forall (a :: Constraint). a => Dict a
Dict

-- | Check at runtime that a value of the given type cannot contain nested @big_map@s.
nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoNestedBigMaps t)
nestedBigMapsAbsense :: forall (t :: T). Sing t -> Maybe (Dict $ HasNoNestedBigMaps t)
nestedBigMapsAbsense Sing t
s = case Sing t -> NestedBigMapsPresence t
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing t
s of
  NestedBigMapsPresence t
NestedBigMapsPresent -> Maybe (Dict $ HasNoNestedBigMaps t)
forall a. Maybe a
Nothing
  NestedBigMapsPresence t
NestedBigMapsAbsent -> (Dict $ HasNoNestedBigMaps t)
-> Maybe (Dict $ HasNoNestedBigMaps t)
forall a. a -> Maybe a
Just Dict $ HasNoNestedBigMaps t
forall (a :: Constraint). a => Dict a
Dict

----------------------------------------------------------------------------
-- Scopes
----------------------------------------------------------------------------

data BadTypeForScope
  = BtNotComparable
  | BtIsOperation
  | BtHasBigMap
  | BtHasNestedBigMap
  | BtHasContract
  | BtHasTicket
  | BtHasSaplingState
  deriving stock (Int -> BadTypeForScope -> ShowS
[BadTypeForScope] -> ShowS
BadTypeForScope -> String
(Int -> BadTypeForScope -> ShowS)
-> (BadTypeForScope -> String)
-> ([BadTypeForScope] -> ShowS)
-> Show BadTypeForScope
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BadTypeForScope] -> ShowS
$cshowList :: [BadTypeForScope] -> ShowS
show :: BadTypeForScope -> String
$cshow :: BadTypeForScope -> String
showsPrec :: Int -> BadTypeForScope -> ShowS
$cshowsPrec :: Int -> BadTypeForScope -> ShowS
Show, BadTypeForScope -> BadTypeForScope -> Bool
(BadTypeForScope -> BadTypeForScope -> Bool)
-> (BadTypeForScope -> BadTypeForScope -> Bool)
-> Eq BadTypeForScope
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BadTypeForScope -> BadTypeForScope -> Bool
$c/= :: BadTypeForScope -> BadTypeForScope -> Bool
== :: BadTypeForScope -> BadTypeForScope -> Bool
$c== :: BadTypeForScope -> BadTypeForScope -> Bool
Eq, (forall x. BadTypeForScope -> Rep BadTypeForScope x)
-> (forall x. Rep BadTypeForScope x -> BadTypeForScope)
-> Generic BadTypeForScope
forall x. Rep BadTypeForScope x -> BadTypeForScope
forall x. BadTypeForScope -> Rep BadTypeForScope x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep BadTypeForScope x -> BadTypeForScope
$cfrom :: forall x. BadTypeForScope -> Rep BadTypeForScope x
Generic)
  deriving anyclass (BadTypeForScope -> ()
(BadTypeForScope -> ()) -> NFData BadTypeForScope
forall a. (a -> ()) -> NFData a
rnf :: BadTypeForScope -> ()
$crnf :: BadTypeForScope -> ()
NFData)

instance Buildable BadTypeForScope where
  build :: BadTypeForScope -> Builder
build = BadTypeForScope -> Builder
forall a. RenderDoc a => a -> Builder
buildRenderDoc

instance RenderDoc BadTypeForScope where
  renderDoc :: RenderContext -> BadTypeForScope -> Doc
renderDoc RenderContext
_ = \case
    BadTypeForScope
BtNotComparable -> Doc
"is not comparable"
    BadTypeForScope
BtIsOperation -> Doc
"has 'operation' type"
    BadTypeForScope
BtHasBigMap -> Doc
"has 'big_map'"
    BadTypeForScope
BtHasNestedBigMap -> Doc
"has nested 'big_map'"
    BadTypeForScope
BtHasContract -> Doc
"has 'contract' type"
    BadTypeForScope
BtHasTicket -> Doc
"has 'ticket' type"
    BadTypeForScope
BtHasSaplingState -> Doc
"has 'sapling_state' type"

-- | Set of constraints that Michelson applies to parameters.
--
-- Not just a type alias in order to be able to partially apply it
class (SingI t, WellTyped t, HasNoOp t, HasNoNestedBigMaps t) => ParameterScope t
instance (SingI t, WellTyped t, HasNoOp t, HasNoNestedBigMaps t) => ParameterScope t

-- | Set of constraints that Michelson applies to contract storage.
--
-- Not just a type alias in order to be able to partially apply it
class (SingI t, WellTyped t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) => StorageScope t
instance (SingI t, WellTyped t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) => StorageScope t

-- | Set of constraints that Michelson applies to pushed constants.
--
-- Not just a type alias in order to be able to partially apply it
class (SingI t, WellTyped t, HasNoOp t, HasNoBigMap t, HasNoContract t, HasNoTicket t, HasNoSaplingState t) => ConstantScope t
instance (SingI t, WellTyped t, HasNoOp t, HasNoBigMap t, HasNoContract t, HasNoTicket t, HasNoSaplingState t) => ConstantScope t

-- | Alias for constraints which Michelson requires in @DUP@ instruction.
class (SingI t, HasNoTicket t) => DupableScope t
instance (SingI t, HasNoTicket t) => DupableScope t

-- | Returns whether the type is dupable.
type family IsDupableScope (t :: T) :: Bool where
  IsDupableScope t = Not (ContainsTicket t)

-- | Set of constraints that Michelson applies to packed values.
--
-- Not just a type alias in order to be able to partially apply it
class (SingI t, WellTyped t, HasNoOp t, HasNoBigMap t, HasNoTicket t, HasNoSaplingState t) => PackedValScope t
instance (SingI t, WellTyped t, HasNoOp t, HasNoBigMap t, HasNoTicket t, HasNoSaplingState t ) => PackedValScope t

-- | Set of constraints that Michelson applies to unpacked values.
--
-- It is different from 'PackedValScope', e.g. @contract@ type cannot appear
-- in a value we unpack to.
--
-- Not just a type alias in order to be able to partially apply it
class (WellTyped t, PackedValScope t, ConstantScope t) => UnpackedValScope t
instance (WellTyped t, PackedValScope t, ConstantScope t) => UnpackedValScope t

-- | Set of constraints that Michelson applies to argument type and
-- return type of views.
-- All info related to views can be found in
-- [TZIP](https://gitlab.com/tezos/tzip/-/blob/master/drafts/current/draft_views.md).
--
-- Not just a type alias in order to be able to partially apply it
class (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => ViewableScope t
instance (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => ViewableScope t

-- | Alias for constraints which are required for untyped representation.
type UntypedValScope t = (SingI t, HasNoOp t)

----------------------------------------------------------------------------
-- Conveniences
----------------------------------------------------------------------------

-- | Should be present for common scopes.
class CheckScope (c :: Constraint) where
  -- | Check that constraint hold for a given type.
  checkScope :: Either BadTypeForScope (Dict c)

instance SingI t => CheckScope (WellTyped t) where
  checkScope :: Either BadTypeForScope (Dict (WellTyped t))
checkScope = (NotWellTyped -> BadTypeForScope)
-> Either NotWellTyped (Dict (WellTyped t))
-> Either BadTypeForScope (Dict (WellTyped t))
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first NotWellTyped -> BadTypeForScope
nwtCause (Either NotWellTyped (Dict (WellTyped t))
 -> Either BadTypeForScope (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
-> Either BadTypeForScope (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ forall (t :: T).
SingI t =>
Either NotWellTyped (Dict (WellTyped t))
getWTP @t
instance SingI t => CheckScope (HasNoOp t) where
  checkScope :: Either BadTypeForScope (Dict (HasNoOp t))
checkScope = BadTypeForScope
-> Maybe (Dict (HasNoOp t))
-> Either BadTypeForScope (Dict (HasNoOp t))
forall l r. l -> Maybe r -> Either l r
maybeToRight BadTypeForScope
BtIsOperation (Maybe (Dict (HasNoOp t))
 -> Either BadTypeForScope (Dict (HasNoOp t)))
-> Maybe (Dict (HasNoOp t))
-> Either BadTypeForScope (Dict (HasNoOp t))
forall a b. (a -> b) -> a -> b
$ Sing t -> Maybe (Dict (HasNoOp t))
forall (t :: T). Sing t -> Maybe (Dict $ HasNoOp t)
opAbsense Sing t
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI t => CheckScope (HasNoBigMap t) where
  checkScope :: Either BadTypeForScope (Dict (HasNoBigMap t))
checkScope = BadTypeForScope
-> Maybe (Dict (HasNoBigMap t))
-> Either BadTypeForScope (Dict (HasNoBigMap t))
forall l r. l -> Maybe r -> Either l r
maybeToRight BadTypeForScope
BtHasBigMap (Maybe (Dict (HasNoBigMap t))
 -> Either BadTypeForScope (Dict (HasNoBigMap t)))
-> Maybe (Dict (HasNoBigMap t))
-> Either BadTypeForScope (Dict (HasNoBigMap t))
forall a b. (a -> b) -> a -> b
$ Sing t -> Maybe (Dict (HasNoBigMap t))
forall (t :: T). Sing t -> Maybe (Dict $ HasNoBigMap t)
bigMapAbsense Sing t
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI t => CheckScope (HasNoNestedBigMaps t) where
  checkScope :: Either BadTypeForScope (Dict (HasNoNestedBigMaps t))
checkScope = BadTypeForScope
-> Maybe (Dict (HasNoNestedBigMaps t))
-> Either BadTypeForScope (Dict (HasNoNestedBigMaps t))
forall l r. l -> Maybe r -> Either l r
maybeToRight BadTypeForScope
BtHasNestedBigMap (Maybe (Dict (HasNoNestedBigMaps t))
 -> Either BadTypeForScope (Dict (HasNoNestedBigMaps t)))
-> Maybe (Dict (HasNoNestedBigMaps t))
-> Either BadTypeForScope (Dict (HasNoNestedBigMaps t))
forall a b. (a -> b) -> a -> b
$ Sing t -> Maybe (Dict (HasNoNestedBigMaps t))
forall (t :: T). Sing t -> Maybe (Dict $ HasNoNestedBigMaps t)
nestedBigMapsAbsense Sing t
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI t => CheckScope (HasNoContract t) where
  checkScope :: Either BadTypeForScope (Dict (HasNoContract t))
checkScope = BadTypeForScope
-> Maybe (Dict (HasNoContract t))
-> Either BadTypeForScope (Dict (HasNoContract t))
forall l r. l -> Maybe r -> Either l r
maybeToRight BadTypeForScope
BtHasContract (Maybe (Dict (HasNoContract t))
 -> Either BadTypeForScope (Dict (HasNoContract t)))
-> Maybe (Dict (HasNoContract t))
-> Either BadTypeForScope (Dict (HasNoContract t))
forall a b. (a -> b) -> a -> b
$ Sing t -> Maybe (Dict (HasNoContract t))
forall (t :: T). Sing t -> Maybe (Dict $ HasNoContract t)
contractTypeAbsense Sing t
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI t => CheckScope (HasNoTicket t) where
  checkScope :: Either BadTypeForScope (Dict (HasNoTicket t))
checkScope = BadTypeForScope
-> Maybe (Dict (HasNoTicket t))
-> Either BadTypeForScope (Dict (HasNoTicket t))
forall l r. l -> Maybe r -> Either l r
maybeToRight BadTypeForScope
BtHasTicket (Maybe (Dict (HasNoTicket t))
 -> Either BadTypeForScope (Dict (HasNoTicket t)))
-> Maybe (Dict (HasNoTicket t))
-> Either BadTypeForScope (Dict (HasNoTicket t))
forall a b. (a -> b) -> a -> b
$ Sing t -> Maybe (Dict (HasNoTicket t))
forall (t :: T). Sing t -> Maybe (Dict $ HasNoTicket t)
ticketAbsense Sing t
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI t => CheckScope (HasNoSaplingState t) where
  checkScope :: Either BadTypeForScope (Dict (HasNoSaplingState t))
checkScope = BadTypeForScope
-> Maybe (Dict (HasNoSaplingState t))
-> Either BadTypeForScope (Dict (HasNoSaplingState t))
forall l r. l -> Maybe r -> Either l r
maybeToRight BadTypeForScope
BtHasSaplingState (Maybe (Dict (HasNoSaplingState t))
 -> Either BadTypeForScope (Dict (HasNoSaplingState t)))
-> Maybe (Dict (HasNoSaplingState t))
-> Either BadTypeForScope (Dict (HasNoSaplingState t))
forall a b. (a -> b) -> a -> b
$ Sing t -> Maybe (Dict (HasNoSaplingState t))
forall (t :: T). Sing t -> Maybe (Dict $ HasNoSaplingState t)
saplingStateAbsense Sing t
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI t => CheckScope (Comparable t) where
  checkScope :: Either BadTypeForScope (Dict (Comparable t))
checkScope = BadTypeForScope
-> Maybe (Dict (Comparable t))
-> Either BadTypeForScope (Dict (Comparable t))
forall l r. l -> Maybe r -> Either l r
maybeToRight BadTypeForScope
BtNotComparable (Maybe (Dict (Comparable t))
 -> Either BadTypeForScope (Dict (Comparable t)))
-> Maybe (Dict (Comparable t))
-> Either BadTypeForScope (Dict (Comparable t))
forall a b. (a -> b) -> a -> b
$ Sing t -> Maybe (Dict (Comparable t))
forall (t :: T). Sing t -> Maybe (Dict (Comparable t))
comparabilityPresence Sing t
forall {k} (a :: k). SingI a => Sing a
sing

-- | Alias for comparable types.
type ComparabilityScope t =
  (SingI t, Comparable t)

comparabilityPresence :: Sing t -> Maybe (Dict (Comparable t))
comparabilityPresence :: forall (t :: T). Sing t -> Maybe (Dict (Comparable t))
comparabilityPresence Sing t
s = case Sing t -> Comparability t
forall (t :: T). Sing t -> Comparability t
checkComparability Sing t
s of
  Comparability t
CanBeCompared -> Dict (Comparable t) -> Maybe (Dict (Comparable t))
forall a. a -> Maybe a
Just Dict (Comparable t)
forall (a :: Constraint). a => Dict a
Dict
  Comparability t
CannotBeCompared -> Maybe (Dict (Comparable t))
forall a. Maybe a
Nothing

instance SingI t => CheckScope (ParameterScope t) where
  checkScope :: Either BadTypeForScope (Dict (ParameterScope t))
checkScope =
    (\Dict (WellTyped t)
Dict Dict (HasNoOp t)
Dict Dict (HasNoNestedBigMaps t)
Dict -> Dict (ParameterScope t)
forall (a :: Constraint). a => Dict a
Dict)
      (Dict (WellTyped t)
 -> Dict (HasNoOp t)
 -> Dict (HasNoNestedBigMaps t)
 -> Dict (ParameterScope t))
-> Either BadTypeForScope (Dict (WellTyped t))
-> Either
     BadTypeForScope
     (Dict (HasNoOp t)
      -> Dict (HasNoNestedBigMaps t) -> Dict (ParameterScope t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(WellTyped t)
      Either
  BadTypeForScope
  (Dict (HasNoOp t)
   -> Dict (HasNoNestedBigMaps t) -> Dict (ParameterScope t))
-> Either BadTypeForScope (Dict (HasNoOp t))
-> Either
     BadTypeForScope
     (Dict (HasNoNestedBigMaps t) -> Dict (ParameterScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoOp t)
      Either
  BadTypeForScope
  (Dict (HasNoNestedBigMaps t) -> Dict (ParameterScope t))
-> Either BadTypeForScope (Dict (HasNoNestedBigMaps t))
-> Either BadTypeForScope (Dict (ParameterScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoNestedBigMaps t)

instance SingI t => CheckScope (StorageScope t) where
  checkScope :: Either BadTypeForScope (Dict (StorageScope t))
checkScope =
    (\Dict (WellTyped t)
Dict Dict (HasNoOp t)
Dict Dict (HasNoNestedBigMaps t)
Dict Dict (HasNoContract t)
Dict -> Dict (StorageScope t)
forall (a :: Constraint). a => Dict a
Dict)
      (Dict (WellTyped t)
 -> Dict (HasNoOp t)
 -> Dict (HasNoNestedBigMaps t)
 -> Dict (HasNoContract t)
 -> Dict (StorageScope t))
-> Either BadTypeForScope (Dict (WellTyped t))
-> Either
     BadTypeForScope
     (Dict (HasNoOp t)
      -> Dict (HasNoNestedBigMaps t)
      -> Dict (HasNoContract t)
      -> Dict (StorageScope t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(WellTyped t)
      Either
  BadTypeForScope
  (Dict (HasNoOp t)
   -> Dict (HasNoNestedBigMaps t)
   -> Dict (HasNoContract t)
   -> Dict (StorageScope t))
-> Either BadTypeForScope (Dict (HasNoOp t))
-> Either
     BadTypeForScope
     (Dict (HasNoNestedBigMaps t)
      -> Dict (HasNoContract t) -> Dict (StorageScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoOp t)
      Either
  BadTypeForScope
  (Dict (HasNoNestedBigMaps t)
   -> Dict (HasNoContract t) -> Dict (StorageScope t))
-> Either BadTypeForScope (Dict (HasNoNestedBigMaps t))
-> Either
     BadTypeForScope (Dict (HasNoContract t) -> Dict (StorageScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoNestedBigMaps t)
      Either
  BadTypeForScope (Dict (HasNoContract t) -> Dict (StorageScope t))
-> Either BadTypeForScope (Dict (HasNoContract t))
-> Either BadTypeForScope (Dict (StorageScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoContract t)

instance SingI t => CheckScope (ConstantScope t) where
  checkScope :: Either BadTypeForScope (Dict (ConstantScope t))
checkScope =
    (\Dict (WellTyped t)
Dict Dict (HasNoOp t)
Dict Dict (HasNoBigMap t)
Dict Dict (HasNoContract t)
Dict Dict (HasNoTicket t)
Dict Dict (HasNoSaplingState t)
Dict -> Dict (ConstantScope t)
forall (a :: Constraint). a => Dict a
Dict)
      (Dict (WellTyped t)
 -> Dict (HasNoOp t)
 -> Dict (HasNoBigMap t)
 -> Dict (HasNoContract t)
 -> Dict (HasNoTicket t)
 -> Dict (HasNoSaplingState t)
 -> Dict (ConstantScope t))
-> Either BadTypeForScope (Dict (WellTyped t))
-> Either
     BadTypeForScope
     (Dict (HasNoOp t)
      -> Dict (HasNoBigMap t)
      -> Dict (HasNoContract t)
      -> Dict (HasNoTicket t)
      -> Dict (HasNoSaplingState t)
      -> Dict (ConstantScope t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(WellTyped t)
      Either
  BadTypeForScope
  (Dict (HasNoOp t)
   -> Dict (HasNoBigMap t)
   -> Dict (HasNoContract t)
   -> Dict (HasNoTicket t)
   -> Dict (HasNoSaplingState t)
   -> Dict (ConstantScope t))
-> Either BadTypeForScope (Dict (HasNoOp t))
-> Either
     BadTypeForScope
     (Dict (HasNoBigMap t)
      -> Dict (HasNoContract t)
      -> Dict (HasNoTicket t)
      -> Dict (HasNoSaplingState t)
      -> Dict (ConstantScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoOp t)
      Either
  BadTypeForScope
  (Dict (HasNoBigMap t)
   -> Dict (HasNoContract t)
   -> Dict (HasNoTicket t)
   -> Dict (HasNoSaplingState t)
   -> Dict (ConstantScope t))
-> Either BadTypeForScope (Dict (HasNoBigMap t))
-> Either
     BadTypeForScope
     (Dict (HasNoContract t)
      -> Dict (HasNoTicket t)
      -> Dict (HasNoSaplingState t)
      -> Dict (ConstantScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoBigMap t)
      Either
  BadTypeForScope
  (Dict (HasNoContract t)
   -> Dict (HasNoTicket t)
   -> Dict (HasNoSaplingState t)
   -> Dict (ConstantScope t))
-> Either BadTypeForScope (Dict (HasNoContract t))
-> Either
     BadTypeForScope
     (Dict (HasNoTicket t)
      -> Dict (HasNoSaplingState t) -> Dict (ConstantScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoContract t)
      Either
  BadTypeForScope
  (Dict (HasNoTicket t)
   -> Dict (HasNoSaplingState t) -> Dict (ConstantScope t))
-> Either BadTypeForScope (Dict (HasNoTicket t))
-> Either
     BadTypeForScope
     (Dict (HasNoSaplingState t) -> Dict (ConstantScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoTicket t)
      Either
  BadTypeForScope
  (Dict (HasNoSaplingState t) -> Dict (ConstantScope t))
-> Either BadTypeForScope (Dict (HasNoSaplingState t))
-> Either BadTypeForScope (Dict (ConstantScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoSaplingState t)

instance SingI t => CheckScope (DupableScope t) where
  checkScope :: Either BadTypeForScope (Dict (DupableScope t))
checkScope =
    (\Dict (HasNoTicket t)
Dict -> Dict (DupableScope t)
forall (a :: Constraint). a => Dict a
Dict)
      (Dict (HasNoTicket t) -> Dict (DupableScope t))
-> Either BadTypeForScope (Dict (HasNoTicket t))
-> Either BadTypeForScope (Dict (DupableScope t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoTicket t)

instance SingI t => CheckScope (PackedValScope t) where
  checkScope :: Either BadTypeForScope (Dict (PackedValScope t))
checkScope =
    (\Dict (WellTyped t)
Dict Dict (HasNoOp t)
Dict Dict (HasNoBigMap t)
Dict Dict (HasNoTicket t)
Dict Dict (HasNoSaplingState t)
Dict -> Dict (PackedValScope t)
forall (a :: Constraint). a => Dict a
Dict)
      (Dict (WellTyped t)
 -> Dict (HasNoOp t)
 -> Dict (HasNoBigMap t)
 -> Dict (HasNoTicket t)
 -> Dict (HasNoSaplingState t)
 -> Dict (PackedValScope t))
-> Either BadTypeForScope (Dict (WellTyped t))
-> Either
     BadTypeForScope
     (Dict (HasNoOp t)
      -> Dict (HasNoBigMap t)
      -> Dict (HasNoTicket t)
      -> Dict (HasNoSaplingState t)
      -> Dict (PackedValScope t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(WellTyped t)
      Either
  BadTypeForScope
  (Dict (HasNoOp t)
   -> Dict (HasNoBigMap t)
   -> Dict (HasNoTicket t)
   -> Dict (HasNoSaplingState t)
   -> Dict (PackedValScope t))
-> Either BadTypeForScope (Dict (HasNoOp t))
-> Either
     BadTypeForScope
     (Dict (HasNoBigMap t)
      -> Dict (HasNoTicket t)
      -> Dict (HasNoSaplingState t)
      -> Dict (PackedValScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoOp t)
      Either
  BadTypeForScope
  (Dict (HasNoBigMap t)
   -> Dict (HasNoTicket t)
   -> Dict (HasNoSaplingState t)
   -> Dict (PackedValScope t))
-> Either BadTypeForScope (Dict (HasNoBigMap t))
-> Either
     BadTypeForScope
     (Dict (HasNoTicket t)
      -> Dict (HasNoSaplingState t) -> Dict (PackedValScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoBigMap t)
      Either
  BadTypeForScope
  (Dict (HasNoTicket t)
   -> Dict (HasNoSaplingState t) -> Dict (PackedValScope t))
-> Either BadTypeForScope (Dict (HasNoTicket t))
-> Either
     BadTypeForScope
     (Dict (HasNoSaplingState t) -> Dict (PackedValScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoTicket t)
      Either
  BadTypeForScope
  (Dict (HasNoSaplingState t) -> Dict (PackedValScope t))
-> Either BadTypeForScope (Dict (HasNoSaplingState t))
-> Either BadTypeForScope (Dict (PackedValScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoSaplingState t)

instance SingI t => CheckScope (UnpackedValScope t) where
  checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t))
checkScope =
    (\Dict (WellTyped t)
Dict Dict (PackedValScope t)
Dict Dict (ConstantScope t)
Dict -> Dict (UnpackedValScope t)
forall (a :: Constraint). a => Dict a
Dict)
      (Dict (WellTyped t)
 -> Dict (PackedValScope t)
 -> Dict (ConstantScope t)
 -> Dict (UnpackedValScope t))
-> Either BadTypeForScope (Dict (WellTyped t))
-> Either
     BadTypeForScope
     (Dict (PackedValScope t)
      -> Dict (ConstantScope t) -> Dict (UnpackedValScope t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(WellTyped t)
      Either
  BadTypeForScope
  (Dict (PackedValScope t)
   -> Dict (ConstantScope t) -> Dict (UnpackedValScope t))
-> Either BadTypeForScope (Dict (PackedValScope t))
-> Either
     BadTypeForScope
     (Dict (ConstantScope t) -> Dict (UnpackedValScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(PackedValScope t)
      Either
  BadTypeForScope
  (Dict (ConstantScope t) -> Dict (UnpackedValScope t))
-> Either BadTypeForScope (Dict (ConstantScope t))
-> Either BadTypeForScope (Dict (UnpackedValScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope t)

instance SingI t => CheckScope (ViewableScope t) where
  checkScope :: Either BadTypeForScope (Dict (ViewableScope t))
checkScope =
    (\Dict (HasNoOp t)
Dict Dict (HasNoBigMap t)
Dict Dict (HasNoTicket t)
Dict -> Dict (ViewableScope t)
forall (a :: Constraint). a => Dict a
Dict)
      (Dict (HasNoOp t)
 -> Dict (HasNoBigMap t)
 -> Dict (HasNoTicket t)
 -> Dict (ViewableScope t))
-> Either BadTypeForScope (Dict (HasNoOp t))
-> Either
     BadTypeForScope
     (Dict (HasNoBigMap t)
      -> Dict (HasNoTicket t) -> Dict (ViewableScope t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoOp t)
      Either
  BadTypeForScope
  (Dict (HasNoBigMap t)
   -> Dict (HasNoTicket t) -> Dict (ViewableScope t))
-> Either BadTypeForScope (Dict (HasNoBigMap t))
-> Either
     BadTypeForScope (Dict (HasNoTicket t) -> Dict (ViewableScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoBigMap t)
      Either
  BadTypeForScope (Dict (HasNoTicket t) -> Dict (ViewableScope t))
-> Either BadTypeForScope (Dict (HasNoTicket t))
-> Either BadTypeForScope (Dict (ViewableScope t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(HasNoTicket t)

instance SingI t => CheckScope (ComparabilityScope t) where
  checkScope :: Either BadTypeForScope (Dict (ComparabilityScope t))
checkScope =
    (\Dict (Comparable t)
Dict -> Dict (ComparabilityScope t)
forall (a :: Constraint). a => Dict a
Dict) (Dict (Comparable t) -> Dict (ComparabilityScope t))
-> Either BadTypeForScope (Dict (Comparable t))
-> Either BadTypeForScope (Dict (ComparabilityScope t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(Comparable t)

-- | Allows using a scope that can be proven true with a De Morgan law.
--
-- Many scopes are defined as @not a@ (or rather @a ~ 'False@) where @a@ is a
-- negative property we want to avoid as a 'Constraint'.
-- The negative constraints are implemented with a type family that for some
-- combination types resolves to itself applied to the type arguments in an @or@,
-- e.g. A @pair l r@ has @x@ if @l@ or @r@ contain @x@.
--
-- Because of the De Morgan laws @not (a or b)@ implies @(not a) and (not b)@
-- or in our case: @pair@ does not contain @x@ -> @a@ and @b@ don't contain @x@.
class WithDeMorganScope (c :: T -> Constraint) t a b where
  withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret

-- | Produce evidence that the first argument of a disjunction
-- is false if the whole disjunction is false.
orL :: forall a b. (a || b) ~ 'False => Sing a -> a :~: 'False
orL :: forall (a :: Bool) (b :: Bool).
((a || b) ~ 'False) =>
Sing a -> a :~: 'False
orL Sing a
SBool a
SFalse = a :~: 'False
forall {k} (a :: k). a :~: a
Refl
{-# NOINLINE [1] orL #-}

-- This rule is *slightly* illegitimate, because the right hand side is lazier
-- than the left hand side. In context, this is fine, and we really *want* to
-- do it so we have at least some hope of avoiding building singletons that we
-- don't end up using. We'd get a totally legitimate rule if we used a SingI
-- constraint instead of a Sing argument, but then we'd need to use withSingI,
-- which for some reason doesn't use the newfangled GHC machinery for such and
-- therefore risks gumming up optimization. Of course, we could roll our own
-- withSingI, but that's very hairy and GHC version dependent (the
-- never-really-documented magicDict was recently replaced by withDict, which
-- is documented in ... the type checker source code, apparently).
{-# RULES
"orL" forall s. orL s = unsafeCoerce Refl
 #-}

-- | When a class looks like
--
-- @
-- class (SomeTypeFamily t ~ 'False, ...) => TheClass t
-- instance (SomeTypeFamily t ~ 'False, ...) => TheClass t
-- @
--
-- and the additional constraints are satisfied by the instance constraints of
-- the 'WithDeMorganScope' instance for @TheClass@, we can use
-- `simpleWithDeMorgan` to define 'withDeMorganScope' for the instance.
simpleWithDeMorgan
  :: forall sym a b ret.
     ((sym @@ a || sym @@ b) ~ 'False, SingI sym, SingI a)
  => (((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
-- Note: If the "orL" rule fires (which it should), we won't actually calculate
-- the (likely recursive) `sing @sym @@ sing @a` at all. If we're lucky, GHC
-- might not build the `SingI a` dictionary either.
simpleWithDeMorgan :: forall {k1} (sym :: k1 ~> Bool) (a :: k1) (b :: k1) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
simpleWithDeMorgan ((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret
f
  | (sym @@ a) :~: 'False
Refl <- forall (a :: Bool) (b :: Bool).
((a || b) ~ 'False) =>
Sing a -> a :~: 'False
orL @(sym @@ a) @(sym @@ b) (forall {k} (a :: k). SingI a => Sing a
forall (a :: k1 ~> Bool). SingI a => Sing a
sing @sym Sing sym -> Sing a -> Sing (sym @@ a)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ forall (a :: k1). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @a)
  = ret
((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret
f

data ContainsOpSym :: T ~> Bool
type instance Apply ContainsOpSym x = ContainsOp x
instance SingI ContainsOpSym where
  sing :: Sing ContainsOpSym
sing = (forall (t :: T). Sing t -> Sing (ContainsOpSym @@ t))
-> SLambda ContainsOpSym
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda ((forall (t :: T). Sing t -> Sing (ContainsOpSym @@ t))
 -> SLambda ContainsOpSym)
-> (forall (t :: T). Sing t -> Sing (ContainsOpSym @@ t))
-> SLambda ContainsOpSym
forall a b. (a -> b) -> a -> b
$ \Sing t
t -> case Sing t -> OpPresence t
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing t
t of
    OpPresence t
OpPresent -> Sing (ContainsOpSym @@ t)
SBool 'True
STrue
    OpPresence t
OpAbsent -> Sing (ContainsOpSym @@ t)
SBool 'False
SFalse
instance SingI a => WithDeMorganScope HasNoOp 'TPair a b where
  withDeMorganScope :: forall ret.
HasNoOp ('TPair a b) =>
((HasNoOp a, HasNoOp b) => ret) -> ret
withDeMorganScope (HasNoOp a, HasNoOp b) => ret
f = forall {k1} (sym :: k1 ~> Bool) (a :: k1) (b :: k1) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
forall (sym :: TyFun T Bool -> *) (a :: T) (b :: T) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
simpleWithDeMorgan @ContainsOpSym @a @b ((ContainsOpSym @@ a) ~ 'False, (ContainsOpSym @@ b) ~ 'False) =>
ret
(HasNoOp a, HasNoOp b) => ret
f
instance SingI a => WithDeMorganScope HasNoOp 'TOr a b where
  withDeMorganScope :: forall ret.
HasNoOp ('TOr a b) =>
((HasNoOp a, HasNoOp b) => ret) -> ret
withDeMorganScope (HasNoOp a, HasNoOp b) => ret
f = forall {k1} (sym :: k1 ~> Bool) (a :: k1) (b :: k1) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
forall (sym :: TyFun T Bool -> *) (a :: T) (b :: T) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
simpleWithDeMorgan @ContainsOpSym @a @b ((ContainsOpSym @@ a) ~ 'False, (ContainsOpSym @@ b) ~ 'False) =>
ret
(HasNoOp a, HasNoOp b) => ret
f
instance SingI k => WithDeMorganScope HasNoOp 'TMap k v where
  withDeMorganScope :: forall ret.
HasNoOp ('TMap k v) =>
((HasNoOp k, HasNoOp v) => ret) -> ret
withDeMorganScope (HasNoOp k, HasNoOp v) => ret
f = forall {k1} (sym :: k1 ~> Bool) (a :: k1) (b :: k1) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
forall (sym :: TyFun T Bool -> *) (a :: T) (b :: T) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
simpleWithDeMorgan @ContainsOpSym @k @v ((ContainsOpSym @@ k) ~ 'False, (ContainsOpSym @@ v) ~ 'False) =>
ret
(HasNoOp k, HasNoOp v) => ret
f
instance SingI k => WithDeMorganScope HasNoOp 'TBigMap k v where
  withDeMorganScope :: forall ret.
HasNoOp ('TBigMap k v) =>
((HasNoOp k, HasNoOp v) => ret) -> ret
withDeMorganScope (HasNoOp k, HasNoOp v) => ret
f = forall {k1} (sym :: k1 ~> Bool) (a :: k1) (b :: k1) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
forall (sym :: TyFun T Bool -> *) (a :: T) (b :: T) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
simpleWithDeMorgan @ContainsOpSym @k @v ((ContainsOpSym @@ k) ~ 'False, (ContainsOpSym @@ v) ~ 'False) =>
ret
(HasNoOp k, HasNoOp v) => ret
f

data ContainsContractSym :: T ~> Bool
type instance Apply ContainsContractSym x = ContainsContract x
instance SingI ContainsContractSym where
  sing :: Sing ContainsContractSym
sing = (forall (t :: T). Sing t -> Sing (ContainsContractSym @@ t))
-> SLambda ContainsContractSym
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda ((forall (t :: T). Sing t -> Sing (ContainsContractSym @@ t))
 -> SLambda ContainsContractSym)
-> (forall (t :: T). Sing t -> Sing (ContainsContractSym @@ t))
-> SLambda ContainsContractSym
forall a b. (a -> b) -> a -> b
$ \Sing t
t -> case Sing t -> ContractPresence t
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing t
t of
    ContractPresence t
ContractPresent -> Sing (ContainsContractSym @@ t)
SBool 'True
STrue
    ContractPresence t
ContractAbsent -> Sing (ContainsContractSym @@ t)
SBool 'False
SFalse
instance SingI a => WithDeMorganScope HasNoContract 'TPair a b where
  withDeMorganScope :: forall ret.
HasNoContract ('TPair a b) =>
((HasNoContract a, HasNoContract b) => ret) -> ret
withDeMorganScope (HasNoContract a, HasNoContract b) => ret
f = forall {k1} (sym :: k1 ~> Bool) (a :: k1) (b :: k1) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
forall (sym :: TyFun T Bool -> *) (a :: T) (b :: T) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
simpleWithDeMorgan @ContainsContractSym @a @b ((ContainsContractSym @@ a) ~ 'False,
 (ContainsContractSym @@ b) ~ 'False) =>
ret
(HasNoContract a, HasNoContract b) => ret
f
instance SingI a => WithDeMorganScope HasNoContract 'TOr a b where
  withDeMorganScope :: forall ret.
HasNoContract ('TOr a b) =>
((HasNoContract a, HasNoContract b) => ret) -> ret
withDeMorganScope (HasNoContract a, HasNoContract b) => ret
f = forall {k1} (sym :: k1 ~> Bool) (a :: k1) (b :: k1) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
forall (sym :: TyFun T Bool -> *) (a :: T) (b :: T) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
simpleWithDeMorgan @ContainsContractSym @a @b ((ContainsContractSym @@ a) ~ 'False,
 (ContainsContractSym @@ b) ~ 'False) =>
ret
(HasNoContract a, HasNoContract b) => ret
f

data ContainsTicketSym :: T ~> Bool
type instance Apply ContainsTicketSym x = ContainsTicket x
instance SingI ContainsTicketSym where
  sing :: Sing ContainsTicketSym
sing = (forall (t :: T). Sing t -> Sing (ContainsTicketSym @@ t))
-> SLambda ContainsTicketSym
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda ((forall (t :: T). Sing t -> Sing (ContainsTicketSym @@ t))
 -> SLambda ContainsTicketSym)
-> (forall (t :: T). Sing t -> Sing (ContainsTicketSym @@ t))
-> SLambda ContainsTicketSym
forall a b. (a -> b) -> a -> b
$ \Sing t
t -> case Sing t -> TicketPresence t
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing t
t of
    TicketPresence t
TicketPresent -> Sing (ContainsTicketSym @@ t)
SBool 'True
STrue
    TicketPresence t
TicketAbsent -> Sing (ContainsTicketSym @@ t)
SBool 'False
SFalse
instance SingI a => WithDeMorganScope HasNoTicket 'TPair a b where
  withDeMorganScope :: forall ret.
HasNoTicket ('TPair a b) =>
((HasNoTicket a, HasNoTicket b) => ret) -> ret
withDeMorganScope (HasNoTicket a, HasNoTicket b) => ret
f = forall {k1} (sym :: k1 ~> Bool) (a :: k1) (b :: k1) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
forall (sym :: TyFun T Bool -> *) (a :: T) (b :: T) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
simpleWithDeMorgan @ContainsTicketSym @a @b ((ContainsTicketSym @@ a) ~ 'False,
 (ContainsTicketSym @@ b) ~ 'False) =>
ret
(HasNoTicket a, HasNoTicket b) => ret
f
instance SingI a => WithDeMorganScope HasNoTicket 'TOr a b where
  withDeMorganScope :: forall ret.
HasNoTicket ('TOr a b) =>
((HasNoTicket a, HasNoTicket b) => ret) -> ret
withDeMorganScope (HasNoTicket a, HasNoTicket b) => ret
f = forall {k1} (sym :: k1 ~> Bool) (a :: k1) (b :: k1) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
forall (sym :: TyFun T Bool -> *) (a :: T) (b :: T) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
simpleWithDeMorgan @ContainsTicketSym @a @b ((ContainsTicketSym @@ a) ~ 'False,
 (ContainsTicketSym @@ b) ~ 'False) =>
ret
(HasNoTicket a, HasNoTicket b) => ret
f

data ContainsBigMapSym :: T ~> Bool
type instance Apply ContainsBigMapSym x = ContainsBigMap x
instance SingI ContainsBigMapSym where
  sing :: Sing ContainsBigMapSym
sing = (forall (t :: T). Sing t -> Sing (ContainsBigMapSym @@ t))
-> SLambda ContainsBigMapSym
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda ((forall (t :: T). Sing t -> Sing (ContainsBigMapSym @@ t))
 -> SLambda ContainsBigMapSym)
-> (forall (t :: T). Sing t -> Sing (ContainsBigMapSym @@ t))
-> SLambda ContainsBigMapSym
forall a b. (a -> b) -> a -> b
$ \Sing t
t -> case Sing t -> BigMapPresence t
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing t
t of
    BigMapPresence t
BigMapPresent -> Sing (ContainsBigMapSym @@ t)
SBool 'True
STrue
    BigMapPresence t
BigMapAbsent -> Sing (ContainsBigMapSym @@ t)
SBool 'False
SFalse
instance SingI a => WithDeMorganScope HasNoBigMap 'TPair a b where
  withDeMorganScope :: forall ret.
HasNoBigMap ('TPair a b) =>
((HasNoBigMap a, HasNoBigMap b) => ret) -> ret
withDeMorganScope (HasNoBigMap a, HasNoBigMap b) => ret
f = forall {k1} (sym :: k1 ~> Bool) (a :: k1) (b :: k1) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
forall (sym :: TyFun T Bool -> *) (a :: T) (b :: T) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
simpleWithDeMorgan @ContainsBigMapSym @a @b ((ContainsBigMapSym @@ a) ~ 'False,
 (ContainsBigMapSym @@ b) ~ 'False) =>
ret
(HasNoBigMap a, HasNoBigMap b) => ret
f
instance SingI a => WithDeMorganScope HasNoBigMap 'TOr a b where
  withDeMorganScope :: forall ret.
HasNoBigMap ('TOr a b) =>
((HasNoBigMap a, HasNoBigMap b) => ret) -> ret
withDeMorganScope (HasNoBigMap a, HasNoBigMap b) => ret
f = forall {k1} (sym :: k1 ~> Bool) (a :: k1) (b :: k1) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
forall (sym :: TyFun T Bool -> *) (a :: T) (b :: T) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
simpleWithDeMorgan @ContainsBigMapSym @a @b ((ContainsBigMapSym @@ a) ~ 'False,
 (ContainsBigMapSym @@ b) ~ 'False) =>
ret
(HasNoBigMap a, HasNoBigMap b) => ret
f

data ContainsNestedBigMapsSym :: T ~> Bool
type instance Apply ContainsNestedBigMapsSym x = ContainsNestedBigMaps x
instance SingI ContainsNestedBigMapsSym where
  sing :: Sing ContainsNestedBigMapsSym
sing = (forall (t :: T). Sing t -> Sing (ContainsNestedBigMapsSym @@ t))
-> SLambda ContainsNestedBigMapsSym
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda ((forall (t :: T). Sing t -> Sing (ContainsNestedBigMapsSym @@ t))
 -> SLambda ContainsNestedBigMapsSym)
-> (forall (t :: T).
    Sing t -> Sing (ContainsNestedBigMapsSym @@ t))
-> SLambda ContainsNestedBigMapsSym
forall a b. (a -> b) -> a -> b
$ \Sing t
t -> case Sing t -> NestedBigMapsPresence t
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing t
t of
    NestedBigMapsPresence t
NestedBigMapsPresent -> Sing (ContainsNestedBigMapsSym @@ t)
SBool 'True
STrue
    NestedBigMapsPresence t
NestedBigMapsAbsent -> Sing (ContainsNestedBigMapsSym @@ t)
SBool 'False
SFalse
instance SingI a => WithDeMorganScope HasNoNestedBigMaps 'TPair a b where
  withDeMorganScope :: forall ret.
HasNoNestedBigMaps ('TPair a b) =>
((HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret) -> ret
withDeMorganScope (HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret
f = forall {k1} (sym :: k1 ~> Bool) (a :: k1) (b :: k1) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
forall (sym :: TyFun T Bool -> *) (a :: T) (b :: T) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
simpleWithDeMorgan @ContainsNestedBigMapsSym @a @b ((ContainsNestedBigMapsSym @@ a) ~ 'False,
 (ContainsNestedBigMapsSym @@ b) ~ 'False) =>
ret
(HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret
f
instance SingI a => WithDeMorganScope HasNoNestedBigMaps 'TOr a b where
  withDeMorganScope :: forall ret.
HasNoNestedBigMaps ('TOr a b) =>
((HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret) -> ret
withDeMorganScope (HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret
f = forall {k1} (sym :: k1 ~> Bool) (a :: k1) (b :: k1) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
forall (sym :: TyFun T Bool -> *) (a :: T) (b :: T) ret.
(((sym @@ a) || (sym @@ b)) ~ 'False, SingI sym, SingI a) =>
(((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
simpleWithDeMorgan @ContainsNestedBigMapsSym @a @b ((ContainsNestedBigMapsSym @@ a) ~ 'False,
 (ContainsNestedBigMapsSym @@ b) ~ 'False) =>
ret
(HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret
f



instance
  ( WithDeMorganScope HasNoOp t a b
  , WithDeMorganScope HasNoNestedBigMaps t a b
  , WellTyped a, WellTyped b
  ) => WithDeMorganScope ParameterScope t a b where
  withDeMorganScope :: forall ret.
ParameterScope (t a b) =>
((ParameterScope a, ParameterScope b) => ret) -> ret
withDeMorganScope (ParameterScope a, ParameterScope b) => ret
f =
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @HasNoOp @t @a @b (((HasNoOp a, HasNoOp b) => ret) -> ret)
-> ((HasNoOp a, HasNoOp b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @HasNoNestedBigMaps @t @a @b (ParameterScope a, ParameterScope b) => ret
(HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret
f

instance
  ( WithDeMorganScope HasNoOp t a b
  , WithDeMorganScope HasNoNestedBigMaps t a b
  , WithDeMorganScope HasNoContract t a b
  , WellTyped a, WellTyped b
  ) => WithDeMorganScope StorageScope t a b where
  withDeMorganScope :: forall ret.
StorageScope (t a b) =>
((StorageScope a, StorageScope b) => ret) -> ret
withDeMorganScope (StorageScope a, StorageScope b) => ret
f =
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @HasNoOp @t @a @b (((HasNoOp a, HasNoOp b) => ret) -> ret)
-> ((HasNoOp a, HasNoOp b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @HasNoNestedBigMaps @t @a @b (((HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret) -> ret)
-> ((HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @HasNoContract @t @a @b (StorageScope a, StorageScope b) => ret
(HasNoContract a, HasNoContract b) => ret
f

instance
  ( WithDeMorganScope HasNoOp t a b
  , WithDeMorganScope HasNoBigMap t a b
  , WithDeMorganScope HasNoContract t a b
  , WithDeMorganScope HasNoTicket t a b
  , WithDeMorganScope HasNoSaplingState t a b
  , WellTyped a, WellTyped b
  ) => WithDeMorganScope ConstantScope t a b where
  withDeMorganScope :: forall ret.
ConstantScope (t a b) =>
((ConstantScope a, ConstantScope b) => ret) -> ret
withDeMorganScope (ConstantScope a, ConstantScope b) => ret
f =
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @HasNoOp @t @a @b (((HasNoOp a, HasNoOp b) => ret) -> ret)
-> ((HasNoOp a, HasNoOp b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @HasNoBigMap @t @a @b (((HasNoBigMap a, HasNoBigMap b) => ret) -> ret)
-> ((HasNoBigMap a, HasNoBigMap b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @HasNoContract @t @a @b (((HasNoContract a, HasNoContract b) => ret) -> ret)
-> ((HasNoContract a, HasNoContract b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @HasNoTicket @t @a @b (((HasNoTicket a, HasNoTicket b) => ret) -> ret)
-> ((HasNoTicket a, HasNoTicket b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @HasNoSaplingState @t @a @b (ConstantScope a, ConstantScope b) => ret
(HasNoSaplingState a, HasNoSaplingState b) => ret
f

instance
  ( WithDeMorganScope HasNoOp t a b
  , WithDeMorganScope HasNoBigMap t a b
  , WithDeMorganScope HasNoTicket t a b
  , WithDeMorganScope HasNoSaplingState t a b
  , WellTyped a, WellTyped b
  ) => WithDeMorganScope PackedValScope t a b where
  withDeMorganScope :: forall ret.
PackedValScope (t a b) =>
((PackedValScope a, PackedValScope b) => ret) -> ret
withDeMorganScope (PackedValScope a, PackedValScope b) => ret
f =
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @HasNoOp @t @a @b (((HasNoOp a, HasNoOp b) => ret) -> ret)
-> ((HasNoOp a, HasNoOp b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @HasNoBigMap @t @a @b (((HasNoBigMap a, HasNoBigMap b) => ret) -> ret)
-> ((HasNoBigMap a, HasNoBigMap b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @HasNoTicket @t @a @b (((HasNoTicket a, HasNoTicket b) => ret) -> ret)
-> ((HasNoTicket a, HasNoTicket b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @HasNoSaplingState @t @a @b (PackedValScope a, PackedValScope b) => ret
(HasNoSaplingState a, HasNoSaplingState b) => ret
f

instance
  ( WithDeMorganScope PackedValScope t a b
  , WithDeMorganScope ConstantScope t a b
  , WellTyped a, WellTyped b
  ) => WithDeMorganScope UnpackedValScope t a b where
  withDeMorganScope :: forall ret.
UnpackedValScope (t a b) =>
((UnpackedValScope a, UnpackedValScope b) => ret) -> ret
withDeMorganScope (UnpackedValScope a, UnpackedValScope b) => ret
f =
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @PackedValScope @t @a @b (((PackedValScope a, PackedValScope b) => ret) -> ret)
-> ((PackedValScope a, PackedValScope b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ConstantScope @t @a @b (UnpackedValScope a, UnpackedValScope b) => ret
(ConstantScope a, ConstantScope b) => ret
f

-- Versions for eDSL
----------------------------------------------------------------------------

{- These constraints are supposed to be used only in eDSL code and eDSL should
define its own wrapers over it.
-}

type ProperParameterBetterErrors t =
  (SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t)

type ProperStorageBetterErrors t =
  (SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t)

type ProperConstantBetterErrors t =
  (SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidContract t, ForbidTicket t, ForbidSaplingState t)

type ProperDupableBetterErrors t =
  (SingI t, ForbidTicket t)

type ProperPackedValBetterErrors t =
  (SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidTicket t, ForbidSaplingState t)

type ProperUnpackedValBetterErrors t =
  (ProperPackedValBetterErrors t, ProperConstantBetterErrors t)

type ProperViewableBetterErrors t =
  (SingI t, ForbidOp t, ForbidBigMap t, ForbidTicket t)

type ProperUntypedValBetterErrors t =
  (SingI t, ForbidOp t)

type ProperNonComparableValBetterErrors t =
  (SingI t, ForbidNonComparable t)

{-# DEPRECATED properParameterEvi, properStorageEvi, properConstantEvi
 , properDupableEvi, properPackedValEvi, properUnpackedValEvi
 , properViewableEvi, properUntypedValEvi
 "This entailment is now trivial; there is no need to introduce evidence for it."
 #-}
properParameterEvi :: forall t. ProperParameterBetterErrors t :- ParameterScope t
properParameterEvi :: forall (t :: T). ProperParameterBetterErrors t :- ParameterScope t
properParameterEvi = ((SingI t, WellTyped t,
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsOp t) 'False))
     ('Text "Operations are not allowed in this scope")
     (() :: Constraint),
   ContainsOp t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsNestedBigMaps t) 'False))
     ('Text "Nested BigMaps are not allowed")
     (() :: Constraint),
   ContainsNestedBigMaps t ~ 'False)) =>
 Dict (ParameterScope t))
-> (SingI t, WellTyped t,
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsOp t) 'False))
       ('Text "Operations are not allowed in this scope")
       (() :: Constraint),
     ContainsOp t ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsNestedBigMaps t) 'False))
       ('Text "Nested BigMaps are not allowed")
       (() :: Constraint),
     ContainsNestedBigMaps t ~ 'False))
   :- ParameterScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (SingI t, WellTyped t,
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsOp t) 'False))
    ('Text "Operations are not allowed in this scope")
    (() :: Constraint),
  ContainsOp t ~ 'False),
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsNestedBigMaps t) 'False))
    ('Text "Nested BigMaps are not allowed")
    (() :: Constraint),
  ContainsNestedBigMaps t ~ 'False)) =>
Dict (ParameterScope t)
forall (a :: Constraint). a => Dict a
Dict

properStorageEvi :: forall t. ProperStorageBetterErrors t :- StorageScope t
properStorageEvi :: forall (t :: T). ProperStorageBetterErrors t :- StorageScope t
properStorageEvi = ((SingI t, WellTyped t,
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsOp t) 'False))
     ('Text "Operations are not allowed in this scope")
     (() :: Constraint),
   ContainsOp t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsNestedBigMaps t) 'False))
     ('Text "Nested BigMaps are not allowed")
     (() :: Constraint),
   ContainsNestedBigMaps t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsContract t) 'False))
     ('Text "Type `contract` is not allowed in this scope")
     (() :: Constraint),
   ContainsContract t ~ 'False)) =>
 Dict (StorageScope t))
-> (SingI t, WellTyped t,
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsOp t) 'False))
       ('Text "Operations are not allowed in this scope")
       (() :: Constraint),
     ContainsOp t ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsNestedBigMaps t) 'False))
       ('Text "Nested BigMaps are not allowed")
       (() :: Constraint),
     ContainsNestedBigMaps t ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsContract t) 'False))
       ('Text "Type `contract` is not allowed in this scope")
       (() :: Constraint),
     ContainsContract t ~ 'False))
   :- StorageScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (SingI t, WellTyped t,
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsOp t) 'False))
    ('Text "Operations are not allowed in this scope")
    (() :: Constraint),
  ContainsOp t ~ 'False),
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsNestedBigMaps t) 'False))
    ('Text "Nested BigMaps are not allowed")
    (() :: Constraint),
  ContainsNestedBigMaps t ~ 'False),
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsContract t) 'False))
    ('Text "Type `contract` is not allowed in this scope")
    (() :: Constraint),
  ContainsContract t ~ 'False)) =>
Dict (StorageScope t)
forall (a :: Constraint). a => Dict a
Dict

properConstantEvi :: forall t. ProperConstantBetterErrors t :- ConstantScope t
properConstantEvi :: forall (t :: T). ProperConstantBetterErrors t :- ConstantScope t
properConstantEvi = ((SingI t, WellTyped t,
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsOp t) 'False))
     ('Text "Operations are not allowed in this scope")
     (() :: Constraint),
   ContainsOp t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsBigMap t) 'False))
     ('Text "BigMaps are not allowed in this scope")
     (() :: Constraint),
   ContainsBigMap t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsContract t) 'False))
     ('Text "Type `contract` is not allowed in this scope")
     (() :: Constraint),
   ContainsContract t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsTicket t) 'False))
     ('Text "Type `ticket` is not allowed in this scope")
     (() :: Constraint),
   ContainsTicket t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsSaplingState t) 'False))
     ('Text "Type `sapling_state` is not allowed in this scope")
     (() :: Constraint),
   ContainsSaplingState t ~ 'False)) =>
 Dict (ConstantScope t))
-> (SingI t, WellTyped t,
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsOp t) 'False))
       ('Text "Operations are not allowed in this scope")
       (() :: Constraint),
     ContainsOp t ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsBigMap t) 'False))
       ('Text "BigMaps are not allowed in this scope")
       (() :: Constraint),
     ContainsBigMap t ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsContract t) 'False))
       ('Text "Type `contract` is not allowed in this scope")
       (() :: Constraint),
     ContainsContract t ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsTicket t) 'False))
       ('Text "Type `ticket` is not allowed in this scope")
       (() :: Constraint),
     ContainsTicket t ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsSaplingState t) 'False))
       ('Text "Type `sapling_state` is not allowed in this scope")
       (() :: Constraint),
     ContainsSaplingState t ~ 'False))
   :- ConstantScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (SingI t, WellTyped t,
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsOp t) 'False))
    ('Text "Operations are not allowed in this scope")
    (() :: Constraint),
  ContainsOp t ~ 'False),
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsBigMap t) 'False))
    ('Text "BigMaps are not allowed in this scope")
    (() :: Constraint),
  ContainsBigMap t ~ 'False),
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsContract t) 'False))
    ('Text "Type `contract` is not allowed in this scope")
    (() :: Constraint),
  ContainsContract t ~ 'False),
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsTicket t) 'False))
    ('Text "Type `ticket` is not allowed in this scope")
    (() :: Constraint),
  ContainsTicket t ~ 'False),
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsSaplingState t) 'False))
    ('Text "Type `sapling_state` is not allowed in this scope")
    (() :: Constraint),
  ContainsSaplingState t ~ 'False)) =>
Dict (ConstantScope t)
forall (a :: Constraint). a => Dict a
Dict

properDupableEvi :: forall t. ProperDupableBetterErrors t :- DupableScope t
properDupableEvi :: forall (t :: T). ProperDupableBetterErrors t :- DupableScope t
properDupableEvi = ((SingI t,
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsTicket t) 'False))
     ('Text "Type `ticket` is not allowed in this scope")
     (() :: Constraint),
   ContainsTicket t ~ 'False)) =>
 Dict (DupableScope t))
-> (SingI t,
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsTicket t) 'False))
       ('Text "Type `ticket` is not allowed in this scope")
       (() :: Constraint),
     ContainsTicket t ~ 'False))
   :- DupableScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (SingI t,
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsTicket t) 'False))
    ('Text "Type `ticket` is not allowed in this scope")
    (() :: Constraint),
  ContainsTicket t ~ 'False)) =>
Dict (DupableScope t)
forall (a :: Constraint). a => Dict a
Dict

properPackedValEvi :: forall t. ProperPackedValBetterErrors t :- PackedValScope t
properPackedValEvi :: forall (t :: T). ProperPackedValBetterErrors t :- PackedValScope t
properPackedValEvi = ((SingI t, WellTyped t,
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsOp t) 'False))
     ('Text "Operations are not allowed in this scope")
     (() :: Constraint),
   ContainsOp t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsBigMap t) 'False))
     ('Text "BigMaps are not allowed in this scope")
     (() :: Constraint),
   ContainsBigMap t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsTicket t) 'False))
     ('Text "Type `ticket` is not allowed in this scope")
     (() :: Constraint),
   ContainsTicket t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsSaplingState t) 'False))
     ('Text "Type `sapling_state` is not allowed in this scope")
     (() :: Constraint),
   ContainsSaplingState t ~ 'False)) =>
 Dict (PackedValScope t))
-> (SingI t, WellTyped t,
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsOp t) 'False))
       ('Text "Operations are not allowed in this scope")
       (() :: Constraint),
     ContainsOp t ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsBigMap t) 'False))
       ('Text "BigMaps are not allowed in this scope")
       (() :: Constraint),
     ContainsBigMap t ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsTicket t) 'False))
       ('Text "Type `ticket` is not allowed in this scope")
       (() :: Constraint),
     ContainsTicket t ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsSaplingState t) 'False))
       ('Text "Type `sapling_state` is not allowed in this scope")
       (() :: Constraint),
     ContainsSaplingState t ~ 'False))
   :- PackedValScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (SingI t, WellTyped t,
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsOp t) 'False))
    ('Text "Operations are not allowed in this scope")
    (() :: Constraint),
  ContainsOp t ~ 'False),
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsBigMap t) 'False))
    ('Text "BigMaps are not allowed in this scope")
    (() :: Constraint),
  ContainsBigMap t ~ 'False),
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsTicket t) 'False))
    ('Text "Type `ticket` is not allowed in this scope")
    (() :: Constraint),
  ContainsTicket t ~ 'False),
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsSaplingState t) 'False))
    ('Text "Type `sapling_state` is not allowed in this scope")
    (() :: Constraint),
  ContainsSaplingState t ~ 'False)) =>
Dict (PackedValScope t)
forall (a :: Constraint). a => Dict a
Dict

properUnpackedValEvi :: forall t. ProperUnpackedValBetterErrors t :- UnpackedValScope t
properUnpackedValEvi :: forall (t :: T).
ProperUnpackedValBetterErrors t :- UnpackedValScope t
properUnpackedValEvi = (((SingI t, WellTyped t,
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsOp t) 'False))
      ('Text "Operations are not allowed in this scope")
      (() :: Constraint),
    ContainsOp t ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsBigMap t) 'False))
      ('Text "BigMaps are not allowed in this scope")
      (() :: Constraint),
    ContainsBigMap t ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsTicket t) 'False))
      ('Text "Type `ticket` is not allowed in this scope")
      (() :: Constraint),
    ContainsTicket t ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsSaplingState t) 'False))
      ('Text "Type `sapling_state` is not allowed in this scope")
      (() :: Constraint),
    ContainsSaplingState t ~ 'False)),
  (SingI t, WellTyped t,
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsOp t) 'False))
      ('Text "Operations are not allowed in this scope")
      (() :: Constraint),
    ContainsOp t ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsBigMap t) 'False))
      ('Text "BigMaps are not allowed in this scope")
      (() :: Constraint),
    ContainsBigMap t ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsContract t) 'False))
      ('Text "Type `contract` is not allowed in this scope")
      (() :: Constraint),
    ContainsContract t ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsTicket t) 'False))
      ('Text "Type `ticket` is not allowed in this scope")
      (() :: Constraint),
    ContainsTicket t ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsSaplingState t) 'False))
      ('Text "Type `sapling_state` is not allowed in this scope")
      (() :: Constraint),
    ContainsSaplingState t ~ 'False))) =>
 Dict (UnpackedValScope t))
-> ((SingI t, WellTyped t,
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsOp t) 'False))
        ('Text "Operations are not allowed in this scope")
        (() :: Constraint),
      ContainsOp t ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsBigMap t) 'False))
        ('Text "BigMaps are not allowed in this scope")
        (() :: Constraint),
      ContainsBigMap t ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsTicket t) 'False))
        ('Text "Type `ticket` is not allowed in this scope")
        (() :: Constraint),
      ContainsTicket t ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsSaplingState t) 'False))
        ('Text "Type `sapling_state` is not allowed in this scope")
        (() :: Constraint),
      ContainsSaplingState t ~ 'False)),
    (SingI t, WellTyped t,
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsOp t) 'False))
        ('Text "Operations are not allowed in this scope")
        (() :: Constraint),
      ContainsOp t ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsBigMap t) 'False))
        ('Text "BigMaps are not allowed in this scope")
        (() :: Constraint),
      ContainsBigMap t ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsContract t) 'False))
        ('Text "Type `contract` is not allowed in this scope")
        (() :: Constraint),
      ContainsContract t ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsTicket t) 'False))
        ('Text "Type `ticket` is not allowed in this scope")
        (() :: Constraint),
      ContainsTicket t ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsSaplingState t) 'False))
        ('Text "Type `sapling_state` is not allowed in this scope")
        (() :: Constraint),
      ContainsSaplingState t ~ 'False)))
   :- UnpackedValScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((SingI t, WellTyped t,
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsOp t) 'False))
     ('Text "Operations are not allowed in this scope")
     (() :: Constraint),
   ContainsOp t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsBigMap t) 'False))
     ('Text "BigMaps are not allowed in this scope")
     (() :: Constraint),
   ContainsBigMap t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsTicket t) 'False))
     ('Text "Type `ticket` is not allowed in this scope")
     (() :: Constraint),
   ContainsTicket t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsSaplingState t) 'False))
     ('Text "Type `sapling_state` is not allowed in this scope")
     (() :: Constraint),
   ContainsSaplingState t ~ 'False)),
 (SingI t, WellTyped t,
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsOp t) 'False))
     ('Text "Operations are not allowed in this scope")
     (() :: Constraint),
   ContainsOp t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsBigMap t) 'False))
     ('Text "BigMaps are not allowed in this scope")
     (() :: Constraint),
   ContainsBigMap t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsContract t) 'False))
     ('Text "Type `contract` is not allowed in this scope")
     (() :: Constraint),
   ContainsContract t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsTicket t) 'False))
     ('Text "Type `ticket` is not allowed in this scope")
     (() :: Constraint),
   ContainsTicket t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsSaplingState t) 'False))
     ('Text "Type `sapling_state` is not allowed in this scope")
     (() :: Constraint),
   ContainsSaplingState t ~ 'False))) =>
Dict (UnpackedValScope t)
forall (a :: Constraint). a => Dict a
Dict

properViewableEvi :: forall t. ProperViewableBetterErrors t :- ViewableScope t
properViewableEvi :: forall (t :: T). ProperViewableBetterErrors t :- ViewableScope t
properViewableEvi = ((SingI t,
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsOp t) 'False))
     ('Text "Operations are not allowed in this scope")
     (() :: Constraint),
   ContainsOp t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsBigMap t) 'False))
     ('Text "BigMaps are not allowed in this scope")
     (() :: Constraint),
   ContainsBigMap t ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsTicket t) 'False))
     ('Text "Type `ticket` is not allowed in this scope")
     (() :: Constraint),
   ContainsTicket t ~ 'False)) =>
 Dict (ViewableScope t))
-> (SingI t,
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsOp t) 'False))
       ('Text "Operations are not allowed in this scope")
       (() :: Constraint),
     ContainsOp t ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsBigMap t) 'False))
       ('Text "BigMaps are not allowed in this scope")
       (() :: Constraint),
     ContainsBigMap t ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsTicket t) 'False))
       ('Text "Type `ticket` is not allowed in this scope")
       (() :: Constraint),
     ContainsTicket t ~ 'False))
   :- ViewableScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (SingI t,
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsOp t) 'False))
    ('Text "Operations are not allowed in this scope")
    (() :: Constraint),
  ContainsOp t ~ 'False),
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsBigMap t) 'False))
    ('Text "BigMaps are not allowed in this scope")
    (() :: Constraint),
  ContainsBigMap t ~ 'False),
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsTicket t) 'False))
    ('Text "Type `ticket` is not allowed in this scope")
    (() :: Constraint),
  ContainsTicket t ~ 'False)) =>
Dict (ViewableScope t)
forall (a :: Constraint). a => Dict a
Dict

properUntypedValEvi :: forall t. ProperUntypedValBetterErrors t :- UntypedValScope t
properUntypedValEvi :: forall (t :: T).
ProperUntypedValBetterErrors t :- UntypedValScope t
properUntypedValEvi = ((SingI t,
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsOp t) 'False))
     ('Text "Operations are not allowed in this scope")
     (() :: Constraint),
   ContainsOp t ~ 'False)) =>
 Dict (UntypedValScope t))
-> (SingI t,
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsOp t) 'False))
       ('Text "Operations are not allowed in this scope")
       (() :: Constraint),
     ContainsOp t ~ 'False))
   :- UntypedValScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (SingI t,
 (FailWhenElsePoly
    (Not (DefaultEq (ContainsOp t) 'False))
    ('Text "Operations are not allowed in this scope")
    (() :: Constraint),
  ContainsOp t ~ 'False)) =>
Dict (UntypedValScope t)
forall (a :: Constraint). a => Dict a
Dict

class (IsComparable t ~ 'True, SingI t, ComparableSuperC t) => Comparable t where
  -- | Constraints required for instance of a given type.
  type ComparableSuperC t :: Constraint
  type ComparableSuperC _ = ()

instance ComparableSuperC ('TPair t1 t2) => Comparable ('TPair t1 t2) where
  type ComparableSuperC ('TPair t1 t2) =
    (Comparable t1, Comparable t2, FailOnNonComparableFound (IsComparable t1 && IsComparable t2))

instance ComparableSuperC ('TOr t1 t2) => Comparable ('TOr t1 t2) where
  type ComparableSuperC ('TOr t1 t2) =
    (Comparable t1, Comparable t2, FailOnNonComparableFound (IsComparable t1 && IsComparable t2))

instance ComparableSuperC ('TOption t) => Comparable ('TOption t) where
  type ComparableSuperC ('TOption t) = (Comparable t, ForbidNonComparable t)

instance Comparable 'TUnit
instance Comparable 'TInt
instance Comparable 'TNat
instance Comparable 'TString
instance Comparable 'TBytes
instance Comparable 'TMutez
instance Comparable 'TBool
instance Comparable 'TKeyHash
instance Comparable 'TTimestamp
instance Comparable 'TAddress
instance Comparable 'TTxRollupL2Address
instance Comparable 'TNever
instance Comparable 'TChainId
instance Comparable 'TSignature
instance Comparable 'TKey

-- | This class encodes Michelson rules w.r.t where it requires comparable
-- types. Earlier we had a dedicated type for representing comparable types @CT@.
-- But then we integreated those types into @T@. This meant that some of the
-- types that could be formed with various combinations of @T@ would be
-- illegal as per Michelson typing rule. Using this class, we inductively
-- enforce that a type and all types it contains are well typed as per
-- Michelson's rules.
class (SingI t, WellTypedSuperC t) => WellTyped (t :: T) where
  -- | Constraints required for instance of a given type.
  type WellTypedSuperC t :: Constraint
  type WellTypedSuperC _ = ()

instance WellTyped 'TKey
instance WellTyped 'TUnit
instance WellTyped 'TNever
instance WellTyped 'TSignature
instance WellTyped 'TChainId
instance WellTyped 'TChest
instance WellTyped 'TChestKey
instance WellTyped 'TTxRollupL2Address

instance WellTypedSuperC ('TOption t) => WellTyped ('TOption t) where
  type WellTypedSuperC ('TOption t) = WellTyped t

instance WellTypedSuperC ('TList t) => WellTyped ('TList t) where
  type WellTypedSuperC ('TList t) = WellTyped t

instance WellTypedSuperC ('TSet t) => WellTyped ('TSet t) where
  type WellTypedSuperC ('TSet t) = (Comparable t, WellTyped t)

instance WellTyped 'TOperation

instance WellTypedSuperC ('TContract t) => WellTyped ('TContract t) where
  type WellTypedSuperC ('TContract t) = (WellTyped t, HasNoOp t, HasNoNestedBigMaps t)

instance WellTypedSuperC ('TTicket t) => WellTyped ('TTicket t) where
  type WellTypedSuperC ('TTicket t) = (WellTyped t, Comparable t)

instance WellTypedSuperC ('TPair t1 t2) => WellTyped ('TPair t1 t2) where
  type WellTypedSuperC ('TPair t1 t2) = (WellTyped t1, WellTyped t2)

instance WellTypedSuperC ('TOr t1 t2) => WellTyped ('TOr t1 t2) where
  type WellTypedSuperC ('TOr t1 t2) = (WellTyped t1, WellTyped t2)

instance WellTypedSuperC ('TLambda t1 t2) => WellTyped ('TLambda t1 t2) where
  type WellTypedSuperC ('TLambda t1 t2) = (WellTyped t1, WellTyped t2)

instance WellTypedSuperC ('TMap k v) => WellTyped ('TMap k v) where
  type WellTypedSuperC ('TMap k v) = (Comparable k, WellTyped k, WellTyped v)

instance WellTypedSuperC ('TBigMap k v) => WellTyped ('TBigMap k v) where
  type WellTypedSuperC ('TBigMap k v) = ( Comparable k, WellTyped k, WellTyped v
                                        , HasNoBigMap v, HasNoOp v)

instance WellTyped 'TInt
instance WellTyped 'TNat
instance WellTyped 'TString
instance WellTyped 'TBytes
instance WellTyped 'TMutez
instance WellTyped 'TBool
instance WellTyped 'TKeyHash
instance WellTyped 'TBls12381Fr
instance WellTyped 'TBls12381G1
instance WellTyped 'TBls12381G2
instance WellTyped 'TTimestamp
instance WellTyped 'TAddress

instance (SingI n) => WellTyped ('TSaplingState n) where
  type WellTypedSuperC ('TSaplingState n) = (SingI n)

instance (SingI n) => WellTyped ('TSaplingTransaction n) where
  type WellTypedSuperC ('TSaplingTransaction n) = (SingI n)

-- | Error type for when a value is not well-typed.
data NotWellTyped = NotWellTyped
  { NotWellTyped -> T
nwtBadType :: T
  , NotWellTyped -> BadTypeForScope
nwtCause :: BadTypeForScope
  }

instance Buildable NotWellTyped where
  build :: NotWellTyped -> Builder
build (NotWellTyped T
t BadTypeForScope
c) =
    Builder
"Given type is not well typed because '" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> (T -> Builder
forall p. Buildable p => p -> Builder
build T
t) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"' " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> (BadTypeForScope -> Builder
forall p. Buildable p => p -> Builder
build BadTypeForScope
c)

data Comparability t where
  CanBeCompared :: (Comparable t) => Comparability t
  CannotBeCompared :: (IsComparable t ~ 'False) => Comparability t

-- | Given a type, provide evidence that it is well typed w.r.t to the
--  Michelson rules regarding where comparable types are required.
getWTP :: forall t. (SingI t) => Either NotWellTyped (Dict (WellTyped t))
getWTP :: forall (t :: T).
SingI t =>
Either NotWellTyped (Dict (WellTyped t))
getWTP = Sing t -> Either NotWellTyped (Dict (WellTyped t))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing t
forall {k} (a :: k). SingI a => Sing a
sing

-- | Version of 'getWTP' that accepts 'Sing' at term-level.
getWTP' :: Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' :: forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' = \case
  Sing t
SingT t
STKey -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STUnit -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STSignature -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STChainId -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  STOption Sing n
s -> do
    Dict (WellTyped n)
Dict <- Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n
s
    Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  STList Sing n
s -> do
    Dict (WellTyped n)
Dict <- Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n
s
    Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  STSet Sing n
s -> do
    Dict (WellTyped n)
Dict <- Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n
s
    Dict (Comparable n)
Dict <- BadTypeForScope
-> (Sing n -> Maybe (Dict (Comparable n)))
-> Sing n
-> Either NotWellTyped (Dict (Comparable n))
forall (ty :: T) a.
BadTypeForScope
-> (Sing ty -> Maybe a) -> Sing ty -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtNotComparable Sing n -> Maybe (Dict (Comparable n))
forall (t :: T). Sing t -> Maybe (Dict (Comparable t))
getComparableProofS Sing n
s
    Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STOperation -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  STContract Sing n
s -> do
    Dict (WellTyped n)
Dict <- Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n
s
    Dict (HasNoOp n)
Dict <- BadTypeForScope
-> (Sing n -> Maybe (Dict (HasNoOp n)))
-> Sing n
-> Either NotWellTyped (Dict (HasNoOp n))
forall (ty :: T) a.
BadTypeForScope
-> (Sing ty -> Maybe a) -> Sing ty -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtIsOperation Sing n -> Maybe (Dict (HasNoOp n))
forall (t :: T). Sing t -> Maybe (Dict $ HasNoOp t)
opAbsense Sing n
s
    Dict (HasNoNestedBigMaps n)
Dict <- BadTypeForScope
-> (Sing n -> Maybe (Dict (HasNoNestedBigMaps n)))
-> Sing n
-> Either NotWellTyped (Dict (HasNoNestedBigMaps n))
forall (ty :: T) a.
BadTypeForScope
-> (Sing ty -> Maybe a) -> Sing ty -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtHasNestedBigMap Sing n -> Maybe (Dict (HasNoNestedBigMaps n))
forall (t :: T). Sing t -> Maybe (Dict $ HasNoNestedBigMaps t)
nestedBigMapsAbsense Sing n
s
    Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  STTicket Sing n
s -> do
    Dict (WellTyped n)
Dict <- Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n
s
    Dict (Comparable n)
Dict <- BadTypeForScope
-> (Sing n -> Maybe (Dict (Comparable n)))
-> Sing n
-> Either NotWellTyped (Dict (Comparable n))
forall (ty :: T) a.
BadTypeForScope
-> (Sing ty -> Maybe a) -> Sing ty -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtNotComparable Sing n -> Maybe (Dict (Comparable n))
forall (t :: T). Sing t -> Maybe (Dict (Comparable t))
getComparableProofS Sing n
s
    Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  STPair Sing n1
s1 Sing n2
s2 -> do
    Dict (WellTyped n1)
Dict <- Sing n1 -> Either NotWellTyped (Dict (WellTyped n1))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n1
s1
    Dict (WellTyped n2)
Dict <- Sing n2 -> Either NotWellTyped (Dict (WellTyped n2))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n2
s2
    Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  STOr Sing n1
s1 Sing n2
s2 -> do
    Dict (WellTyped n1)
Dict <- Sing n1 -> Either NotWellTyped (Dict (WellTyped n1))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n1
s1
    Dict (WellTyped n2)
Dict <- Sing n2 -> Either NotWellTyped (Dict (WellTyped n2))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n2
s2
    Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  STLambda Sing n1
s1 Sing n2
s2 -> do
    Dict (WellTyped n1)
Dict <- Sing n1 -> Either NotWellTyped (Dict (WellTyped n1))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n1
s1
    Dict (WellTyped n2)
Dict <- Sing n2 -> Either NotWellTyped (Dict (WellTyped n2))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n2
s2
    Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  STMap Sing n1
s1 Sing n2
s2 -> do
    Dict (WellTyped n1)
Dict <- Sing n1 -> Either NotWellTyped (Dict (WellTyped n1))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n1
s1
    Dict (WellTyped n2)
Dict <- Sing n2 -> Either NotWellTyped (Dict (WellTyped n2))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n2
s2
    Dict (Comparable n1)
Dict <- BadTypeForScope
-> (Sing n1 -> Maybe (Dict (Comparable n1)))
-> Sing n1
-> Either NotWellTyped (Dict (Comparable n1))
forall (ty :: T) a.
BadTypeForScope
-> (Sing ty -> Maybe a) -> Sing ty -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtNotComparable Sing n1 -> Maybe (Dict (Comparable n1))
forall (t :: T). Sing t -> Maybe (Dict (Comparable t))
getComparableProofS Sing n1
s1
    Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  STBigMap Sing n1
s1 Sing n2
s2 -> do
    Dict (WellTyped n1)
Dict <- Sing n1 -> Either NotWellTyped (Dict (WellTyped n1))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n1
s1
    Dict (WellTyped n2)
Dict <- Sing n2 -> Either NotWellTyped (Dict (WellTyped n2))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n2
s2
    Dict (Comparable n1)
Dict <- BadTypeForScope
-> (Sing n1 -> Maybe (Dict (Comparable n1)))
-> Sing n1
-> Either NotWellTyped (Dict (Comparable n1))
forall (ty :: T) a.
BadTypeForScope
-> (Sing ty -> Maybe a) -> Sing ty -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtNotComparable Sing n1 -> Maybe (Dict (Comparable n1))
forall (t :: T). Sing t -> Maybe (Dict (Comparable t))
getComparableProofS Sing n1
s1
    Dict (HasNoOp n2)
Dict <- BadTypeForScope
-> (Sing n2 -> Maybe (Dict (HasNoOp n2)))
-> Sing n2
-> Either NotWellTyped (Dict (HasNoOp n2))
forall (ty :: T) a.
BadTypeForScope
-> (Sing ty -> Maybe a) -> Sing ty -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtIsOperation Sing n2 -> Maybe (Dict (HasNoOp n2))
forall (t :: T). Sing t -> Maybe (Dict $ HasNoOp t)
opAbsense Sing n2
s2
    Dict (HasNoBigMap n2)
Dict <- BadTypeForScope
-> (Sing n2 -> Maybe (Dict (HasNoBigMap n2)))
-> Sing n2
-> Either NotWellTyped (Dict (HasNoBigMap n2))
forall (ty :: T) a.
BadTypeForScope
-> (Sing ty -> Maybe a) -> Sing ty -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtHasBigMap Sing n2 -> Maybe (Dict (HasNoBigMap n2))
forall (t :: T). Sing t -> Maybe (Dict $ HasNoBigMap t)
bigMapAbsense Sing n2
s2
    Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STInt -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STNat -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STString -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STBytes -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STMutez -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STBool -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STKeyHash -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STBls12381Fr -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STBls12381G1 -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STBls12381G2 -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STTimestamp -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STAddress -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STChest -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STChestKey -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STTxRollupL2Address -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  Sing t
SingT t
STNever -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  STSaplingState Sing n
s -> Sing n
-> (SingI n => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
s ((SingI n => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (SingI n => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped ('TSaplingState n))
-> Either NotWellTyped (Dict (WellTyped ('TSaplingState n)))
forall a b. b -> Either a b
Right Dict (WellTyped ('TSaplingState n))
forall (a :: Constraint). a => Dict a
Dict
  STSaplingTransaction Sing n
s -> Sing n
-> (SingI n => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
s ((SingI n => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (SingI n => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped ('TSaplingTransaction n))
-> Either NotWellTyped (Dict (WellTyped ('TSaplingTransaction n)))
forall a b. b -> Either a b
Right Dict (WellTyped ('TSaplingTransaction n))
forall (a :: Constraint). a => Dict a
Dict
  where
    eitherWellTyped
      :: BadTypeForScope
      -> (Sing (ty :: T) -> Maybe a)
      -> Sing (ty :: T)
      -> Either NotWellTyped a
    eitherWellTyped :: forall (ty :: T) a.
BadTypeForScope
-> (Sing ty -> Maybe a) -> Sing ty -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
bt Sing ty -> Maybe a
sf Sing ty
sng = NotWellTyped -> Maybe a -> Either NotWellTyped a
forall l r. l -> Maybe r -> Either l r
maybeToRight (T -> BadTypeForScope -> NotWellTyped
NotWellTyped (Sing ty -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing ty
sng) BadTypeForScope
bt) (Maybe a -> Either NotWellTyped a)
-> Maybe a -> Either NotWellTyped a
forall a b. (a -> b) -> a -> b
$ Sing ty -> Maybe a
sf Sing ty
sng

getComparableProofS :: Sing (a :: T) -> Maybe (Dict (Comparable a))
getComparableProofS :: forall (t :: T). Sing t -> Maybe (Dict (Comparable t))
getComparableProofS Sing a
s = case Sing a -> Comparability a
forall (t :: T). Sing t -> Comparability t
checkComparability Sing a
s of
  Comparability a
CanBeCompared -> Dict (Comparable a) -> Maybe (Dict (Comparable a))
forall a. a -> Maybe a
Just Dict (Comparable a)
forall (a :: Constraint). a => Dict a
Dict
  Comparability a
CannotBeCompared -> Maybe (Dict (Comparable a))
forall a. Maybe a
Nothing

checkComparability :: Sing t -> Comparability t
checkComparability :: forall (t :: T). Sing t -> Comparability t
checkComparability = \case
  STPair Sing n1
a Sing n2
b -> case (Sing n1 -> Comparability n1
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n1
a, Sing n2 -> Comparability n2
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n2
b) of
    (Comparability n1
CanBeCompared, Comparability n2
CanBeCompared) -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
    (Comparability n1
CannotBeCompared, Comparability n2
_) -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
    (Comparability n1
_, Comparability n2
CannotBeCompared) -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STOr Sing n1
a Sing n2
b -> case (Sing n1 -> Comparability n1
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n1
a, Sing n2 -> Comparability n2
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n2
b) of
    (Comparability n1
CanBeCompared, Comparability n2
CanBeCompared) -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
    (Comparability n1
CannotBeCompared, Comparability n2
_) -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
    (Comparability n1
_, Comparability n2
CannotBeCompared) -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STOption Sing n
t -> case Sing n -> Comparability n
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n
t of
    Comparability n
CanBeCompared -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
    Comparability n
CannotBeCompared -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STList Sing n
_ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STSet Sing n
_ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  Sing t
SingT t
STOperation -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STContract Sing n
_ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STTicket Sing n
_ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STLambda Sing n1
_ Sing n2
_ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STMap Sing n1
_ Sing n2
_ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STBigMap Sing n1
_ Sing n2
_ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  Sing t
SingT t
STNever -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  Sing t
SingT t
STUnit -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  Sing t
SingT t
STInt -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  Sing t
SingT t
STNat -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  Sing t
SingT t
STString -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  Sing t
SingT t
STBytes -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  Sing t
SingT t
STMutez -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  Sing t
SingT t
STBool -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  Sing t
SingT t
STKeyHash -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  Sing t
SingT t
STBls12381Fr -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  Sing t
SingT t
STBls12381G1 -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  Sing t
SingT t
STBls12381G2 -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  Sing t
SingT t
STTimestamp -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  Sing t
SingT t
STAddress -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  Sing t
SingT t
STKey -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  Sing t
SingT t
STSignature -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  Sing t
SingT t
STChainId -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  Sing t
SingT t
STChest -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  Sing t
SingT t
STChestKey -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  Sing t
SingT t
STTxRollupL2Address -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  STSaplingState Sing n
_ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STSaplingTransaction Sing n
_ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared