{-# OPTIONS_HADDOCK not-home #-}
module Morley.Michelson.Typed.Scope.Internal.Deprecated
( module Morley.Michelson.Typed.Scope.Internal.Deprecated
) where
import Data.Constraint (Dict(..), (\\))
import Data.Singletons (Sing, SingI(..))
import Data.Type.Bool (Not)
import Data.Type.Equality ((:~:)(..))
import Morley.Michelson.Typed.Scope.Internal.Comparable
import Morley.Michelson.Typed.Scope.Internal.ForbidT
import Morley.Michelson.Typed.Scope.Internal.Presence
import Morley.Michelson.Typed.Scope.Internal.WellTyped
import Morley.Michelson.Typed.Sing (SingT(..))
import Morley.Michelson.Typed.T (T(..))
import Morley.Util.StubbedProof (stubProof)
type ContainsOp t = ContainsT 'PSOp t
type ContainsContract t = ContainsT 'PSContract t
type ContainsTicket t = ContainsT 'PSTicket t
type ContainsBigMap t = ContainsT 'PSBigMap t
type ContainsNestedBigMaps t = ContainsT 'PSNestedBigMaps t
type ContainsSaplingState t = ContainsT 'PSSaplingState t
{-# DEPRECATED
ContainsOp
, ContainsContract
, ContainsTicket
, ContainsBigMap
, ContainsNestedBigMaps
, ContainsSaplingState
"Use 'ContainsT' with the corresponding type marker, e.g. \
\'ContainsT PSOp', 'ContainsT PSTicket', etc"
#-}
class (ContainsOp t ~ 'False) => HasNoOp t
instance (ContainsOp t ~ 'False) => HasNoOp t
class (ContainsContract t ~ 'False) => HasNoContract t
instance (ContainsContract t ~ 'False) => HasNoContract t
class (ContainsTicket t ~ 'False) => HasNoTicket t
instance (ContainsTicket t ~ 'False) => HasNoTicket t
class (ContainsBigMap t ~ 'False) => HasNoBigMap t
instance (ContainsBigMap t ~ 'False) => HasNoBigMap t
class (ContainsSaplingState t ~ 'False) => HasNoSaplingState t
instance (ContainsSaplingState t ~ 'False) => HasNoSaplingState t
class (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t
instance (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t
{-# DEPRECATED HasNoOp, HasNoContract, HasNoTicket, HasNoBigMap, HasNoSaplingState, HasNoNestedBigMaps
"Use Forbid* instead" #-}
type OpPresence (t :: T) = TPresence 'PSOp t
pattern OpPresent :: () => ContainsOp t ~ 'True => OpPresence t
pattern $bOpPresent :: forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
$mOpPresent :: forall {r} {t :: T}.
OpPresence t -> ((ContainsOp t ~ 'True) => r) -> (Void# -> r) -> r
OpPresent = TPresent
pattern OpAbsent :: () => ContainsOp t ~ 'False => OpPresence t
pattern $bOpAbsent :: forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
$mOpAbsent :: forall {r} {t :: T}.
OpPresence t -> ((ContainsOp t ~ 'False) => r) -> (Void# -> r) -> r
OpAbsent = TAbsent
{-# COMPLETE OpPresent, OpAbsent #-}
type ContractPresence (t :: T) = TPresence 'PSContract t
pattern ContractPresent :: () => ContainsContract t ~ 'True => ContractPresence t
pattern $bContractPresent :: forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
$mContractPresent :: forall {r} {t :: T}.
ContractPresence t
-> ((ContainsContract t ~ 'True) => r) -> (Void# -> r) -> r
ContractPresent = TPresent
pattern ContractAbsent :: () => ContainsContract t ~ 'False => ContractPresence t
pattern $bContractAbsent :: forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
$mContractAbsent :: forall {r} {t :: T}.
ContractPresence t
-> ((ContainsContract t ~ 'False) => r) -> (Void# -> r) -> r
ContractAbsent = TAbsent
{-# COMPLETE ContractPresent, ContractAbsent #-}
type TicketPresence (t :: T) = TPresence 'PSTicket t
pattern TicketPresent :: () => ContainsTicket t ~ 'True => TicketPresence t
pattern $bTicketPresent :: forall (t :: T). (ContainsTicket t ~ 'True) => TicketPresence t
$mTicketPresent :: forall {r} {t :: T}.
TicketPresence t
-> ((ContainsTicket t ~ 'True) => r) -> (Void# -> r) -> r
TicketPresent = TPresent
pattern TicketAbsent :: () => ContainsTicket t ~ 'False => TicketPresence t
pattern $bTicketAbsent :: forall (t :: T). (ContainsTicket t ~ 'False) => TicketPresence t
$mTicketAbsent :: forall {r} {t :: T}.
TicketPresence t
-> ((ContainsTicket t ~ 'False) => r) -> (Void# -> r) -> r
TicketAbsent = TAbsent
{-# COMPLETE TicketPresent, TicketAbsent #-}
type BigMapPresence (t :: T) = TPresence 'PSBigMap t
pattern BigMapPresent :: () => ContainsBigMap t ~ 'True => BigMapPresence t
pattern $bBigMapPresent :: forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
$mBigMapPresent :: forall {r} {t :: T}.
BigMapPresence t
-> ((ContainsBigMap t ~ 'True) => r) -> (Void# -> r) -> r
BigMapPresent = TPresent
pattern BigMapAbsent :: () => ContainsBigMap t ~ 'False => BigMapPresence t
pattern $bBigMapAbsent :: forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
$mBigMapAbsent :: forall {r} {t :: T}.
BigMapPresence t
-> ((ContainsBigMap t ~ 'False) => r) -> (Void# -> r) -> r
BigMapAbsent = TAbsent
{-# COMPLETE BigMapPresent, BigMapAbsent #-}
type NestedBigMapsPresence (t :: T) = TPresence 'PSNestedBigMaps t
pattern NestedBigMapsPresent :: () => ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresence t
pattern $bNestedBigMapsPresent :: forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
$mNestedBigMapsPresent :: forall {r} {t :: T}.
NestedBigMapsPresence t
-> ((ContainsNestedBigMaps t ~ 'True) => r) -> (Void# -> r) -> r
NestedBigMapsPresent = TPresent
pattern NestedBigMapsAbsent :: () => ContainsNestedBigMaps t ~ 'False => NestedBigMapsPresence t
pattern $bNestedBigMapsAbsent :: forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
$mNestedBigMapsAbsent :: forall {r} {t :: T}.
NestedBigMapsPresence t
-> ((ContainsNestedBigMaps t ~ 'False) => r) -> (Void# -> r) -> r
NestedBigMapsAbsent = TAbsent
{-# COMPLETE NestedBigMapsPresent, NestedBigMapsAbsent #-}
type SaplingStatePresence (t :: T) = TPresence 'PSSaplingState t
pattern SaplingStatePresent :: () => ContainsSaplingState t ~ 'True => SaplingStatePresence t
pattern $bSaplingStatePresent :: forall (t :: T).
(ContainsSaplingState t ~ 'True) =>
SaplingStatePresence t
$mSaplingStatePresent :: forall {r} {t :: T}.
SaplingStatePresence t
-> ((ContainsSaplingState t ~ 'True) => r) -> (Void# -> r) -> r
SaplingStatePresent = TPresent
pattern SaplingStateAbsent :: () => ContainsSaplingState t ~ 'False => SaplingStatePresence t
pattern $bSaplingStateAbsent :: forall (t :: T).
(ContainsSaplingState t ~ 'False) =>
SaplingStatePresence t
$mSaplingStateAbsent :: forall {r} {t :: T}.
SaplingStatePresence t
-> ((ContainsSaplingState t ~ 'False) => r) -> (Void# -> r) -> r
SaplingStateAbsent = TAbsent
{-# COMPLETE SaplingStatePresent, SaplingStateAbsent #-}
{-# DEPRECATED
OpPresence, OpPresent, OpAbsent
, ContractPresence, ContractPresent, ContractAbsent
, TicketPresence, TicketPresent, TicketAbsent
, BigMapPresence, BigMapPresent, BigMapAbsent
, NestedBigMapsPresence, NestedBigMapsPresent, NestedBigMapsAbsent
, SaplingStatePresence, SaplingStatePresent, SaplingStateAbsent
"Use TPresence instead" #-}
type ProperParameterBetterErrors t =
(SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t)
type ProperStorageBetterErrors t =
(SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t)
type ProperConstantBetterErrors t =
(SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidContract t, ForbidTicket t, ForbidSaplingState t)
type ProperDupableBetterErrors t =
(SingI t, ForbidTicket t)
type ProperPackedValBetterErrors t =
(SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidTicket t, ForbidSaplingState t)
type ProperUnpackedValBetterErrors t =
(ProperPackedValBetterErrors t, ProperConstantBetterErrors t)
type ProperViewableBetterErrors t =
(SingI t, ForbidOp t, ForbidBigMap t, ForbidTicket t)
type ProperUntypedValBetterErrors t =
(SingI t, ForbidOp t)
type ProperNonComparableValBetterErrors t =
(SingI t, ForbidNonComparable t)
{-# DEPRECATED ProperParameterBetterErrors
, ProperStorageBetterErrors
, ProperConstantBetterErrors
, ProperDupableBetterErrors
, ProperPackedValBetterErrors
, ProperUnpackedValBetterErrors
, ProperViewableBetterErrors
, ProperUntypedValBetterErrors
, ProperNonComparableValBetterErrors
"Use *Scope instead"
#-}
checkOpPresence :: Sing (ty :: T) -> TPresence 'PSOp ty
checkOpPresence :: forall (ty :: T). Sing ty -> TPresence 'PSOp ty
checkOpPresence = Sing 'PSOp -> Sing ty -> TPresence 'PSOp ty
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp
checkContractTypePresence :: Sing (ty :: T) -> TPresence 'PSContract ty
checkContractTypePresence :: forall (ty :: T). Sing ty -> TPresence 'PSContract ty
checkContractTypePresence = Sing 'PSContract -> Sing ty -> TPresence 'PSContract ty
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing 'PSContract
SingTPredicateSym 'PSContract
SPSContract
checkTicketPresence :: Sing (ty :: T) -> TPresence 'PSTicket ty
checkTicketPresence :: forall (ty :: T). Sing ty -> TPresence 'PSTicket ty
checkTicketPresence = Sing 'PSTicket -> Sing ty -> TPresence 'PSTicket ty
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing 'PSTicket
SingTPredicateSym 'PSTicket
SPSTicket
checkBigMapPresence :: Sing (ty :: T) -> TPresence 'PSBigMap ty
checkBigMapPresence :: forall (ty :: T). Sing ty -> TPresence 'PSBigMap ty
checkBigMapPresence = Sing 'PSBigMap -> Sing ty -> TPresence 'PSBigMap ty
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing 'PSBigMap
SingTPredicateSym 'PSBigMap
SPSBigMap
checkNestedBigMapsPresence :: Sing (ty :: T) -> TPresence 'PSNestedBigMaps ty
checkNestedBigMapsPresence :: forall (ty :: T). Sing ty -> TPresence 'PSNestedBigMaps ty
checkNestedBigMapsPresence = Sing 'PSNestedBigMaps -> Sing ty -> TPresence 'PSNestedBigMaps ty
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing 'PSNestedBigMaps
SingTPredicateSym 'PSNestedBigMaps
SPSNestedBigMaps
{-# DEPRECATED checkOpPresence, checkContractTypePresence, checkTicketPresence, checkBigMapPresence, checkNestedBigMapsPresence
"Use checkTPresence instead" #-}
opAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidOp t)
opAbsense :: forall (t :: T). Sing t -> Maybe (Dict $ ForbidOp t)
opAbsense = ((ContainsT 'PSOp t :~: 'False) -> Dict $ ForbidOp t)
-> Maybe (ContainsT 'PSOp t :~: 'False)
-> Maybe (Dict $ ForbidOp t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ContainsT 'PSOp t :~: 'False
Refl -> Dict $ ForbidOp t
forall (a :: Constraint). a => Dict a
Dict) (Maybe (ContainsT 'PSOp t :~: 'False) -> Maybe (Dict $ ForbidOp t))
-> (SingT t -> Maybe (ContainsT 'PSOp t :~: 'False))
-> SingT t
-> Maybe (Dict $ ForbidOp t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing 'PSOp -> Sing t -> Maybe (ContainsT 'PSOp t :~: 'False)
forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp
contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidContract t)
contractTypeAbsense :: forall (t :: T). Sing t -> Maybe (Dict $ ForbidContract t)
contractTypeAbsense = ((ContainsT 'PSContract t :~: 'False) -> Dict $ ForbidContract t)
-> Maybe (ContainsT 'PSContract t :~: 'False)
-> Maybe (Dict $ ForbidContract t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ContainsT 'PSContract t :~: 'False
Refl -> Dict $ ForbidContract t
forall (a :: Constraint). a => Dict a
Dict) (Maybe (ContainsT 'PSContract t :~: 'False)
-> Maybe (Dict $ ForbidContract t))
-> (SingT t -> Maybe (ContainsT 'PSContract t :~: 'False))
-> SingT t
-> Maybe (Dict $ ForbidContract t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing 'PSContract
-> Sing t -> Maybe (ContainsT 'PSContract t :~: 'False)
forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence Sing 'PSContract
SingTPredicateSym 'PSContract
SPSContract
bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidBigMap t)
bigMapAbsense :: forall (t :: T). Sing t -> Maybe (Dict $ ForbidBigMap t)
bigMapAbsense = ((ContainsT 'PSBigMap t :~: 'False) -> Dict $ ForbidBigMap t)
-> Maybe (ContainsT 'PSBigMap t :~: 'False)
-> Maybe (Dict $ ForbidBigMap t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ContainsT 'PSBigMap t :~: 'False
Refl -> Dict $ ForbidBigMap t
forall (a :: Constraint). a => Dict a
Dict) (Maybe (ContainsT 'PSBigMap t :~: 'False)
-> Maybe (Dict $ ForbidBigMap t))
-> (SingT t -> Maybe (ContainsT 'PSBigMap t :~: 'False))
-> SingT t
-> Maybe (Dict $ ForbidBigMap t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing 'PSBigMap
-> Sing t -> Maybe (ContainsT 'PSBigMap t :~: 'False)
forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence Sing 'PSBigMap
SingTPredicateSym 'PSBigMap
SPSBigMap
nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidNestedBigMaps t)
nestedBigMapsAbsense :: forall (t :: T). Sing t -> Maybe (Dict $ ForbidNestedBigMaps t)
nestedBigMapsAbsense = ((ContainsT 'PSNestedBigMaps t :~: 'False)
-> Dict $ ForbidNestedBigMaps t)
-> Maybe (ContainsT 'PSNestedBigMaps t :~: 'False)
-> Maybe (Dict $ ForbidNestedBigMaps t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ContainsT 'PSNestedBigMaps t :~: 'False
Refl -> Dict $ ForbidNestedBigMaps t
forall (a :: Constraint). a => Dict a
Dict) (Maybe (ContainsT 'PSNestedBigMaps t :~: 'False)
-> Maybe (Dict $ ForbidNestedBigMaps t))
-> (SingT t -> Maybe (ContainsT 'PSNestedBigMaps t :~: 'False))
-> SingT t
-> Maybe (Dict $ ForbidNestedBigMaps t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing 'PSNestedBigMaps
-> Sing t -> Maybe (ContainsT 'PSNestedBigMaps t :~: 'False)
forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence Sing 'PSNestedBigMaps
SingTPredicateSym 'PSNestedBigMaps
SPSNestedBigMaps
{-# DEPRECATED opAbsense, contractTypeAbsense, bigMapAbsense, nestedBigMapsAbsense
"Use tAbsence instead"
#-}
comparabilityImpliesNoNestedBigMaps
:: forall t. (SingI t, IsComparable t ~ 'True) => ContainsNestedBigMaps t :~: 'False
comparabilityImpliesNoNestedBigMaps :: forall (t :: T).
(SingI t, IsComparable t ~ 'True) =>
ContainsNestedBigMaps t :~: 'False
comparabilityImpliesNoNestedBigMaps = (Stubbed => ContainsT 'PSNestedBigMaps t :~: 'False)
-> ContainsT 'PSNestedBigMaps t :~: 'False
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => ContainsT 'PSNestedBigMaps t :~: 'False)
-> ContainsT 'PSNestedBigMaps t :~: 'False)
-> (Stubbed => ContainsT 'PSNestedBigMaps t :~: 'False)
-> ContainsT 'PSNestedBigMaps t :~: 'False
forall a b. (a -> b) -> a -> b
$ Sing t -> ContainsT 'PSNestedBigMaps t :~: 'False
forall (a :: T).
(IsComparable a ~ 'True) =>
Sing a -> ContainsNestedBigMaps a :~: 'False
go (forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @t)
where
go :: IsComparable a ~ 'True => Sing a -> ContainsNestedBigMaps a :~: 'False
go :: forall (a :: T).
(IsComparable a ~ 'True) =>
Sing a -> ContainsNestedBigMaps a :~: 'False
go = \case
STPair (Sing n1
a :: Sing a) (Sing n2
b :: Sing b) -> case (Sing n1 -> Comparability n1
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n1
a, Sing n2 -> Comparability n2
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n2
b) of
(Comparability n1
CanBeCompared, Comparability n2
CanBeCompared) -> ('False ~ 'False) => 'False :~: 'False
forall {k} (a :: k). a :~: a
Refl (('False ~ 'False) => 'False :~: 'False)
-> (ContainsT 'PSNestedBigMaps n1 :~: 'False) -> 'False :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> ContainsT 'PSNestedBigMaps n1 :~: 'False
forall (a :: T).
(IsComparable a ~ 'True) =>
Sing a -> ContainsNestedBigMaps a :~: 'False
go Sing n1
a (('False ~ 'False) => 'False :~: 'False)
-> (ContainsT 'PSNestedBigMaps n2 :~: 'False) -> 'False :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> ContainsT 'PSNestedBigMaps n2 :~: 'False
forall (a :: T).
(IsComparable a ~ 'True) =>
Sing a -> ContainsNestedBigMaps a :~: 'False
go Sing n2
b
STOr Sing n1
a Sing n2
b -> case (Sing n1 -> Comparability n1
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n1
a, Sing n2 -> Comparability n2
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n2
b) of
(Comparability n1
CanBeCompared, Comparability n2
CanBeCompared) -> ('False ~ 'False) => 'False :~: 'False
forall {k} (a :: k). a :~: a
Refl (('False ~ 'False) => 'False :~: 'False)
-> (ContainsT 'PSNestedBigMaps n1 :~: 'False) -> 'False :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> ContainsT 'PSNestedBigMaps n1 :~: 'False
forall (a :: T).
(IsComparable a ~ 'True) =>
Sing a -> ContainsNestedBigMaps a :~: 'False
go Sing n1
a (('False ~ 'False) => 'False :~: 'False)
-> (ContainsT 'PSNestedBigMaps n2 :~: 'False) -> 'False :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> ContainsT 'PSNestedBigMaps n2 :~: 'False
forall (a :: T).
(IsComparable a ~ 'True) =>
Sing a -> ContainsNestedBigMaps a :~: 'False
go Sing n2
b
STOption Sing n
t -> (ContainsT 'PSNestedBigMaps n ~ 'False) =>
ContainsT 'PSNestedBigMaps n :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT 'PSNestedBigMaps n ~ 'False) =>
ContainsT 'PSNestedBigMaps n :~: 'False)
-> (ContainsT 'PSNestedBigMaps n :~: 'False)
-> ContainsT 'PSNestedBigMaps n :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> ContainsT 'PSNestedBigMaps n :~: 'False
forall (a :: T).
(IsComparable a ~ 'True) =>
Sing a -> ContainsNestedBigMaps a :~: 'False
go Sing n
t
Sing a
SingT a
STNever -> ContainsNestedBigMaps a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STUnit -> ContainsNestedBigMaps a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STInt -> ContainsNestedBigMaps a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STNat -> ContainsNestedBigMaps a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STString -> ContainsNestedBigMaps a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STBytes -> ContainsNestedBigMaps a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STMutez -> ContainsNestedBigMaps a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STBool -> ContainsNestedBigMaps a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STKeyHash -> ContainsNestedBigMaps a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STTimestamp -> ContainsNestedBigMaps a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STAddress -> ContainsNestedBigMaps a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STKey -> ContainsNestedBigMaps a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STSignature -> ContainsNestedBigMaps a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STChainId -> ContainsNestedBigMaps a :~: 'False
forall {k} (a :: k). a :~: a
Refl
comparabilityImpliesNoOp
:: forall t. (SingI t, IsComparable t ~ 'True) => ContainsOp t :~: 'False
comparabilityImpliesNoOp :: forall (t :: T).
(SingI t, IsComparable t ~ 'True) =>
ContainsOp t :~: 'False
comparabilityImpliesNoOp = (Stubbed => ContainsT 'PSOp t :~: 'False)
-> ContainsT 'PSOp t :~: 'False
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => ContainsT 'PSOp t :~: 'False)
-> ContainsT 'PSOp t :~: 'False)
-> (Stubbed => ContainsT 'PSOp t :~: 'False)
-> ContainsT 'PSOp t :~: 'False
forall a b. (a -> b) -> a -> b
$ Sing t -> ContainsT 'PSOp t :~: 'False
forall (a :: T).
(IsComparable a ~ 'True) =>
Sing a -> ContainsOp a :~: 'False
go (forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @t)
where
go :: IsComparable a ~ 'True => Sing a -> ContainsOp a :~: 'False
go :: forall (a :: T).
(IsComparable a ~ 'True) =>
Sing a -> ContainsOp a :~: 'False
go = \case
STPair (Sing n1
a :: Sing a) (Sing n2
b :: Sing b) -> case (Sing n1 -> Comparability n1
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n1
a, Sing n2 -> Comparability n2
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n2
b) of
(Comparability n1
CanBeCompared, Comparability n2
CanBeCompared) -> ('False ~ 'False) => 'False :~: 'False
forall {k} (a :: k). a :~: a
Refl (('False ~ 'False) => 'False :~: 'False)
-> (ContainsT 'PSOp n1 :~: 'False) -> 'False :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> ContainsT 'PSOp n1 :~: 'False
forall (a :: T).
(IsComparable a ~ 'True) =>
Sing a -> ContainsOp a :~: 'False
go Sing n1
a (('False ~ 'False) => 'False :~: 'False)
-> (ContainsT 'PSOp n2 :~: 'False) -> 'False :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> ContainsT 'PSOp n2 :~: 'False
forall (a :: T).
(IsComparable a ~ 'True) =>
Sing a -> ContainsOp a :~: 'False
go Sing n2
b
STOr Sing n1
a Sing n2
b -> case (Sing n1 -> Comparability n1
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n1
a, Sing n2 -> Comparability n2
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n2
b) of
(Comparability n1
CanBeCompared, Comparability n2
CanBeCompared) -> ('False ~ 'False) => 'False :~: 'False
forall {k} (a :: k). a :~: a
Refl (('False ~ 'False) => 'False :~: 'False)
-> (ContainsT 'PSOp n1 :~: 'False) -> 'False :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> ContainsT 'PSOp n1 :~: 'False
forall (a :: T).
(IsComparable a ~ 'True) =>
Sing a -> ContainsOp a :~: 'False
go Sing n1
a (('False ~ 'False) => 'False :~: 'False)
-> (ContainsT 'PSOp n2 :~: 'False) -> 'False :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> ContainsT 'PSOp n2 :~: 'False
forall (a :: T).
(IsComparable a ~ 'True) =>
Sing a -> ContainsOp a :~: 'False
go Sing n2
b
STOption Sing n
t -> (ContainsT 'PSOp n ~ 'False) => ContainsT 'PSOp n :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT 'PSOp n ~ 'False) => ContainsT 'PSOp n :~: 'False)
-> (ContainsT 'PSOp n :~: 'False) -> ContainsT 'PSOp n :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> ContainsT 'PSOp n :~: 'False
forall (a :: T).
(IsComparable a ~ 'True) =>
Sing a -> ContainsOp a :~: 'False
go Sing n
t
Sing a
SingT a
STNever -> ContainsOp a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STUnit -> ContainsOp a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STInt -> ContainsOp a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STNat -> ContainsOp a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STString -> ContainsOp a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STBytes -> ContainsOp a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STMutez -> ContainsOp a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STBool -> ContainsOp a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STKeyHash -> ContainsOp a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STTimestamp -> ContainsOp a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STAddress -> ContainsOp a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STKey -> ContainsOp a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STSignature -> ContainsOp a :~: 'False
forall {k} (a :: k). a :~: a
Refl
Sing a
SingT a
STChainId -> ContainsOp a :~: 'False
forall {k} (a :: k). a :~: a
Refl
{-# DEPRECATED comparabilityImpliesNoNestedBigMaps, comparabilityImpliesNoOp
"Already implied by Comparable constraint" #-}
getComparableProofS :: Sing (a :: T) -> Maybe (Dict (Comparable a))
getComparableProofS :: forall (a :: T). Sing a -> Maybe (Dict (Comparable a))
getComparableProofS = Sing a -> Maybe (Dict (Comparable a))
forall (a :: T). Sing a -> Maybe (Dict (Comparable a))
comparabilityPresence
{-# DEPRECATED getComparableProofS "Use comparabilityPresence" #-}
type IsComparable t = Not (ContainsT 'PSNonComparable t)
{-# DEPRECATED IsComparable "Use 'Not (ContainsT PSNonComparable t)' instead" #-}