{-# 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.Constraint (Dict(..), withDict, (:-)(..), (\\))
import Data.Singletons (Sing, SingI(..), fromSing, withSingI)
import Data.Type.Bool (Not, type (&&), type (||))
import Fmt (Buildable(..))
import GHC.TypeLits (ErrorMessage(..), TypeError)
import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDoc)
import Morley.Michelson.Typed.Sing (SingT(..))
import Morley.Michelson.Typed.T (T(..))
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
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 FailOnSaplingStateFound (enabled :: Bool) :: Constraint where
FailOnSaplingStateFound 'True =
TypeError ('Text "Type `sapling_state` is not allowed in this scope")
FailOnSaplingStateFound '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 = FailOnOperationFound (ContainsOp t)
type ForbidContract t = FailOnContractFound (ContainsContract t)
type ForbidTicket t = FailOnTicketFound (ContainsTicket t)
type ForbidSaplingState t = FailOnSaplingStateFound (ContainsSaplingState t)
type ForbidBigMap t = FailOnBigMapFound (ContainsBigMap t)
type ForbidNestedBigMaps t = FailOnNestedBigMapsFound (ContainsNestedBigMaps t)
type ForbidNonComparable t = FailOnNonComparableFound (IsComparable t)
forbiddenOpEvi :: forall t. (SingI t, ForbidOp t) :- HasNoOp t
forbiddenOpEvi :: (SingI t, ForbidOp t) :- HasNoOp t
forbiddenOpEvi = ((SingI t, ForbidOp t) => Dict (HasNoOp t))
-> (SingI t, ForbidOp t) :- HasNoOp t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((SingI t, ForbidOp t) => Dict (HasNoOp t))
-> (SingI t, ForbidOp t) :- HasNoOp t)
-> ((SingI t, ForbidOp t) => Dict (HasNoOp t))
-> (SingI t, ForbidOp t) :- HasNoOp t
forall a b. (a -> b) -> a -> b
$
case Sing t -> OpPresence t
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence (SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @t) of
OpPresence t
OpAbsent -> Dict (HasNoOp t)
forall (a :: Constraint). a => Dict a
Dict
OpPresence t
OpPresent -> Text -> Dict (HasNoOp t)
forall a. HasCallStack => Text -> a
error Text
"impossible"
forbiddenOp
:: forall t a.
(SingI t, ForbidOp t)
=> (HasNoOp t => a)
-> a
forbiddenOp :: (HasNoOp t => a) -> a
forbiddenOp = ((SingI t, FailOnOperationFound (ContainsOp t)) :- HasNoOp t)
-> (HasNoOp t => a) -> a
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (((SingI t, FailOnOperationFound (ContainsOp t)) :- HasNoOp t)
-> (HasNoOp t => a) -> a)
-> ((SingI t, FailOnOperationFound (ContainsOp t)) :- HasNoOp t)
-> (HasNoOp t => a)
-> a
forall a b. (a -> b) -> a -> b
$ (SingI t, FailOnOperationFound (ContainsOp t)) :- HasNoOp t
forall (t :: T). (SingI t, ForbidOp t) :- HasNoOp t
forbiddenOpEvi @t
forbiddenBigMapEvi :: forall t. (SingI t, ForbidBigMap t) :- HasNoBigMap t
forbiddenBigMapEvi :: (SingI t, ForbidBigMap t) :- HasNoBigMap t
forbiddenBigMapEvi = ((SingI t, ForbidBigMap t) => Dict (HasNoBigMap t))
-> (SingI t, ForbidBigMap t) :- HasNoBigMap t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((SingI t, ForbidBigMap t) => Dict (HasNoBigMap t))
-> (SingI t, ForbidBigMap t) :- HasNoBigMap t)
-> ((SingI t, ForbidBigMap t) => Dict (HasNoBigMap t))
-> (SingI t, ForbidBigMap t) :- HasNoBigMap t
forall a b. (a -> b) -> a -> b
$
case Sing t -> BigMapPresence t
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence (SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @t) of
BigMapPresence t
BigMapAbsent -> Dict (HasNoBigMap t)
forall (a :: Constraint). a => Dict a
Dict
BigMapPresence t
BigMapPresent -> Text -> Dict (HasNoBigMap t)
forall a. HasCallStack => Text -> a
error Text
"impossible"
forbiddenNestedBigMapsEvi :: forall t. (SingI t, ForbidNestedBigMaps t) :- HasNoNestedBigMaps t
forbiddenNestedBigMapsEvi :: (SingI t, ForbidNestedBigMaps t) :- HasNoNestedBigMaps t
forbiddenNestedBigMapsEvi = ((SingI t, ForbidNestedBigMaps t) => Dict (HasNoNestedBigMaps t))
-> (SingI t, ForbidNestedBigMaps t) :- HasNoNestedBigMaps t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((SingI t, ForbidNestedBigMaps t) => Dict (HasNoNestedBigMaps t))
-> (SingI t, ForbidNestedBigMaps t) :- HasNoNestedBigMaps t)
-> ((SingI t, ForbidNestedBigMaps t) =>
Dict (HasNoNestedBigMaps t))
-> (SingI t, ForbidNestedBigMaps t) :- HasNoNestedBigMaps t
forall a b. (a -> b) -> a -> b
$
case Sing t -> NestedBigMapsPresence t
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence (SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @t) of
NestedBigMapsPresence t
NestedBigMapsAbsent -> Dict (HasNoNestedBigMaps t)
forall (a :: Constraint). a => Dict a
Dict
NestedBigMapsPresence t
NestedBigMapsPresent -> Text -> Dict (HasNoNestedBigMaps t)
forall a. HasCallStack => Text -> a
error Text
"impossible"
forbiddenBigMap
:: forall t a.
(SingI t, ForbidBigMap t)
=> (HasNoBigMap t => a)
-> a
forbiddenBigMap :: (HasNoBigMap t => a) -> a
forbiddenBigMap = ((SingI t, FailOnBigMapFound (ContainsBigMap t)) :- HasNoBigMap t)
-> (HasNoBigMap t => a) -> a
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (((SingI t, FailOnBigMapFound (ContainsBigMap t)) :- HasNoBigMap t)
-> (HasNoBigMap t => a) -> a)
-> ((SingI t, FailOnBigMapFound (ContainsBigMap t))
:- HasNoBigMap t)
-> (HasNoBigMap t => a)
-> a
forall a b. (a -> b) -> a -> b
$ (SingI t, FailOnBigMapFound (ContainsBigMap t)) :- HasNoBigMap t
forall (t :: T). (SingI t, ForbidBigMap t) :- HasNoBigMap t
forbiddenBigMapEvi @t
forbiddenNestedBigMaps
:: forall t a.
(SingI t, ForbidNestedBigMaps t)
=> (HasNoNestedBigMaps t => a)
-> a
forbiddenNestedBigMaps :: (HasNoNestedBigMaps t => a) -> a
forbiddenNestedBigMaps = ((SingI t, FailOnNestedBigMapsFound (ContainsNestedBigMaps t))
:- HasNoNestedBigMaps t)
-> (HasNoNestedBigMaps t => a) -> a
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (((SingI t, FailOnNestedBigMapsFound (ContainsNestedBigMaps t))
:- HasNoNestedBigMaps t)
-> (HasNoNestedBigMaps t => a) -> a)
-> ((SingI t, FailOnNestedBigMapsFound (ContainsNestedBigMaps t))
:- HasNoNestedBigMaps t)
-> (HasNoNestedBigMaps t => a)
-> a
forall a b. (a -> b) -> a -> b
$ (SingI t, FailOnNestedBigMapsFound (ContainsNestedBigMaps t))
:- HasNoNestedBigMaps t
forall (t :: T).
(SingI t, ForbidNestedBigMaps t) :- HasNoNestedBigMaps t
forbiddenNestedBigMapsEvi @t
forbiddenContractTypeEvi
:: forall t. (SingI t, ForbidContract t) :- HasNoContract t
forbiddenContractTypeEvi :: (SingI t, ForbidContract t) :- HasNoContract t
forbiddenContractTypeEvi = ((SingI t, ForbidContract t) => Dict (HasNoContract t))
-> (SingI t, ForbidContract t) :- HasNoContract t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((SingI t, ForbidContract t) => Dict (HasNoContract t))
-> (SingI t, ForbidContract t) :- HasNoContract t)
-> ((SingI t, ForbidContract t) => Dict (HasNoContract t))
-> (SingI t, ForbidContract t) :- HasNoContract t
forall a b. (a -> b) -> a -> b
$
case Sing t -> ContractPresence t
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence (SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @t) of
ContractPresence t
ContractAbsent -> Dict (HasNoContract t)
forall (a :: Constraint). a => Dict a
Dict
ContractPresence t
ContractPresent -> Text -> Dict (HasNoContract t)
forall a. HasCallStack => Text -> a
error Text
"impossible"
forbiddenContractType
:: forall t a.
(SingI t, ForbidContract t)
=> (HasNoContract t => a)
-> a
forbiddenContractType :: (HasNoContract t => a) -> a
forbiddenContractType = ((SingI t, FailOnContractFound (ContainsContract t))
:- HasNoContract t)
-> (HasNoContract t => a) -> a
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (((SingI t, FailOnContractFound (ContainsContract t))
:- HasNoContract t)
-> (HasNoContract t => a) -> a)
-> ((SingI t, FailOnContractFound (ContainsContract t))
:- HasNoContract t)
-> (HasNoContract t => a)
-> a
forall a b. (a -> b) -> a -> b
$ (SingI t, FailOnContractFound (ContainsContract t))
:- HasNoContract t
forall (t :: T). (SingI t, ForbidContract t) :- HasNoContract t
forbiddenContractTypeEvi @t
forbiddenTicketTypeEvi
:: forall t. (SingI t, ForbidTicket t) :- HasNoTicket t
forbiddenTicketTypeEvi :: (SingI t, ForbidTicket t) :- HasNoTicket t
forbiddenTicketTypeEvi = ((SingI t, ForbidTicket t) => Dict (HasNoTicket t))
-> (SingI t, ForbidTicket t) :- HasNoTicket t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((SingI t, ForbidTicket t) => Dict (HasNoTicket t))
-> (SingI t, ForbidTicket t) :- HasNoTicket t)
-> ((SingI t, ForbidTicket t) => Dict (HasNoTicket t))
-> (SingI t, ForbidTicket t) :- HasNoTicket t
forall a b. (a -> b) -> a -> b
$
case Sing t -> TicketPresence t
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence (SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @t) of
TicketPresence t
TicketAbsent -> Dict (HasNoTicket t)
forall (a :: Constraint). a => Dict a
Dict
TicketPresence t
TicketPresent -> Text -> Dict (HasNoTicket t)
forall a. HasCallStack => Text -> a
error Text
"impossible"
forbiddenSaplingStateTypeEvi
:: forall t. (SingI t, ForbidSaplingState t) :- HasNoSaplingState t
forbiddenSaplingStateTypeEvi :: (SingI t, ForbidSaplingState t) :- HasNoSaplingState t
forbiddenSaplingStateTypeEvi = ((SingI t, ForbidSaplingState t) => Dict (HasNoSaplingState t))
-> (SingI t, ForbidSaplingState t) :- HasNoSaplingState t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((SingI t, ForbidSaplingState t) => Dict (HasNoSaplingState t))
-> (SingI t, ForbidSaplingState t) :- HasNoSaplingState t)
-> ((SingI t, ForbidSaplingState t) => Dict (HasNoSaplingState t))
-> (SingI t, ForbidSaplingState t) :- HasNoSaplingState t
forall a b. (a -> b) -> a -> b
$
case Sing t -> SaplingStatePresence t
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence (SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @t) of
SaplingStatePresence t
SaplingStateAbsent -> Dict (HasNoSaplingState t)
forall (a :: Constraint). a => Dict a
Dict
SaplingStatePresence t
SaplingStatePresent -> Text -> Dict (HasNoSaplingState t)
forall a. HasCallStack => Text -> a
error Text
"impossible"
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 :: Sing ty -> OpPresence ty
checkOpPresence = \case
Sing ty
STKey -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STSignature -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STChainId -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STUnit -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
STOption 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 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 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
STOperation -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
STContract _ -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
STTicket 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 a b -> case (Sing n -> OpPresence n
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n
a, Sing n -> OpPresence n
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n
b) of
(OpPresence n
OpPresent, OpPresence n
_) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
(OpPresence n
_, OpPresence n
OpPresent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
(OpPresence n
OpAbsent, OpPresence n
OpAbsent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
STOr a b -> case (Sing n -> OpPresence n
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n
a, Sing n -> OpPresence n
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n
b) of
(OpPresence n
OpPresent, OpPresence n
_) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
(OpPresence n
_, OpPresence n
OpPresent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
(OpPresence n
OpAbsent, OpPresence n
OpAbsent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
STLambda _ _ -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
STMap k v -> case (Sing n -> OpPresence n
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n
k, Sing n -> OpPresence n
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n
v) of
(OpPresence n
OpAbsent, OpPresence n
OpAbsent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
(OpPresence n
OpPresent, OpPresence n
_) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
(OpPresence n
_, OpPresence n
OpPresent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
STBigMap k v -> case (Sing n -> OpPresence n
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n
k, Sing n -> OpPresence n
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n
v) of
(OpPresence n
OpAbsent, OpPresence n
OpAbsent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
(OpPresence n
OpPresent, OpPresence n
_) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
(OpPresence n
_, OpPresence n
OpPresent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
Sing ty
STInt -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STNat -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STString -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STBytes -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STMutez -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STBool -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STKeyHash -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STBls12381Fr -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STBls12381G1 -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STBls12381G2 -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STTimestamp -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STAddress -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STChest -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STChestKey -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
Sing ty
STNever -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
STSaplingState _ -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
STSaplingTransaction _ -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
checkContractTypePresence :: Sing (ty :: T) -> ContractPresence ty
checkContractTypePresence :: Sing ty -> ContractPresence ty
checkContractTypePresence = \case
Sing ty
STKey -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STSignature -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STChainId -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STUnit -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
STOption 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 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 _ -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STOperation -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
STContract _ -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
STTicket _ -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
STPair a b -> case (Sing n -> ContractPresence n
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n
a, Sing n -> ContractPresence n
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n
b) of
(ContractPresence n
ContractPresent, ContractPresence n
_) -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
(ContractPresence n
_, ContractPresence n
ContractPresent) -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
(ContractPresence n
ContractAbsent, ContractPresence n
ContractAbsent) -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
STOr a b -> case (Sing n -> ContractPresence n
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n
a, Sing n -> ContractPresence n
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n
b) of
(ContractPresence n
ContractPresent, ContractPresence n
_) -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
(ContractPresence n
_, ContractPresence n
ContractPresent) -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
(ContractPresence n
ContractAbsent, ContractPresence n
ContractAbsent) -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
STLambda _ _ -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
STMap _ v -> case Sing n -> ContractPresence n
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n
v 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
STBigMap _ v -> case Sing n -> ContractPresence n
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n
v 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
Sing ty
STInt -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STNat -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STString -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STBytes -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STMutez -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STBool -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STKeyHash -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STBls12381Fr -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STBls12381G1 -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STBls12381G2 -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STTimestamp -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STAddress -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STChest -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STChestKey -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
Sing ty
STNever -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
STSaplingState _ -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
STSaplingTransaction _ -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
checkTicketPresence :: Sing (ty :: T) -> TicketPresence ty
checkTicketPresence :: Sing ty -> TicketPresence ty
checkTicketPresence = \case
Sing ty
STKey -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STSignature -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STChainId -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STUnit -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
STOption 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 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 _ -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STOperation -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
STContract _ -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
STTicket _ -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'True) => TicketPresence t
TicketPresent
STPair a b -> case (Sing n -> TicketPresence n
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing n
a, Sing n -> TicketPresence n
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing n
b) of
(TicketPresence n
TicketPresent, TicketPresence n
_) -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'True) => TicketPresence t
TicketPresent
(TicketPresence n
_, TicketPresence n
TicketPresent) -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'True) => TicketPresence t
TicketPresent
(TicketPresence n
TicketAbsent, TicketPresence n
TicketAbsent) -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
STOr a b -> case (Sing n -> TicketPresence n
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing n
a, Sing n -> TicketPresence n
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing n
b) of
(TicketPresence n
TicketPresent, TicketPresence n
_) -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'True) => TicketPresence t
TicketPresent
(TicketPresence n
_, TicketPresence n
TicketPresent) -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'True) => TicketPresence t
TicketPresent
(TicketPresence n
TicketAbsent, TicketPresence n
TicketAbsent) -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
STLambda _ _ -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
STMap _ v -> case Sing n -> TicketPresence n
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing n
v 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
STBigMap _ v -> case Sing n -> TicketPresence n
forall (ty :: T). Sing ty -> TicketPresence ty
checkTicketPresence Sing n
v 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
Sing ty
STInt -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STNat -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STString -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STBytes -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STMutez -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STBool -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STKeyHash -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STBls12381Fr -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STBls12381G1 -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STBls12381G2 -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STTimestamp -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STAddress -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STChest -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STChestKey -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
Sing ty
STNever -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
STSaplingState _ -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
STSaplingTransaction _ -> TicketPresence ty
forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
TicketAbsent
checkBigMapPresence :: Sing (ty :: T) -> BigMapPresence ty
checkBigMapPresence :: Sing ty -> BigMapPresence ty
checkBigMapPresence = \case
Sing ty
STKey -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STSignature -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STChainId -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STUnit -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
STOption 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 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 _ -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STOperation -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
STContract _ -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
STTicket _ -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
STPair a b -> case (Sing n -> BigMapPresence n
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing n
a, Sing n -> BigMapPresence n
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing n
b) of
(BigMapPresence n
BigMapPresent, BigMapPresence n
_) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
(BigMapPresence n
_, BigMapPresence n
BigMapPresent) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
(BigMapPresence n
BigMapAbsent, BigMapPresence n
BigMapAbsent) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
STOr a b -> case (Sing n -> BigMapPresence n
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing n
a, Sing n -> BigMapPresence n
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing n
b) of
(BigMapPresence n
BigMapPresent, BigMapPresence n
_) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
(BigMapPresence n
_, BigMapPresence n
BigMapPresent) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
(BigMapPresence n
BigMapAbsent, BigMapPresence n
BigMapAbsent) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
STLambda _ _ -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
STMap _ v -> case Sing n -> BigMapPresence n
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing n
v 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
STBigMap _ _ ->
BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
Sing ty
STInt -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STNat -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STString -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STBytes -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STMutez -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STBool -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STKeyHash -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STBls12381Fr -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STBls12381G1 -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STBls12381G2 -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STTimestamp -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STAddress -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STChest -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STChestKey -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
Sing ty
STNever -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
STSaplingState _ -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
STSaplingTransaction _ -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
checkNestedBigMapsPresence :: Sing (ty :: T) -> NestedBigMapsPresence ty
checkNestedBigMapsPresence :: Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence = \case
Sing ty
STKey -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STSignature -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STChainId -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STUnit -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
STOption 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 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 _ -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STOperation -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
STContract _ -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
STTicket _ -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
STPair a b -> case (Sing n -> NestedBigMapsPresence n
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing n
a, Sing n -> NestedBigMapsPresence n
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing n
b) of
(NestedBigMapsPresence n
NestedBigMapsPresent, NestedBigMapsPresence n
_) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
(NestedBigMapsPresence n
_, NestedBigMapsPresence n
NestedBigMapsPresent) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
(NestedBigMapsPresence n
NestedBigMapsAbsent, NestedBigMapsPresence n
NestedBigMapsAbsent) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
STOr a b -> case (Sing n -> NestedBigMapsPresence n
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing n
a, Sing n -> NestedBigMapsPresence n
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing n
b) of
(NestedBigMapsPresence n
NestedBigMapsPresent, NestedBigMapsPresence n
_) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
(NestedBigMapsPresence n
_, NestedBigMapsPresence n
NestedBigMapsPresent) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
(NestedBigMapsPresence n
NestedBigMapsAbsent, NestedBigMapsPresence n
NestedBigMapsAbsent) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
STLambda _ _ -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
STMap _ v -> case Sing n -> NestedBigMapsPresence n
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing n
v 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
STBigMap _ v -> case Sing n -> BigMapPresence n
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing n
v of
BigMapPresence n
BigMapPresent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
BigMapPresence n
BigMapAbsent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STInt -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STNat -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STString -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STBytes -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STMutez -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STBool -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STKeyHash -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STBls12381Fr -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STBls12381G1 -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STBls12381G2 -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STTimestamp -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STAddress -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STChest -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STChestKey -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
Sing ty
STNever -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
STSaplingState _ -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
STSaplingTransaction _ -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
checkSaplingStatePresence :: Sing (ty :: T) -> SaplingStatePresence ty
checkSaplingStatePresence :: Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence = \case
Sing ty
STKey -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STSignature -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STChainId -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STUnit -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
STOption 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 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 _ -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STOperation -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
STContract _ -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
STTicket _ -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
STPair a b -> case (Sing n -> SaplingStatePresence n
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence Sing n
a, Sing n -> SaplingStatePresence n
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence Sing n
b) of
(SaplingStatePresence n
SaplingStatePresent, SaplingStatePresence n
_) -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'True) =>
SaplingStatePresence t
SaplingStatePresent
(SaplingStatePresence n
_, SaplingStatePresence n
SaplingStatePresent) -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'True) =>
SaplingStatePresence t
SaplingStatePresent
(SaplingStatePresence n
SaplingStateAbsent, SaplingStatePresence n
SaplingStateAbsent) -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
STOr a b -> case (Sing n -> SaplingStatePresence n
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence Sing n
a, Sing n -> SaplingStatePresence n
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence Sing n
b) of
(SaplingStatePresence n
SaplingStatePresent, SaplingStatePresence n
_) -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'True) =>
SaplingStatePresence t
SaplingStatePresent
(SaplingStatePresence n
_, SaplingStatePresence n
SaplingStatePresent) -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'True) =>
SaplingStatePresence t
SaplingStatePresent
(SaplingStatePresence n
SaplingStateAbsent, SaplingStatePresence n
SaplingStateAbsent) -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
STLambda _ _ -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
STMap _ v -> case Sing n -> SaplingStatePresence n
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence Sing n
v 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
STBigMap _ v -> case Sing n -> SaplingStatePresence n
forall (ty :: T). Sing ty -> SaplingStatePresence ty
checkSaplingStatePresence Sing n
v 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
Sing ty
STInt -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STNat -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STString -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STBytes -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STMutez -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STBool -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STKeyHash -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STBls12381Fr -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STBls12381G1 -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STBls12381G2 -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STTimestamp -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STAddress -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STChest -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STChestKey -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
Sing ty
STNever -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
STSaplingState _ -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'True) =>
SaplingStatePresence t
SaplingStatePresent
STSaplingTransaction _ -> SaplingStatePresence ty
forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
SaplingStateAbsent
opAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoOp t)
opAbsense :: 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 :: 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 :: 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 :: 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 :: 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 :: 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
$ SingI t => Either NotWellTyped (Dict (WellTyped t))
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 :: 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
<$> CheckScope (WellTyped t) =>
Either BadTypeForScope (Dict (WellTyped t))
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
<*> CheckScope (HasNoOp t) => Either BadTypeForScope (Dict (HasNoOp t))
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
<*> CheckScope (HasNoNestedBigMaps t) =>
Either BadTypeForScope (Dict (HasNoNestedBigMaps t))
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
<$> CheckScope (WellTyped t) =>
Either BadTypeForScope (Dict (WellTyped t))
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
<*> CheckScope (HasNoOp t) => Either BadTypeForScope (Dict (HasNoOp t))
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
<*> CheckScope (HasNoNestedBigMaps t) =>
Either BadTypeForScope (Dict (HasNoNestedBigMaps t))
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
<*> CheckScope (HasNoContract t) =>
Either BadTypeForScope (Dict (HasNoContract t))
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
<$> CheckScope (WellTyped t) =>
Either BadTypeForScope (Dict (WellTyped t))
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
<*> CheckScope (HasNoOp t) => Either BadTypeForScope (Dict (HasNoOp t))
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
<*> CheckScope (HasNoBigMap t) =>
Either BadTypeForScope (Dict (HasNoBigMap t))
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
<*> CheckScope (HasNoContract t) =>
Either BadTypeForScope (Dict (HasNoContract t))
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
<*> CheckScope (HasNoTicket t) =>
Either BadTypeForScope (Dict (HasNoTicket t))
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
<*> CheckScope (HasNoSaplingState t) =>
Either BadTypeForScope (Dict (HasNoSaplingState t))
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
<$> CheckScope (HasNoTicket t) =>
Either BadTypeForScope (Dict (HasNoTicket t))
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
<$> CheckScope (WellTyped t) =>
Either BadTypeForScope (Dict (WellTyped t))
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
<*> CheckScope (HasNoOp t) => Either BadTypeForScope (Dict (HasNoOp t))
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
<*> CheckScope (HasNoBigMap t) =>
Either BadTypeForScope (Dict (HasNoBigMap t))
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
<*> CheckScope (HasNoTicket t) =>
Either BadTypeForScope (Dict (HasNoTicket t))
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
<*> CheckScope (HasNoSaplingState t) =>
Either BadTypeForScope (Dict (HasNoSaplingState t))
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
<$> CheckScope (WellTyped t) =>
Either BadTypeForScope (Dict (WellTyped t))
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
<*> CheckScope (PackedValScope t) =>
Either BadTypeForScope (Dict (PackedValScope t))
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
<*> CheckScope (ConstantScope t) =>
Either BadTypeForScope (Dict (ConstantScope t))
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
<$> CheckScope (HasNoOp t) => Either BadTypeForScope (Dict (HasNoOp t))
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
<*> CheckScope (HasNoBigMap t) =>
Either BadTypeForScope (Dict (HasNoBigMap t))
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
<*> CheckScope (HasNoTicket t) =>
Either BadTypeForScope (Dict (HasNoTicket t))
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
<$> CheckScope (Comparable t) =>
Either BadTypeForScope (Dict (Comparable t))
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
mkWithDeMorgan
:: forall scope a ret. CheckScope (scope a)
=> (scope a => ret) -> ret
mkWithDeMorgan :: (scope a => ret) -> ret
mkWithDeMorgan scope a => ret
f = ret -> Either BadTypeForScope ret -> ret
forall b a. b -> Either a b -> b
fromRight (Text -> ret
forall a. HasCallStack => Text -> a
error Text
"impossible") (Either BadTypeForScope ret -> ret)
-> Either BadTypeForScope ret -> ret
forall a b. (a -> b) -> a -> b
$ do
Dict (scope a)
Dict <- CheckScope (scope a) => Either BadTypeForScope (Dict (scope a))
forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(scope a)
ret -> Either BadTypeForScope ret
forall (f :: * -> *) a. Applicative f => a -> f a
pure ret
scope a => ret
f
instance SingI a => WithDeMorganScope HasNoOp 'TPair a b where
withDeMorganScope :: ((HasNoOp a, HasNoOp b) => ret) -> ret
withDeMorganScope = forall ret. CheckScope (HasNoOp a) => (HasNoOp a => ret) -> ret
forall k (scope :: k -> Constraint) (a :: k) ret.
CheckScope (scope a) =>
(scope a => ret) -> ret
mkWithDeMorgan @HasNoOp @a
instance SingI a => WithDeMorganScope HasNoContract 'TPair a b where
withDeMorganScope :: ((HasNoContract a, HasNoContract b) => ret) -> ret
withDeMorganScope = forall ret.
CheckScope (HasNoContract a) =>
(HasNoContract a => ret) -> ret
forall k (scope :: k -> Constraint) (a :: k) ret.
CheckScope (scope a) =>
(scope a => ret) -> ret
mkWithDeMorgan @HasNoContract @a
instance SingI a => WithDeMorganScope HasNoTicket 'TPair a b where
withDeMorganScope :: ((HasNoTicket a, HasNoTicket b) => ret) -> ret
withDeMorganScope = forall ret.
CheckScope (HasNoTicket a) =>
(HasNoTicket a => ret) -> ret
forall k (scope :: k -> Constraint) (a :: k) ret.
CheckScope (scope a) =>
(scope a => ret) -> ret
mkWithDeMorgan @HasNoTicket @a
instance SingI a => WithDeMorganScope HasNoBigMap 'TPair a b where
withDeMorganScope :: ((HasNoBigMap a, HasNoBigMap b) => ret) -> ret
withDeMorganScope = forall ret.
CheckScope (HasNoBigMap a) =>
(HasNoBigMap a => ret) -> ret
forall k (scope :: k -> Constraint) (a :: k) ret.
CheckScope (scope a) =>
(scope a => ret) -> ret
mkWithDeMorgan @HasNoBigMap @a
instance SingI a => WithDeMorganScope HasNoNestedBigMaps 'TPair a b where
withDeMorganScope :: ((HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret) -> ret
withDeMorganScope = forall ret.
CheckScope (HasNoNestedBigMaps a) =>
(HasNoNestedBigMaps a => ret) -> ret
forall k (scope :: k -> Constraint) (a :: k) ret.
CheckScope (scope a) =>
(scope a => ret) -> ret
mkWithDeMorgan @HasNoNestedBigMaps @a
instance SingI a => WithDeMorganScope HasNoOp 'TOr a b where
withDeMorganScope :: ((HasNoOp a, HasNoOp b) => ret) -> ret
withDeMorganScope = forall ret. CheckScope (HasNoOp a) => (HasNoOp a => ret) -> ret
forall k (scope :: k -> Constraint) (a :: k) ret.
CheckScope (scope a) =>
(scope a => ret) -> ret
mkWithDeMorgan @HasNoOp @a
instance SingI a => WithDeMorganScope HasNoContract 'TOr a b where
withDeMorganScope :: ((HasNoContract a, HasNoContract b) => ret) -> ret
withDeMorganScope = forall ret.
CheckScope (HasNoContract a) =>
(HasNoContract a => ret) -> ret
forall k (scope :: k -> Constraint) (a :: k) ret.
CheckScope (scope a) =>
(scope a => ret) -> ret
mkWithDeMorgan @HasNoContract @a
instance SingI a => WithDeMorganScope HasNoTicket 'TOr a b where
withDeMorganScope :: ((HasNoTicket a, HasNoTicket b) => ret) -> ret
withDeMorganScope = forall ret.
CheckScope (HasNoTicket a) =>
(HasNoTicket a => ret) -> ret
forall k (scope :: k -> Constraint) (a :: k) ret.
CheckScope (scope a) =>
(scope a => ret) -> ret
mkWithDeMorgan @HasNoTicket @a
instance SingI a => WithDeMorganScope HasNoBigMap 'TOr a b where
withDeMorganScope :: ((HasNoBigMap a, HasNoBigMap b) => ret) -> ret
withDeMorganScope = forall ret.
CheckScope (HasNoBigMap a) =>
(HasNoBigMap a => ret) -> ret
forall k (scope :: k -> Constraint) (a :: k) ret.
CheckScope (scope a) =>
(scope a => ret) -> ret
mkWithDeMorgan @HasNoBigMap @a
instance SingI a => WithDeMorganScope HasNoNestedBigMaps 'TOr a b where
withDeMorganScope :: ((HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret) -> ret
withDeMorganScope = forall ret.
CheckScope (HasNoNestedBigMaps a) =>
(HasNoNestedBigMaps a => ret) -> ret
forall k (scope :: k -> Constraint) (a :: k) ret.
CheckScope (scope a) =>
(scope a => ret) -> ret
mkWithDeMorgan @HasNoNestedBigMaps @a
instance SingI k => WithDeMorganScope HasNoOp 'TMap k v where
withDeMorganScope :: ((HasNoOp k, HasNoOp v) => ret) -> ret
withDeMorganScope = forall ret. CheckScope (HasNoOp k) => (HasNoOp k => ret) -> ret
forall k (scope :: k -> Constraint) (a :: k) ret.
CheckScope (scope a) =>
(scope a => ret) -> ret
mkWithDeMorgan @HasNoOp @k
instance SingI k => WithDeMorganScope HasNoOp 'TBigMap k v where
withDeMorganScope :: ((HasNoOp k, HasNoOp v) => ret) -> ret
withDeMorganScope = forall ret. CheckScope (HasNoOp k) => (HasNoOp k => ret) -> ret
forall k (scope :: k -> Constraint) (a :: k) ret.
CheckScope (scope a) =>
(scope a => ret) -> ret
mkWithDeMorgan @HasNoOp @k
instance
( WithDeMorganScope HasNoOp t a b
, WithDeMorganScope HasNoNestedBigMaps t a b
, SingI a, SingI b
, WellTyped a, WellTyped b
) => WithDeMorganScope ParameterScope t a b where
withDeMorganScope :: ((ParameterScope a, ParameterScope b) => ret) -> ret
withDeMorganScope (ParameterScope a, ParameterScope b) => ret
f =
forall ret.
(WithDeMorganScope HasNoOp t a b, HasNoOp (t a b)) =>
((HasNoOp a, HasNoOp b) => ret) -> ret
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
$
((HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret) -> ret
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
, SingI a, SingI b
, WellTyped a, WellTyped b
) => WithDeMorganScope StorageScope t a b where
withDeMorganScope :: ((StorageScope a, StorageScope b) => ret) -> ret
withDeMorganScope (StorageScope a, StorageScope b) => ret
f =
forall ret.
(WithDeMorganScope HasNoOp t a b, HasNoOp (t a b)) =>
((HasNoOp a, HasNoOp b) => ret) -> ret
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 ret.
(WithDeMorganScope HasNoNestedBigMaps t a b,
HasNoNestedBigMaps (t a b)) =>
((HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret) -> ret
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
$
((HasNoContract a, HasNoContract b) => ret) -> ret
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
, SingI a, SingI b
, WellTyped a, WellTyped b
) => WithDeMorganScope ConstantScope t a b where
withDeMorganScope :: ((ConstantScope a, ConstantScope b) => ret) -> ret
withDeMorganScope (ConstantScope a, ConstantScope b) => ret
f =
forall ret.
(WithDeMorganScope HasNoOp t a b, HasNoOp (t a b)) =>
((HasNoOp a, HasNoOp b) => ret) -> ret
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 ret.
(WithDeMorganScope HasNoBigMap t a b, HasNoBigMap (t a b)) =>
((HasNoBigMap a, HasNoBigMap b) => ret) -> ret
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 ret.
(WithDeMorganScope HasNoContract t a b, HasNoContract (t a b)) =>
((HasNoContract a, HasNoContract b) => ret) -> ret
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 ret.
(WithDeMorganScope HasNoTicket t a b, HasNoTicket (t a b)) =>
((HasNoTicket a, HasNoTicket b) => ret) -> ret
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
$
((HasNoSaplingState a, HasNoSaplingState b) => ret) -> ret
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
, SingI a, SingI b
, WellTyped a, WellTyped b
) => WithDeMorganScope PackedValScope t a b where
withDeMorganScope :: ((PackedValScope a, PackedValScope b) => ret) -> ret
withDeMorganScope (PackedValScope a, PackedValScope b) => ret
f =
forall ret.
(WithDeMorganScope HasNoOp t a b, HasNoOp (t a b)) =>
((HasNoOp a, HasNoOp b) => ret) -> ret
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 ret.
(WithDeMorganScope HasNoBigMap t a b, HasNoBigMap (t a b)) =>
((HasNoBigMap a, HasNoBigMap b) => ret) -> ret
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 ret.
(WithDeMorganScope HasNoTicket t a b, HasNoTicket (t a b)) =>
((HasNoTicket a, HasNoTicket b) => ret) -> ret
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
$
((HasNoSaplingState a, HasNoSaplingState b) => ret) -> ret
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
, SingI a, SingI b
, WellTyped a, WellTyped b
) => WithDeMorganScope UnpackedValScope t a b where
withDeMorganScope :: ((UnpackedValScope a, UnpackedValScope b) => ret) -> ret
withDeMorganScope (UnpackedValScope a, UnpackedValScope b) => ret
f =
forall ret.
(WithDeMorganScope PackedValScope t a b, PackedValScope (t a b)) =>
((PackedValScope a, PackedValScope b) => ret) -> ret
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
$
((ConstantScope a, ConstantScope b) => ret) -> ret
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)
properParameterEvi :: forall t. ProperParameterBetterErrors t :- ParameterScope t
properParameterEvi :: ProperParameterBetterErrors t :- ParameterScope t
properParameterEvi = (ProperParameterBetterErrors t => Dict (ParameterScope t))
-> ProperParameterBetterErrors t :- ParameterScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((ProperParameterBetterErrors t => Dict (ParameterScope t))
-> ProperParameterBetterErrors t :- ParameterScope t)
-> (ProperParameterBetterErrors t => Dict (ParameterScope t))
-> ProperParameterBetterErrors t :- ParameterScope t
forall a b. (a -> b) -> a -> b
$
HasNoOp t => Dict (ParameterScope t)
forall (a :: Constraint). a => Dict a
Dict (HasNoOp t => Dict (ParameterScope t))
-> ((SingI t, FailOnOperationFound (ContainsOp t)) :- HasNoOp t)
-> Dict (ParameterScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnOperationFound (ContainsOp t)) :- HasNoOp t
forall (t :: T). (SingI t, ForbidOp t) :- HasNoOp t
forbiddenOpEvi @t (HasNoNestedBigMaps t => Dict (ParameterScope t))
-> ((SingI t, FailOnNestedBigMapsFound (ContainsNestedBigMaps t))
:- HasNoNestedBigMaps t)
-> Dict (ParameterScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnNestedBigMapsFound (ContainsNestedBigMaps t))
:- HasNoNestedBigMaps t
forall (t :: T).
(SingI t, ForbidNestedBigMaps t) :- HasNoNestedBigMaps t
forbiddenNestedBigMapsEvi @t
properStorageEvi :: forall t. ProperStorageBetterErrors t :- StorageScope t
properStorageEvi :: ProperStorageBetterErrors t :- StorageScope t
properStorageEvi = (ProperStorageBetterErrors t => Dict (StorageScope t))
-> ProperStorageBetterErrors t :- StorageScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((ProperStorageBetterErrors t => Dict (StorageScope t))
-> ProperStorageBetterErrors t :- StorageScope t)
-> (ProperStorageBetterErrors t => Dict (StorageScope t))
-> ProperStorageBetterErrors t :- StorageScope t
forall a b. (a -> b) -> a -> b
$
HasNoOp t => Dict (StorageScope t)
forall (a :: Constraint). a => Dict a
Dict (HasNoOp t => Dict (StorageScope t))
-> ((SingI t, FailOnOperationFound (ContainsOp t)) :- HasNoOp t)
-> Dict (StorageScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnOperationFound (ContainsOp t)) :- HasNoOp t
forall (t :: T). (SingI t, ForbidOp t) :- HasNoOp t
forbiddenOpEvi @t
(HasNoContract t => Dict (StorageScope t))
-> ((SingI t, () :: Constraint) :- HasNoContract t)
-> Dict (StorageScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, ForbidContract t) :- HasNoContract t
forall (t :: T). (SingI t, ForbidContract t) :- HasNoContract t
forbiddenContractTypeEvi @t
(HasNoNestedBigMaps t => Dict (StorageScope t))
-> ((SingI t, FailOnNestedBigMapsFound (ContainsNestedBigMaps t))
:- HasNoNestedBigMaps t)
-> Dict (StorageScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnNestedBigMapsFound (ContainsNestedBigMaps t))
:- HasNoNestedBigMaps t
forall (t :: T).
(SingI t, ForbidNestedBigMaps t) :- HasNoNestedBigMaps t
forbiddenNestedBigMapsEvi @t
(HasNoContract t => Dict (StorageScope t))
-> ((SingI t, ForbidContract t) :- HasNoContract t)
-> Dict (StorageScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, ForbidContract t) :- HasNoContract t
forall (t :: T). (SingI t, ForbidContract t) :- HasNoContract t
forbiddenContractTypeEvi @t
properConstantEvi :: forall t. ProperConstantBetterErrors t :- ConstantScope t
properConstantEvi :: ProperConstantBetterErrors t :- ConstantScope t
properConstantEvi = (ProperConstantBetterErrors t => Dict (ConstantScope t))
-> ProperConstantBetterErrors t :- ConstantScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((ProperConstantBetterErrors t => Dict (ConstantScope t))
-> ProperConstantBetterErrors t :- ConstantScope t)
-> (ProperConstantBetterErrors t => Dict (ConstantScope t))
-> ProperConstantBetterErrors t :- ConstantScope t
forall a b. (a -> b) -> a -> b
$
HasNoOp t => Dict (ConstantScope t)
forall (a :: Constraint). a => Dict a
Dict (HasNoOp t => Dict (ConstantScope t))
-> ((SingI t, FailOnOperationFound (ContainsOp t)) :- HasNoOp t)
-> Dict (ConstantScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnOperationFound (ContainsOp t)) :- HasNoOp t
forall (t :: T). (SingI t, ForbidOp t) :- HasNoOp t
forbiddenOpEvi @t
(HasNoBigMap t => Dict (ConstantScope t))
-> ((SingI t, FailOnBigMapFound (ContainsBigMap t))
:- HasNoBigMap t)
-> Dict (ConstantScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnBigMapFound (ContainsBigMap t)) :- HasNoBigMap t
forall (t :: T). (SingI t, ForbidBigMap t) :- HasNoBigMap t
forbiddenBigMapEvi @t
(HasNoContract t => Dict (ConstantScope t))
-> ((SingI t, FailOnContractFound (ContainsContract t))
:- HasNoContract t)
-> Dict (ConstantScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnContractFound (ContainsContract t))
:- HasNoContract t
forall (t :: T). (SingI t, ForbidContract t) :- HasNoContract t
forbiddenContractTypeEvi @t
(HasNoTicket t => Dict (ConstantScope t))
-> ((SingI t, FailOnTicketFound (ContainsTicket t))
:- HasNoTicket t)
-> Dict (ConstantScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnTicketFound (ContainsTicket t)) :- HasNoTicket t
forall (t :: T). (SingI t, ForbidTicket t) :- HasNoTicket t
forbiddenTicketTypeEvi @t
(HasNoSaplingState t => Dict (ConstantScope t))
-> ((SingI t, FailOnSaplingStateFound (ContainsSaplingState t))
:- HasNoSaplingState t)
-> Dict (ConstantScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnSaplingStateFound (ContainsSaplingState t))
:- HasNoSaplingState t
forall (t :: T).
(SingI t, ForbidSaplingState t) :- HasNoSaplingState t
forbiddenSaplingStateTypeEvi @t
properDupableEvi :: forall t. ProperDupableBetterErrors t :- DupableScope t
properDupableEvi :: ProperDupableBetterErrors t :- DupableScope t
properDupableEvi = (ProperDupableBetterErrors t => Dict (DupableScope t))
-> ProperDupableBetterErrors t :- DupableScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((ProperDupableBetterErrors t => Dict (DupableScope t))
-> ProperDupableBetterErrors t :- DupableScope t)
-> (ProperDupableBetterErrors t => Dict (DupableScope t))
-> ProperDupableBetterErrors t :- DupableScope t
forall a b. (a -> b) -> a -> b
$
HasNoTicket t => Dict (DupableScope t)
forall (a :: Constraint). a => Dict a
Dict (HasNoTicket t => Dict (DupableScope t))
-> (ProperDupableBetterErrors t :- HasNoTicket t)
-> Dict (DupableScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ProperDupableBetterErrors t :- HasNoTicket t
forall (t :: T). (SingI t, ForbidTicket t) :- HasNoTicket t
forbiddenTicketTypeEvi @t
properPackedValEvi :: forall t. ProperPackedValBetterErrors t :- PackedValScope t
properPackedValEvi :: ProperPackedValBetterErrors t :- PackedValScope t
properPackedValEvi = (ProperPackedValBetterErrors t => Dict (PackedValScope t))
-> ProperPackedValBetterErrors t :- PackedValScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((ProperPackedValBetterErrors t => Dict (PackedValScope t))
-> ProperPackedValBetterErrors t :- PackedValScope t)
-> (ProperPackedValBetterErrors t => Dict (PackedValScope t))
-> ProperPackedValBetterErrors t :- PackedValScope t
forall a b. (a -> b) -> a -> b
$
HasNoOp t => Dict (PackedValScope t)
forall (a :: Constraint). a => Dict a
Dict (HasNoOp t => Dict (PackedValScope t))
-> ((SingI t, FailOnOperationFound (ContainsOp t)) :- HasNoOp t)
-> Dict (PackedValScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnOperationFound (ContainsOp t)) :- HasNoOp t
forall (t :: T). (SingI t, ForbidOp t) :- HasNoOp t
forbiddenOpEvi @t
(HasNoBigMap t => Dict (PackedValScope t))
-> ((SingI t, FailOnBigMapFound (ContainsBigMap t))
:- HasNoBigMap t)
-> Dict (PackedValScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnBigMapFound (ContainsBigMap t)) :- HasNoBigMap t
forall (t :: T). (SingI t, ForbidBigMap t) :- HasNoBigMap t
forbiddenBigMapEvi @t
(HasNoTicket t => Dict (PackedValScope t))
-> ((SingI t, FailOnTicketFound (ContainsTicket t))
:- HasNoTicket t)
-> Dict (PackedValScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnTicketFound (ContainsTicket t)) :- HasNoTicket t
forall (t :: T). (SingI t, ForbidTicket t) :- HasNoTicket t
forbiddenTicketTypeEvi @t
(HasNoSaplingState t => Dict (PackedValScope t))
-> ((SingI t, FailOnSaplingStateFound (ContainsSaplingState t))
:- HasNoSaplingState t)
-> Dict (PackedValScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnSaplingStateFound (ContainsSaplingState t))
:- HasNoSaplingState t
forall (t :: T).
(SingI t, ForbidSaplingState t) :- HasNoSaplingState t
forbiddenSaplingStateTypeEvi @t
properUnpackedValEvi :: forall t. ProperUnpackedValBetterErrors t :- UnpackedValScope t
properUnpackedValEvi :: ProperUnpackedValBetterErrors t :- UnpackedValScope t
properUnpackedValEvi = (ProperUnpackedValBetterErrors t => Dict (UnpackedValScope t))
-> ProperUnpackedValBetterErrors t :- UnpackedValScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((ProperUnpackedValBetterErrors t => Dict (UnpackedValScope t))
-> ProperUnpackedValBetterErrors t :- UnpackedValScope t)
-> (ProperUnpackedValBetterErrors t => Dict (UnpackedValScope t))
-> ProperUnpackedValBetterErrors t :- UnpackedValScope t
forall a b. (a -> b) -> a -> b
$
PackedValScope t => Dict (UnpackedValScope t)
forall (a :: Constraint). a => Dict a
Dict (PackedValScope t => Dict (UnpackedValScope t))
-> ((SingI t, WellTyped t, () :: Constraint, () :: Constraint,
() :: Constraint, () :: Constraint)
:- PackedValScope t)
-> Dict (UnpackedValScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ProperPackedValBetterErrors t :- PackedValScope t
forall (t :: T). ProperPackedValBetterErrors t :- PackedValScope t
properPackedValEvi @t
(ConstantScope t => Dict (UnpackedValScope t))
-> ((SingI t, WellTyped t, FailOnOperationFound (ContainsOp t),
FailOnBigMapFound (ContainsBigMap t),
FailOnContractFound (ContainsContract t),
FailOnTicketFound (ContainsTicket t),
FailOnSaplingStateFound (ContainsSaplingState t))
:- ConstantScope t)
-> Dict (UnpackedValScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, WellTyped t, FailOnOperationFound (ContainsOp t),
FailOnBigMapFound (ContainsBigMap t),
FailOnContractFound (ContainsContract t),
FailOnTicketFound (ContainsTicket t),
FailOnSaplingStateFound (ContainsSaplingState t))
:- ConstantScope t
forall (t :: T). ProperConstantBetterErrors t :- ConstantScope t
properConstantEvi @t
properViewableEvi :: forall t. ProperViewableBetterErrors t :- ViewableScope t
properViewableEvi :: ProperViewableBetterErrors t :- ViewableScope t
properViewableEvi = (ProperViewableBetterErrors t => Dict (ViewableScope t))
-> ProperViewableBetterErrors t :- ViewableScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((ProperViewableBetterErrors t => Dict (ViewableScope t))
-> ProperViewableBetterErrors t :- ViewableScope t)
-> (ProperViewableBetterErrors t => Dict (ViewableScope t))
-> ProperViewableBetterErrors t :- ViewableScope t
forall a b. (a -> b) -> a -> b
$
HasNoOp t => Dict (ViewableScope t)
forall (a :: Constraint). a => Dict a
Dict (HasNoOp t => Dict (ViewableScope t))
-> ((SingI t, FailOnOperationFound (ContainsOp t)) :- HasNoOp t)
-> Dict (ViewableScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnOperationFound (ContainsOp t)) :- HasNoOp t
forall (t :: T). (SingI t, ForbidOp t) :- HasNoOp t
forbiddenOpEvi @t
(HasNoBigMap t => Dict (ViewableScope t))
-> ((SingI t, FailOnBigMapFound (ContainsBigMap t))
:- HasNoBigMap t)
-> Dict (ViewableScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnBigMapFound (ContainsBigMap t)) :- HasNoBigMap t
forall (t :: T). (SingI t, ForbidBigMap t) :- HasNoBigMap t
forbiddenBigMapEvi @t
(HasNoTicket t => Dict (ViewableScope t))
-> ((SingI t, FailOnTicketFound (ContainsTicket t))
:- HasNoTicket t)
-> Dict (ViewableScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, FailOnTicketFound (ContainsTicket t)) :- HasNoTicket t
forall (t :: T). (SingI t, ForbidTicket t) :- HasNoTicket t
forbiddenTicketTypeEvi @t
properUntypedValEvi :: forall t. ProperUntypedValBetterErrors t :- UntypedValScope t
properUntypedValEvi :: ProperUntypedValBetterErrors t :- UntypedValScope t
properUntypedValEvi = (ProperUntypedValBetterErrors t => Dict (UntypedValScope t))
-> ProperUntypedValBetterErrors t :- UntypedValScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((ProperUntypedValBetterErrors t => Dict (UntypedValScope t))
-> ProperUntypedValBetterErrors t :- UntypedValScope t)
-> (ProperUntypedValBetterErrors t => Dict (UntypedValScope t))
-> ProperUntypedValBetterErrors t :- UntypedValScope t
forall a b. (a -> b) -> a -> b
$
HasNoOp t => Dict (UntypedValScope t)
forall (a :: Constraint). a => Dict a
Dict (HasNoOp t => Dict (UntypedValScope t))
-> (ProperUntypedValBetterErrors t :- HasNoOp t)
-> Dict (UntypedValScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ProperUntypedValBetterErrors t :- HasNoOp t
forall (t :: T). (SingI t, ForbidOp t) :- HasNoOp t
forbiddenOpEvi @t
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 '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 where
instance WellTyped 'TChestKey where
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)
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 :: 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' :: Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' = \case
Sing 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
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
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
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 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 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 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
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 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 (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 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 s1 s2 -> 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
s1
Dict (WellTyped n)
Dict <- Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n
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 s1 s2 -> 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
s1
Dict (WellTyped n)
Dict <- Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n
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 s1 s2 -> 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
s1
Dict (WellTyped n)
Dict <- Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n
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 s1 s2 -> 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
s1
Dict (WellTyped n)
Dict <- Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n
s2
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
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 s1 s2 -> 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
s1
Dict (WellTyped n)
Dict <- Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n
s2
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
s1
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
s2
Dict (HasNoBigMap n)
Dict <- BadTypeForScope
-> (Sing n -> Maybe (Dict (HasNoBigMap n)))
-> Sing n
-> Either NotWellTyped (Dict (HasNoBigMap n))
forall (ty :: T) a.
BadTypeForScope
-> (Sing ty -> Maybe a) -> Sing ty -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtHasBigMap Sing n -> Maybe (Dict (HasNoBigMap n))
forall (t :: T). Sing t -> Maybe (Dict $ HasNoBigMap t)
bigMapAbsense Sing n
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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 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 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 :: 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 :: Sing a -> Maybe (Dict (Comparable a))
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 :: Sing t -> Comparability t
checkComparability = \case
STPair a b -> case (Sing n -> Comparability n
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n
a, Sing n -> Comparability n
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n
b) of
(Comparability n
CanBeCompared, Comparability n
CanBeCompared) -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
(Comparability n
CannotBeCompared, Comparability n
_) -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
(Comparability n
_, Comparability n
CannotBeCompared) -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STOr a b -> case (Sing n -> Comparability n
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n
a, Sing n -> Comparability n
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n
b) of
(Comparability n
CanBeCompared, Comparability n
CanBeCompared) -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
(Comparability n
CannotBeCompared, Comparability n
_) -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
(Comparability n
_, Comparability n
CannotBeCompared) -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STOption 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 _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STSet _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
Sing t
STOperation -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STContract _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STTicket _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STLambda _ _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STMap _ _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STBigMap _ _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
Sing t
STNever -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STUnit -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STInt -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STNat -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STString -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STBytes -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STMutez -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STBool -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STKeyHash -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STBls12381Fr -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
Sing t
STBls12381G1 -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
Sing t
STBls12381G2 -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
Sing t
STTimestamp -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STAddress -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STKey -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STSignature -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STChainId -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STChest -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
Sing t
STChestKey -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STSaplingState _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STSaplingTransaction _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared