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

{-# 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)

-- | Whether a value of this type _may_ contain an operation.
--
-- In some scopes (constants, parameters, storage) appearing for operation type
-- is prohibited.
-- Operations in input/output of lambdas are allowed without limits though.
type ContainsOp t = ContainsT 'PSOp t

-- | Whether a value of this type _may_ contain a @contract@ value.
--
-- In some scopes (constants, storage) appearing for contract type
-- is prohibited.
-- Contracts in input/output of lambdas are allowed without limits though.
type ContainsContract t = ContainsT 'PSContract t

-- | Whether a value of this type _may_ contain a @ticket@ value.
type ContainsTicket t = ContainsT 'PSTicket t

-- | Whether a value of this type _may_ contain a @big_map@ value.
type ContainsBigMap t = ContainsT 'PSBigMap t

-- | Whether a value of this type _may_ contain nested @big_map@s.
--
-- Nested big_maps (i.e. big_map which contains another big_map inside of it's value type) are
-- prohibited in all contexts. Some context such as PUSH, APPLY, PACK/UNPACK instructions are more
-- strict because they don't work with big_map at all.
type ContainsNestedBigMaps t = ContainsT 'PSNestedBigMaps t

-- | Whether a value of this type _may_ contain a @samping_state@ value.
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"
  #-}


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

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

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

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

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

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

{-# DEPRECATED HasNoOp, HasNoContract, HasNoTicket, HasNoBigMap, HasNoSaplingState, HasNoNestedBigMaps
  "Use Forbid* instead" #-}


-- | Whether a value of this type _may_ contain an operation.
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 #-}

-- | Whether a value of this type _may_ contain a @contract@ value.
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 #-}

-- | Whether a value of this type _may_ contain a @ticket@ value.
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 #-}

-- | Whether a value of this type _may_ contain a @big_map@ value.
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 #-}

-- | Whether a value of this type _may_ contain nested @big_map@s.
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 #-}

-- | Whether a value of this type _may_ contain a @sapling_state@ value.
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"
  #-}

-- | Check at runtime whether a value of the given type _may_ contain an operation.
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

-- | Check at runtime whether a value of the given type _may_ contain a @contract@ value.
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

-- | Check at runtime whether a value of the given type _may_ contain a @ticket@ value.
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

-- | Check at runtime whether a value of the given type _may_ contain a @big_map@ value.
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

-- | Check at runtime whether a value of the given type _may_ contain nested @big_map@s.
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" #-}

-- | Check at runtime that a value of the given type cannot contain operations.
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

-- | Check at runtime that a value of the given type cannot contain @contract@ values.
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

-- | Check at runtime that a value of the given type cannot containt @big_map@ values
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

-- | Check at runtime that a value of the given type cannot contain nested @big_map@s.
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"
 #-}

-- | Inductive proof that 'Comparable' implies 'HasNoNestedBigMaps'. This is
-- stubbed with an @unsafeCoerce Refl@ at runtime to avoid runtime traversals.
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

-- | Inductive proof that 'Comparable' implies 'HasNoOp'. This is
-- stubbed with an @unsafeCoerce Refl@ at runtime to avoid runtime traversals.
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" #-}