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

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

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

Michelson have multiple restrictions on values, examples:

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

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

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

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

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

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

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

-}

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

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

  , IsDupableScope

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

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

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

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

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

  , Comparability(..)
  , checkComparability
  , getComparableProofS

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

import Data.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(..))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | This is like 'HasNoOp', it raises a more human-readable error
-- when @t@ type is concrete, but GHC cannot make any conclusions
-- from such constraint as it can for 'HasNoOp'.
-- Though, hopefully, it will someday:
-- <https://gitlab.haskell.org/ghc/ghc/issues/11503 #11503>.
--
-- Use this constraint in our eDSL.
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)

-- | Constraint that rises human-readable error message, in case given value
-- can't be compared
type ForbidNonComparable t = FailOnNonComparableFound (IsComparable t)

-- | Evidence of that 'HasNoOp' is deducable from 'ForbidOp'.
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
$
  -- It's not clear now to proof GHC that @HasNoOp t@ is implication of
  -- @ForbidOp t@, so we use @error@ below and also disable
  -- "-Wredundant-constraints" extension.
  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"

-- | Reify 'HasNoOp' contraint from 'ForbidOp'.
--
-- Left for backward compatibility.
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

-- | Reify 'HasNoContract' contraint from 'ForbidContract'.
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"

-- | Reify 'HasNoContract' contraint from 'ForbidContract'.
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

-- | Reify 'HasNoTicket' contraint from 'ForbidTicket'.
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"

-- | Reify 'HasNoSaplingState' contraint from 'ForbidSaplingState'.
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"

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

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

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

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

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

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

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

-- | Check at runtime whether a value of the given type _may_ contain an operation.
checkOpPresence :: Sing (ty :: T) -> OpPresence ty
checkOpPresence :: Sing ty -> OpPresence ty
checkOpPresence = \case
  -- This is a sad amount of boilerplate, but at least
  -- there is no chance to make a mistake in it.
  -- We can't do in a simpler way while requiring only @Sing ty@ / @SingI ty@,
  -- and a more complex constraint would be too unpleasant and confusing to
  -- propagate everywhere.
  Sing ty
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

-- | Check at runtime whether a value of the given type _may_ contain a @contract@ value.
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  -- contract type is not allowed in tickets at all
  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

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

-- | Check at runtime whether a value of the given type _may_ contain a @big_map@ value.
checkBigMapPresence :: Sing (ty :: T) -> BigMapPresence ty
checkBigMapPresence :: Sing ty -> BigMapPresence ty
checkBigMapPresence = \case
  -- More boilerplate to boilerplate god.
  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  -- big_maps are not allowed in tickets at all
  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

-- | Check at runtime whether a value of the given type _may_ contain nested @big_map@s.
checkNestedBigMapsPresence :: Sing (ty :: T) -> NestedBigMapsPresence ty
checkNestedBigMapsPresence :: Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence = \case
  -- More boilerplate to boilerplate god.
  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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance SingI t => CheckScope (WellTyped t) where
  checkScope :: Either BadTypeForScope (Dict (WellTyped t))
checkScope = (NotWellTyped -> BadTypeForScope)
-> Either NotWellTyped (Dict (WellTyped t))
-> Either BadTypeForScope (Dict (WellTyped t))
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first NotWellTyped -> BadTypeForScope
nwtCause (Either NotWellTyped (Dict (WellTyped t))
 -> Either BadTypeForScope (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
-> Either BadTypeForScope (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ 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

-- | Alias for comparable types.
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)

-- | Allows using a scope that can be proven true with a De Morgan law.
--
-- Many scopes are defined as @not a@ (or rather @a ~ 'False@) where @a@ is a
-- negative property we want to avoid as a 'Constraint'.
-- The negative constraints are implemented with a type family that for some
-- combination types resolves to itself applied to the type arguments in an @or@,
-- e.g. A @pair l r@ has @x@ if @l@ or @r@ contain @x@.
--
-- Because of the De Morgan laws @not (a or b)@ implies @(not a) and (not b)@
-- or in our case: @pair@ does not contain @x@ -> @a@ and @b@ don't contain @x@.
--
-- GHC is however not able to prove this, so we need to use another (impossible)
-- 'error' to forcefully "prove" one of the two scopes.
-- Funnily enough however GHC is able to prove that if one holds then the other
-- does too, so we don't actually have to prove both, see 'mkWithDeMorgan'.
class WithDeMorganScope (c :: T -> Constraint) t a b where
  withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret

-- | Helper to builds a 'WithDeMorganScope' by using a 'CheckScope' that we know
-- cannot fail.
--
-- This can be used to make instances that also prove the other side of a
-- negative @or-like@ scope constraint, see 'WithDeMorganScope'.
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

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

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

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

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

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

type ProperDupableBetterErrors t =
  (SingI t, ForbidTicket t)

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

type ProperUnpackedValBetterErrors t =
  (ProperPackedValBetterErrors t, ProperConstantBetterErrors t)

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

type ProperUntypedValBetterErrors t =
  (SingI t, ForbidOp t)

type ProperNonComparableValBetterErrors t =
  (SingI t, ForbidNonComparable t)

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
  -- | Constraints required for instance of a given type.
  type ComparableSuperC t :: Constraint
  type ComparableSuperC _ = ()

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

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

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

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

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

instance WellTyped 'TKey
instance WellTyped 'TUnit
instance WellTyped 'TNever
instance WellTyped 'TSignature
instance WellTyped 'TChainId
instance WellTyped 'TChest 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)

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

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

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

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

-- | Version of 'getWTP' that accepts 'Sing' at term-level.
getWTP' :: Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' :: 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