content: {-# LANGUAGE UndecidableSuperClasses, FunctionalDependencies, RoleAnnotations, ExplicitNamespaces, TypeFamilies, RankNTypes, TypeApplications, LambdaCase, DerivingStrategies, ScopedTypeVariables, TypeOperators, DataKinds, PolyKinds, GADTs, TypeFamilyDependencies, ConstraintKinds, UndecidableInstances, TypeSynonymInstances, FlexibleInstances, DeriveGeneric, AllowAmbiguousTypes, StrictData #-}
  {-# OPTIONS_GHC -Wno-redundant-constraints -fforce-recomp -Wincomplete-patterns #-}
  
  {- | 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 T18478
    ( -- * Scopes
      ConstantScope
    , StorageScope
    , PackedValScope
    , ParameterScope
    , PrintedValScope
    , UnpackedValScope
  
    , ProperParameterBetterErrors
    , ProperStorageBetterErrors
    , ProperConstantBetterErrors
    , ProperPackedValBetterErrors
    , ProperUnpackedValBetterErrors
    , ProperPrintedValBetterErrors
  
    , properParameterEvi
    , properStorageEvi
    , properConstantEvi
    , properPackedValEvi
    , properUnpackedValEvi
    , properPrintedValEvi
    , (:-)(..)
  
    , BadTypeForScope (..)
    , CheckScope (..)
  
      -- * Implementation internals
    , HasNoBigMap
    , HasNoNestedBigMaps
    , HasNoOp
    , HasNoContract
    , ContainsBigMap
    , ContainsNestedBigMaps
  
    , ForbidOp
    , ForbidContract
    , ForbidBigMap
    , ForbidNestedBigMaps
    , FailOnBigMapFound
    , FailOnNestedBigMapsFound
    , FailOnOperationFound
  
    , OpPresence (..)
    , ContractPresence (..)
    , BigMapPresence (..)
    , NestedBigMapsPresence (..)
    , checkOpPresence
    , checkContractTypePresence
    , checkBigMapPresence
    , checkNestedBigMapsPresence
    , opAbsense
    , contractTypeAbsense
    , bigMapAbsense
    , nestedBigMapsAbsense
    , forbiddenOp
    , forbiddenContractType
    , forbiddenBigMap
    , forbiddenNestedBigMaps
  
      -- * Re-exports
    , withDict
    , SingI (..)
    ) where
  
  import Data.Type.Bool (type (||))
  import Data.Type.Coercion
  import GHC.TypeLits (ErrorMessage(..), TypeError)
  import Data.Typeable
  import GHC.Generics
  import GHC.Exts hiding (withDict)
  import Data.Kind
  
  data T =
      TKey
    | TUnit
    | TSignature
    | TChainId
    | TOption T
    | TList T
    | TSet T
    | TOperation
    | TContract T
    | TPair T T
    | TOr T T
    | TLambda T T
    | TMap T T
    | TBigMap T T
    | TInt
    | TNat
    | TString
    | TBytes
    | TMutez
    | TBool
    | TKeyHash
    | TTimestamp
    | TAddress
    deriving stock (Eq, Show)
  
  type family Sing :: k -> Type
  
  class SingI a where
    sing :: Sing a
  
  class SingKind (k :: Type) where
    -- | Get a base type from the promoted kind. For example,
    -- @Demote Bool@ will be the type @Bool@. Rarely, the type and kind do not
    -- match. For example, @Demote Nat@ is @Natural@.
    type Demote k = (r :: Type) | r -> k
  
    -- | Convert a singleton to its unrefined version.
    fromSing :: Sing (a :: k) -> Demote k
  
    -- | Convert an unrefined type to an existentially-quantified singleton type.
    toSing   :: Demote k -> SomeSing k
  
  data SomeSing (k :: Type) :: Type where
    SomeSing :: Sing (a :: k) -> SomeSing k
  
  
  -- | Instance of data family 'Sing' for 'T'.
  -- Custom instance is implemented in order to inject 'Typeable'
  -- constraint for some of constructors.
  data SingT :: T -> Type where
    STKey :: SingT  'TKey
    STUnit :: SingT  'TUnit
    STSignature :: SingT  'TSignature
    STChainId :: SingT  'TChainId
    STOption :: (SingI a, Typeable a) => Sing a -> SingT ( 'TOption a)
    STList :: (SingI a, Typeable a) => Sing a -> SingT ( 'TList a )
    STSet :: (SingI a, Typeable a) => Sing a -> SingT ( 'TSet a )
    STOperation  :: SingT 'TOperation
    STContract   :: (SingI a, Typeable a)
                  => Sing a -> SingT ( 'TContract a )
    STPair       :: (SingI a, SingI b, Typeable a, Typeable b)
                  => Sing a -> Sing b -> SingT ('TPair a b)
    STOr         :: (SingI a, SingI b, Typeable a, Typeable b)
                  => Sing a -> Sing b -> SingT ('TOr a b)
    STLambda     :: (SingI a, SingI b, Typeable a, Typeable b)
                  => Sing a -> Sing b -> SingT ('TLambda a b)
    STMap        :: (SingI a, SingI b, Typeable a, Typeable b)
                  => Sing a -> Sing b -> SingT ('TMap a b)
    STBigMap    :: (SingI a, SingI b, Typeable a, Typeable b)
                  => Sing a -> Sing b -> SingT ('TBigMap a b)
    STInt :: SingT  'TInt
    STNat :: SingT  'TNat
    STString :: SingT  'TString
    STBytes :: SingT  'TBytes
    STMutez :: SingT  'TMutez
    STBool :: SingT  'TBool
    STKeyHash :: SingT  'TKeyHash
    STTimestamp :: SingT  'TTimestamp
    STAddress :: SingT  'TAddress
  
  type instance Sing = SingT
  
  ---------------------------------------------
  -- Singleton-related helpers for T
  --------------------------------------------
  
  -- | Version of 'SomeSing' with 'Typeable' constraint,
  -- specialized for use with 'T' kind.
  data SomeSingT where
    SomeSingT :: forall (a :: T). (Typeable a, SingI a)
              => Sing a -> SomeSingT
  
  -- | Version of 'withSomeSing' with 'Typeable' constraint
  -- provided to processing function.
  --
  -- Required for not to erase these useful constraints when doing
  -- conversion from value of type 'T' to its singleton representation.
  withSomeSingT
    :: T
    -> (forall (a :: T). (Typeable a, SingI a) => Sing a -> r)
    -> r
  withSomeSingT t f = (\(SomeSingT s) -> f s) (toSingT t)
  
  -- | Version of 'fromSing' specialized for use with
  -- @data instance Sing :: T -> Type@ which requires 'Typeable'
  -- constraint for some of its constructors
  fromSingT :: Sing (a :: T) -> T
  fromSingT = \case
    STKey -> TKey
    STUnit -> TUnit
    STSignature -> TSignature
    STChainId -> TChainId
    STOption t -> TOption (fromSingT t)
    STList t -> TList (fromSingT t)
    STSet t -> TSet (fromSingT t)
    STOperation -> TOperation
    STContract t -> TContract (fromSingT t)
    STPair a b -> TPair (fromSingT a) (fromSingT b)
    STOr a b -> TOr (fromSingT a) (fromSingT b)
    STLambda a b -> TLambda (fromSingT a) (fromSingT b)
    STMap a b -> TMap (fromSingT a) (fromSingT b)
    STBigMap a b -> TBigMap (fromSingT a) (fromSingT b)
    STInt -> TInt
    STNat -> TNat
    STString -> TString
    STBytes -> TBytes
    STMutez -> TMutez
    STBool -> TBool
    STKeyHash -> TKeyHash
    STTimestamp -> TTimestamp
    STAddress -> TAddress
  
  -- | Version of 'toSing' which creates 'SomeSingT'.
  toSingT :: T -> SomeSingT
  toSingT = \case
    TKey -> SomeSingT STKey
    TUnit -> SomeSingT STUnit
    TSignature -> SomeSingT STSignature
    TChainId -> SomeSingT STChainId
    TOption t -> withSomeSingT t $ \tSing -> SomeSingT $ STOption tSing
    TList t -> withSomeSingT t $ \tSing -> SomeSingT $ STList tSing
    TSet ct -> withSomeSingT ct $ \ctSing -> SomeSingT $ STSet ctSing
    TOperation -> SomeSingT STOperation
    TContract t -> withSomeSingT t $ \tSing -> SomeSingT $ STContract tSing
    TPair l r ->
      withSomeSingT l $ \lSing ->
      withSomeSingT r $ \rSing ->
        SomeSingT $ STPair lSing rSing
    TOr l r ->
      withSomeSingT l $ \lSing ->
      withSomeSingT r $ \rSing ->
        SomeSingT $ STOr lSing rSing
    TLambda l r ->
      withSomeSingT l $ \lSing ->
      withSomeSingT r $ \rSing ->
        SomeSingT $ STLambda lSing rSing
    TMap l r ->
      withSomeSingT l $ \lSing ->
      withSomeSingT r $ \rSing ->
        SomeSingT $ STMap lSing rSing
    TBigMap l r ->
      withSomeSingT l $ \lSing ->
      withSomeSingT r $ \rSing ->
        SomeSingT $ STBigMap lSing rSing
    TInt -> SomeSingT STInt
    TNat -> SomeSingT STNat
    TString -> SomeSingT STString
    TBytes -> SomeSingT STBytes
    TMutez -> SomeSingT STMutez
    TBool -> SomeSingT STBool
    TKeyHash -> SomeSingT STKeyHash
    TTimestamp -> SomeSingT STTimestamp
    TAddress -> SomeSingT STAddress
  
  instance SingKind T where
    type Demote T = T
    fromSing  = fromSingT
    toSing t = case toSingT t of SomeSingT s -> SomeSing s
  
  instance SingI  'TKey where
    sing = STKey
  instance SingI  'TUnit where
    sing = STUnit
  instance SingI  'TSignature where
    sing = STSignature
  instance SingI  'TChainId where
    sing = STChainId
  instance (SingI a, Typeable a) => SingI ( 'TOption (a :: T)) where
    sing = STOption sing
  instance (SingI a, Typeable a) => SingI ( 'TList (a :: T)) where
    sing = STList sing
  instance (SingI a, Typeable a) => SingI ( 'TSet (a :: T)) where
    sing = STSet sing
  instance SingI 'TOperation where
    sing = STOperation
  instance (SingI a, Typeable a) =>
            SingI ( 'TContract (a :: T)) where
    sing = STContract sing
  instance (SingI a, Typeable a, Typeable b, SingI b) =>
            SingI ( 'TPair a b) where
    sing = STPair sing sing
  instance (SingI a, Typeable a, Typeable b, SingI b) =>
            SingI ( 'TOr a b) where
    sing = STOr sing sing
  instance (SingI a, Typeable a, Typeable b, SingI b) =>
            SingI ( 'TLambda a b) where
    sing = STLambda sing sing
  instance (SingI a, Typeable a, Typeable b, SingI b) =>
            SingI ( 'TMap a b) where
    sing = STMap sing sing
  instance (SingI a, Typeable a, Typeable b, SingI b) =>
            SingI ( 'TBigMap a b) where
    sing = STBigMap sing sing
  instance SingI  'TInt where
    sing = STInt
  instance SingI  'TNat where
    sing = STNat
  instance SingI  'TString where
    sing = STString
  instance SingI  'TBytes where
    sing = STBytes
  instance SingI  'TMutez where
    sing = STMutez
  instance SingI  'TBool where
    sing = STBool
  instance SingI  'TKeyHash where
    sing = STKeyHash
  instance SingI  'TTimestamp where
    sing = STTimestamp
  instance SingI  'TAddress where
    sing = STAddress
  
  data Dict :: Constraint -> Type where
    Dict :: a => Dict a
    deriving Typeable
  
  withDict :: HasDict c e => e -> (c => r) -> r
  withDict d r = case evidence d of
    Dict -> r
  
  class HasDict c e | e -> c where
    evidence :: e -> Dict c
  
  instance HasDict a (Dict a) where
    evidence = Prelude.id
  
  instance a => HasDict b (a :- b) where
    evidence (Sub x) = x
  
  instance HasDict (Coercible a b) (Coercion a b) where
    evidence Coercion = Dict
  
  instance HasDict (a ~ b) (a :~: b) where
    evidence Refl = Dict
  
  infixl 1 \\ -- required comment
  
  (\\) :: HasDict c e => (c => r) -> e -> r
  r \\ d = withDict d r
  infixr 9 :-
  newtype a :- b = Sub (a => Dict b)
    deriving Typeable
  type role (:-) nominal nominal
  (***) :: (a :- b) -> (c :- d) -> (a, c) :- (b, d)
  f *** g = Sub $ Dict \\ f \\ g
  
  type f $ a = f a
  infixr 2 $
  
  maybeToRight a Nothing = Left a
  maybeToRight _ (Just a) = Right a
  
  ----------------------------------------------------------------------------
  -- Constraints
  ----------------------------------------------------------------------------
  -- | Whether this type contains 'TOperation' type.
  --
  -- 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 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 this type contains 'TContract' type.
  --
  -- 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 this type contains 'TBigMap' type.
  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 t) = ContainsBigMap t
    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 this type contains a type with nested 'TBigMap'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 doesn'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 t) = ContainsNestedBigMaps t
    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
  
  -- | Constraint which ensures that operation type does not appear in a given type.
  --
  -- 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 contract type does not appear in a given type.
  class (ContainsContract t ~ 'False) => HasNoContract t
  instance (ContainsContract t ~ 'False) => HasNoContract t
  
  -- | Constraint which ensures that bigmap does not appear in a given type.
  class (ContainsBigMap t ~ 'False) => HasNoBigMap t
  instance (ContainsBigMap t ~ 'False) => HasNoBigMap 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 '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 = ()
  
  -- | This is like 'HasNoOp', but raises a more human-readable error
  -- when the @t@ type is concrete.
  --
  -- Use this constraint in our eDSL.
  type ForbidOp t = FailOnOperationFound (ContainsOp t)
  
  type ForbidContract t = FailOnContractFound (ContainsContract t)
  
  type ForbidBigMap t = FailOnBigMapFound (ContainsBigMap t)
  
  type ForbidNestedBigMaps t = FailOnNestedBigMapsFound (ContainsNestedBigMaps t)
  
  -- | Evidence of that 'HasNoOp' is deducable from 'ForbidOp'.
  forbiddenOpEvi :: forall t. (SingI t, ForbidOp t) :- HasNoOp t
  forbiddenOpEvi = Sub $
    case checkOpPresence (sing @t) of
      OpAbsent -> Dict
  
  -- | Reify 'HasNoOp' constraint from 'ForbidOp'.
  --
  -- Left for backward compatibility.
  forbiddenOp
    :: forall t a.
       (SingI t, ForbidOp t)
    => (HasNoOp t => a)
    -> a
  forbiddenOp = withDict $ forbiddenOpEvi @t
  
  forbiddenBigMapEvi :: forall t. (SingI t, ForbidBigMap t) :- HasNoBigMap t
  forbiddenBigMapEvi = Sub $
    case checkBigMapPresence (sing @t) of
      BigMapAbsent -> Dict
  
  forbiddenNestedBigMapsEvi :: forall t. (SingI t, ForbidNestedBigMaps t) :- HasNoNestedBigMaps t
  forbiddenNestedBigMapsEvi = Sub $
    case checkNestedBigMapsPresence (sing @t) of
      NestedBigMapsAbsent -> Dict
  
  forbiddenBigMap
    :: forall t a.
       (SingI t, ForbidBigMap t)
    => (HasNoBigMap t => a)
    -> a
  forbiddenBigMap = withDict $ forbiddenBigMapEvi @t
  
  forbiddenNestedBigMaps
    :: forall t a.
       (SingI t, ForbidNestedBigMaps t)
    => (HasNoNestedBigMaps t => a)
    -> a
  forbiddenNestedBigMaps = withDict $ forbiddenNestedBigMapsEvi @t
  
  -- | Reify 'HasNoContract' constraint from 'ForbidContract'.
  forbiddenContractTypeEvi
    :: forall t. (SingI t, ForbidContract t) :- HasNoContract t
  forbiddenContractTypeEvi = Sub $
    case checkContractTypePresence (sing @t) of
      ContractAbsent -> Dict
  
  -- | Reify 'HasNoContract' constraint from 'ForbidContract'.
  forbiddenContractType
    :: forall t a.
       (SingI t, ForbidContract t)
    => (HasNoContract t => a)
    -> a
  forbiddenContractType = withDict $ forbiddenContractTypeEvi @t
  
  -- | Whether the type contains 'TOperation', with proof.
  data OpPresence (t :: T)
    = ContainsOp t ~ 'True => OpPresent
    | ContainsOp t ~ 'False => OpAbsent
  
  data ContractPresence (t :: T)
    = ContainsContract t ~ 'True => ContractPresent
    | ContainsContract t ~ 'False => ContractAbsent
  
  data BigMapPresence (t :: T)
    = ContainsBigMap t ~ 'True => BigMapPresent
    | ContainsBigMap t ~ 'False => BigMapAbsent
  
  data NestedBigMapsPresence (t :: T)
    = ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresent
    | ContainsNestedBigMaps t ~ 'False => NestedBigMapsAbsent
  
  -- @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 the given type contains 'TOperation'.
  checkOpPresence :: Sing (ty :: T) -> 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.
    STKey -> OpAbsent
    STSignature -> OpAbsent
    STChainId -> OpAbsent
    STUnit -> OpAbsent
    STOption t -> case checkOpPresence t of
      OpPresent -> OpPresent
      OpAbsent -> OpAbsent
    STList t -> case checkOpPresence t of
      OpPresent -> OpPresent
      OpAbsent -> OpAbsent
    STSet a -> case checkOpPresence a of
      OpPresent -> OpPresent
      OpAbsent -> OpAbsent
    STOperation -> OpPresent
    STContract t -> case checkOpPresence t of
      OpPresent -> OpPresent
      OpAbsent -> OpAbsent
    STPair a b -> case (checkOpPresence a, checkOpPresence b) of
      (OpPresent, _) -> OpPresent
      (_, OpPresent) -> OpPresent
      (OpAbsent, OpAbsent) -> OpAbsent
    STOr a b -> case (checkOpPresence a, checkOpPresence b) of
      (OpPresent, _) -> OpPresent
      (_, OpPresent) -> OpPresent
      (OpAbsent, OpAbsent) -> OpAbsent
    STLambda _ _ -> OpAbsent
    STMap k v -> case (checkOpPresence k, checkOpPresence v) of
      (OpAbsent, OpAbsent) -> OpAbsent
      (OpPresent, _) -> OpPresent
      (_, OpPresent) -> OpPresent
    STBigMap k v -> case (checkOpPresence k, checkOpPresence v) of
      (OpAbsent, OpAbsent) -> OpAbsent
      (OpPresent, _) -> OpPresent
      (_, OpPresent) -> OpPresent
    STInt -> OpAbsent
    STNat -> OpAbsent
    STString -> OpAbsent
    STBytes -> OpAbsent
    STMutez -> OpAbsent
    STBool -> OpAbsent
    STKeyHash -> OpAbsent
    STTimestamp -> OpAbsent
    STAddress -> OpAbsent
  
  -- | Check at runtime whether the given type contains 'TContract'.
  checkContractTypePresence :: Sing (ty :: T) -> ContractPresence ty
  checkContractTypePresence = \case
    STKey -> ContractAbsent
    STSignature -> ContractAbsent
    STChainId -> ContractAbsent
    STUnit -> ContractAbsent
    STOption t -> case checkContractTypePresence t of
      ContractPresent -> ContractPresent
      ContractAbsent -> ContractAbsent
    STList t -> case checkContractTypePresence t of
      ContractPresent -> ContractPresent
      ContractAbsent -> ContractAbsent
    STSet _ -> ContractAbsent
    STOperation -> ContractAbsent
    STContract _ -> ContractPresent
    STPair a b -> case (checkContractTypePresence a, checkContractTypePresence b) of
      (ContractPresent, _) -> ContractPresent
      (_, ContractPresent) -> ContractPresent
      (ContractAbsent, ContractAbsent) -> ContractAbsent
    STOr a b -> case (checkContractTypePresence a, checkContractTypePresence b) of
      (ContractPresent, _) -> ContractPresent
      (_, ContractPresent) -> ContractPresent
      (ContractAbsent, ContractAbsent) -> ContractAbsent
    STLambda _ _ -> ContractAbsent
    STMap _ v -> case checkContractTypePresence v of
      ContractPresent -> ContractPresent
      ContractAbsent -> ContractAbsent
    STBigMap _ v -> case checkContractTypePresence v of
      ContractPresent -> ContractPresent
      ContractAbsent -> ContractAbsent
    STInt -> ContractAbsent
    STNat -> ContractAbsent
    STString -> ContractAbsent
    STBytes -> ContractAbsent
    STMutez -> ContractAbsent
    STBool -> ContractAbsent
    STKeyHash -> ContractAbsent
    STTimestamp -> ContractAbsent
    STAddress -> ContractAbsent
  
  -- | Check at runtime whether the given type contains 'TBigMap'.
  checkBigMapPresence :: Sing (ty :: T) -> BigMapPresence ty
  checkBigMapPresence = \case
    -- More boilerplate to boilerplate god.
    STKey -> BigMapAbsent
    STSignature -> BigMapAbsent
    STChainId -> BigMapAbsent
    STUnit -> BigMapAbsent
    STOption t -> case checkBigMapPresence t of
      BigMapPresent -> BigMapPresent
      BigMapAbsent -> BigMapAbsent
    STList t -> case checkBigMapPresence t of
      BigMapPresent -> BigMapPresent
      BigMapAbsent -> BigMapAbsent
    STSet _ -> BigMapAbsent
    STOperation -> BigMapAbsent
    STContract t -> case checkBigMapPresence t of
      BigMapPresent -> BigMapPresent
      BigMapAbsent -> BigMapAbsent
    STPair a b -> case (checkBigMapPresence a, checkBigMapPresence b) of
      (BigMapPresent, _) -> BigMapPresent
      (_, BigMapPresent) -> BigMapPresent
      (BigMapAbsent, BigMapAbsent) -> BigMapAbsent
    STOr a b -> case (checkBigMapPresence a, checkBigMapPresence b) of
      (BigMapPresent, _) -> BigMapPresent
      (_, BigMapPresent) -> BigMapPresent
      (BigMapAbsent, BigMapAbsent) -> BigMapAbsent
    STLambda _ _ -> BigMapAbsent
    STMap _ v -> case checkBigMapPresence v of
      BigMapPresent -> BigMapPresent
      BigMapAbsent -> BigMapAbsent
    STBigMap _ _ ->
      BigMapPresent
    STInt -> BigMapAbsent
    STNat -> BigMapAbsent
    STString -> BigMapAbsent
    STBytes -> BigMapAbsent
    STMutez -> BigMapAbsent
    STBool -> BigMapAbsent
    STKeyHash -> BigMapAbsent
    STTimestamp -> BigMapAbsent
    STAddress -> BigMapAbsent
  
  -- | Check at runtime whether the given type contains 'TBigMap'.
  checkNestedBigMapsPresence :: Sing (ty :: T) -> NestedBigMapsPresence ty
  checkNestedBigMapsPresence = \case
    -- More boilerplate to boilerplate god.
    STKey -> NestedBigMapsAbsent
    STSignature -> NestedBigMapsAbsent
    STChainId -> NestedBigMapsAbsent
    STUnit -> NestedBigMapsAbsent
    STOption t -> case checkNestedBigMapsPresence t of
      NestedBigMapsPresent -> NestedBigMapsPresent
      NestedBigMapsAbsent -> NestedBigMapsAbsent
    STList                   t -> case checkNestedBigMapsPresence t of
      NestedBigMapsPresent -> NestedBigMapsPresent
      NestedBigMapsAbsent -> NestedBigMapsAbsent
    STSet _ -> NestedBigMapsAbsent
    STOperation -> NestedBigMapsAbsent
    STContract t -> case checkNestedBigMapsPresence t of
      NestedBigMapsPresent -> NestedBigMapsPresent
      NestedBigMapsAbsent -> NestedBigMapsAbsent
    STPair a b -> case (checkNestedBigMapsPresence a, checkNestedBigMapsPresence b) of
      (NestedBigMapsPresent, _) -> NestedBigMapsPresent
      (_, NestedBigMapsPresent) -> NestedBigMapsPresent
      (NestedBigMapsAbsent, NestedBigMapsAbsent) -> NestedBigMapsAbsent
    STOr a b -> case (checkNestedBigMapsPresence a, checkNestedBigMapsPresence b) of
      (NestedBigMapsPresent, _) -> NestedBigMapsPresent
      (_, NestedBigMapsPresent) -> NestedBigMapsPresent
      (NestedBigMapsAbsent, NestedBigMapsAbsent) -> NestedBigMapsAbsent
    STLambda _ _ -> NestedBigMapsAbsent
    STMap _ v -> case checkNestedBigMapsPresence v of
      NestedBigMapsPresent -> NestedBigMapsPresent
      NestedBigMapsAbsent -> NestedBigMapsAbsent
    STBigMap _ v -> case checkBigMapPresence v of
      BigMapPresent -> NestedBigMapsPresent
      BigMapAbsent -> NestedBigMapsAbsent
    STInt -> NestedBigMapsAbsent
    STNat -> NestedBigMapsAbsent
    STString -> NestedBigMapsAbsent
    STBytes -> NestedBigMapsAbsent
    STMutez -> NestedBigMapsAbsent
    STBool -> NestedBigMapsAbsent
    STKeyHash -> NestedBigMapsAbsent
    STTimestamp -> NestedBigMapsAbsent
    STAddress -> NestedBigMapsAbsent
  
  -- | Check at runtime that the given type does not contain 'TOperation'.
  opAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoOp t)
  opAbsense s = case checkOpPresence s of
    OpPresent -> Nothing
    OpAbsent -> Just Dict
  
  -- | Check at runtime that the given type does not contain 'TContract'.
  contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoContract t)
  contractTypeAbsense s = case checkContractTypePresence s of
    ContractPresent -> Nothing
    ContractAbsent -> Just Dict
  
  -- | Check at runtime that the given type does not containt 'TBigMap'
  bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoBigMap t)
  bigMapAbsense s = case checkBigMapPresence s of
    BigMapPresent -> Nothing
    BigMapAbsent -> Just Dict
  
  -- | Check at runtime that the given type does not contain nested 'TBigMap'
  nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoNestedBigMaps t)
  nestedBigMapsAbsense s = case checkNestedBigMapsPresence s of
    NestedBigMapsPresent -> Nothing
    NestedBigMapsAbsent -> Just Dict
  
  ----------------------------------------------------------------------------
  -- Scopes
  ----------------------------------------------------------------------------
  
  data BadTypeForScope
    = BtNotComparable
    | BtIsOperation
    | BtHasBigMap
    | BtHasNestedBigMap
    | BtHasContract
    deriving stock (Show, Eq, Generic)
  
  -- | Alias for constraints which Michelson applies to parameter.
  type ParameterScope t =
    (Typeable t, SingI t, HasNoOp t, HasNoNestedBigMaps t)
  
  -- | Alias for constraints which Michelson applies to contract storage.
  type StorageScope t =
    (Typeable t, SingI t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t)
  
  -- | Alias for constraints which Michelson applies to pushed constants.
  type ConstantScope t =
    (SingI t, HasNoOp t, HasNoBigMap t, HasNoContract t)
  
  -- | Alias for constraints which Michelson applies to packed values.
  type PackedValScope t =
    (SingI t, HasNoOp t, HasNoBigMap t)
  
  -- | Alias for constraints which Michelson applies to unpacked values.
  --
  -- It is different from 'PackedValScope', e.g. @contract@ type cannot appear
  -- in a value we unpack to.
  type UnpackedValScope t =
    (PackedValScope t, ConstantScope t)
  
  -- | Alias for constraints which are required for printing.
  type PrintedValScope 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 (HasNoOp t) where
    checkScope = maybeToRight BtIsOperation $ opAbsense sing
  instance SingI t => CheckScope (HasNoBigMap t) where
    checkScope = maybeToRight BtHasBigMap $ bigMapAbsense sing
  instance SingI t => CheckScope (HasNoNestedBigMaps t) where
    checkScope = maybeToRight BtHasNestedBigMap $ nestedBigMapsAbsense sing
  instance SingI t => CheckScope (HasNoContract t) where
    checkScope = maybeToRight BtHasContract $ contractTypeAbsense sing
  
  instance (Typeable t, SingI t) => CheckScope (ParameterScope t) where
    checkScope =
      (\Dict Dict -> Dict)
        <$> checkScope @(HasNoOp t)
        <*> checkScope @(HasNoNestedBigMaps t)
  
  instance (Typeable t, SingI t) => CheckScope (StorageScope t) where
    checkScope =
      (\Dict Dict Dict -> Dict)
        <$> checkScope @(HasNoOp t)
        <*> checkScope @(HasNoNestedBigMaps t)
        <*> checkScope @(HasNoContract t)
  
  instance (Typeable t, SingI t) => CheckScope (ConstantScope t) where
    checkScope =
      (\Dict Dict Dict -> Dict)
        <$> checkScope @(HasNoOp t)
        <*> checkScope @(HasNoBigMap t)
        <*> checkScope @(HasNoContract t)
  
  instance (Typeable t, SingI t) => CheckScope (PackedValScope t) where
    checkScope =
      (\Dict Dict -> Dict)
        <$> checkScope @(HasNoOp t)
        <*> checkScope @(HasNoBigMap t)
  
  instance (Typeable t, SingI t) => CheckScope (UnpackedValScope t) where
    checkScope =
      (\Dict Dict -> Dict)
        <$> checkScope @(PackedValScope t)
        <*> checkScope @(ConstantScope t)
  
  -- 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 =
    (Typeable t, SingI t, ForbidOp t, ForbidNestedBigMaps t)
  
  type ProperStorageBetterErrors t =
    (Typeable t, SingI t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t)
  
  type ProperConstantBetterErrors t =
    (SingI t, ForbidOp t, ForbidBigMap t, ForbidContract t)
  
  type ProperPackedValBetterErrors t =
    (SingI t, ForbidOp t, ForbidBigMap t)
  
  type ProperUnpackedValBetterErrors t =
    (ProperPackedValBetterErrors t, ProperConstantBetterErrors t)
  
  type ProperPrintedValBetterErrors t =
    (SingI t, ForbidOp t)
  
  properParameterEvi :: forall t. ProperParameterBetterErrors t :- ParameterScope t
  properParameterEvi = Sub $
    Dict \\ forbiddenOpEvi @t \\ forbiddenNestedBigMapsEvi @t
  
  properStorageEvi :: forall t. ProperStorageBetterErrors t :- StorageScope t
  properStorageEvi = Sub $
    Dict \\ forbiddenOpEvi @t
         \\ forbiddenContractTypeEvi @t
         \\ forbiddenNestedBigMapsEvi @t
         \\ forbiddenContractTypeEvi @t
  
  properConstantEvi :: forall t. ProperConstantBetterErrors t :- ConstantScope t
  properConstantEvi = Sub $
    Dict \\ forbiddenOpEvi @t
         \\ forbiddenBigMapEvi @t
         \\ forbiddenContractTypeEvi @t
  
  properPackedValEvi :: forall t. ProperPackedValBetterErrors t :- PackedValScope t
  properPackedValEvi = Sub $
    Dict \\ forbiddenOpEvi @t
         \\ forbiddenBigMapEvi @t
  
  properUnpackedValEvi :: forall t. ProperUnpackedValBetterErrors t :- UnpackedValScope t
  properUnpackedValEvi = properPackedValEvi @t *** properConstantEvi @t
  
  properPrintedValEvi :: forall t. ProperPrintedValBetterErrors t :- PrintedValScope t
  properPrintedValEvi = Sub $
    Dict \\ forbiddenOpEvi @t
  