{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Morley.Michelson.Typed.Scope
(
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 (..)
, 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'
, 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)
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
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
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
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
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
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
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
class (ContainsOp t ~ 'False) => HasNoOp t
instance (ContainsOp t ~ 'False) => HasNoOp t
class (ContainsContract t ~ 'False) => HasNoContract t
instance (ContainsContract t ~ 'False) => HasNoContract t
class (ContainsTicket t ~ 'False) => HasNoTicket t
instance (ContainsTicket t ~ 'False) => HasNoTicket t
class (ContainsBigMap t ~ 'False) => HasNoBigMap t
instance (ContainsBigMap t ~ 'False) => HasNoBigMap t
class (ContainsSaplingState t ~ 'False) => HasNoSaplingState t
instance (ContainsSaplingState t ~ 'False) => HasNoSaplingState t
class (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t
instance (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t
{-# DEPRECATED
FailOnOperationFound
, FailOnContractFound
, FailOnTicketFound
, FailOnBigMapFound
, FailOnNestedBigMapsFound
, FailOnNonComparableFound
"Use a Forbid* constraint instead"
#-}
type family FailOnOperationFound (enabled :: Bool) :: Constraint where
FailOnOperationFound 'True =
TypeError ('Text "Operations are not allowed in this scope")
FailOnOperationFound 'False = ()
type family FailOnContractFound (enabled :: Bool) :: Constraint where
FailOnContractFound 'True =
TypeError ('Text "Type `contract` is not allowed in this scope")
FailOnContractFound 'False = ()
type family FailOnTicketFound (enabled :: Bool) :: Constraint where
FailOnTicketFound 'True =
TypeError ('Text "Type `ticket` is not allowed in this scope")
FailOnTicketFound 'False = ()
type family FailOnBigMapFound (enabled :: Bool) :: Constraint where
FailOnBigMapFound 'True =
TypeError ('Text "BigMaps are not allowed in this scope")
FailOnBigMapFound 'False = ()
type family FailOnNestedBigMapsFound (enabled :: Bool) :: Constraint where
FailOnNestedBigMapsFound 'True =
TypeError ('Text "Nested BigMaps are not allowed")
FailOnNestedBigMapsFound 'False = ()
type family FailOnNonComparableFound (comparable :: Bool) :: Constraint where
FailOnNonComparableFound 'True = ()
FailOnNonComparableFound 'False =
TypeError ('Text "Only comparable types are allowed here")
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")
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."
#-}
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
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
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
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
data OpPresence (t :: T)
= ContainsOp t ~ 'True => OpPresent
| ContainsOp t ~ 'False => OpAbsent
data ContractPresence (t :: T)
= ContainsContract t ~ 'True => ContractPresent
| ContainsContract t ~ 'False => ContractAbsent
data TicketPresence (t :: T)
= ContainsTicket t ~ 'True => TicketPresent
| ContainsTicket t ~ 'False => TicketAbsent
data BigMapPresence (t :: T)
= ContainsBigMap t ~ 'True => BigMapPresent
| ContainsBigMap t ~ 'False => BigMapAbsent
data NestedBigMapsPresence (t :: T)
= ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresent
| ContainsNestedBigMaps t ~ 'False => NestedBigMapsAbsent
data SaplingStatePresence (t :: T)
= ContainsSaplingState t ~ 'True => SaplingStatePresent
| ContainsSaplingState t ~ 'False => SaplingStateAbsent
checkOpPresence :: Sing (ty :: T) -> OpPresence ty
checkOpPresence :: forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence = \case
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
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
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
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
checkBigMapPresence :: Sing (ty :: T) -> BigMapPresence ty
checkBigMapPresence :: forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence = \case
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
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
checkNestedBigMapsPresence :: Sing (ty :: T) -> NestedBigMapsPresence ty
checkNestedBigMapsPresence :: forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence = \case
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
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
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
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
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
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
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
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
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"
class (SingI t, WellTyped t, HasNoOp t, HasNoNestedBigMaps t) => ParameterScope t
instance (SingI t, WellTyped t, HasNoOp t, HasNoNestedBigMaps t) => ParameterScope t
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
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
class (SingI t, HasNoTicket t) => DupableScope t
instance (SingI t, HasNoTicket t) => DupableScope t
type family IsDupableScope (t :: T) :: Bool where
IsDupableScope t = Not (ContainsTicket t)
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
class (WellTyped t, PackedValScope t, ConstantScope t) => UnpackedValScope t
instance (WellTyped t, PackedValScope t, ConstantScope t) => UnpackedValScope t
class (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => ViewableScope t
instance (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => ViewableScope t
type UntypedValScope t = (SingI t, HasNoOp t)
class CheckScope (c :: Constraint) where
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
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)
class WithDeMorganScope (c :: T -> Constraint) t a b where
withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret
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 #-}
{-# RULES
"orL" forall s. orL s = unsafeCoerce Refl
#-}
simpleWithDeMorgan
:: forall sym a b ret.
((sym @@ a || sym @@ b) ~ 'False, SingI sym, SingI a)
=> (((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
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
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
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
class (SingI t, WellTypedSuperC t) => WellTyped (t :: T) where
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)
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
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
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