-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

{-# 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 Michelson.Typed.Scope
  ( -- * 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.Constraint ((:-)(..), Dict(..), withDict, (\\))
import qualified Data.Constraint as C
import Data.Singletons (Sing, SingI(..))
import Data.Type.Bool (type (||))
import Fmt (Buildable(..))
import GHC.TypeLits (ErrorMessage(..), TypeError)

import Michelson.Typed.Sing (KnownT, SingT(..))
import Michelson.Typed.T (T(..))

----------------------------------------------------------------------------
-- 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', 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 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 :: (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
    OpAbsent -> Dict (HasNoOp t)
forall (a :: Constraint). a => Dict a
Dict
    OpPresent -> Text -> Dict (HasNoOp t)
forall a. HasCallStack => Text -> a
error "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
    BigMapAbsent -> Dict (HasNoBigMap t)
forall (a :: Constraint). a => Dict a
Dict
    BigMapPresent -> Text -> Dict (HasNoBigMap t)
forall a. HasCallStack => Text -> a
error "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
    NestedBigMapsAbsent -> Dict (HasNoNestedBigMaps t)
forall (a :: Constraint). a => Dict a
Dict
    NestedBigMapsPresent -> Text -> Dict (HasNoNestedBigMaps t)
forall a. HasCallStack => Text -> a
error "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
    ContractAbsent -> Dict (HasNoContract t)
forall (a :: Constraint). a => Dict a
Dict
    ContractPresent -> Text -> Dict (HasNoContract t)
forall a. HasCallStack => Text -> a
error "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

-- | 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 :: 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.
  STKey -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STSignature -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STChainId -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STUnit -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STOption t -> case Sing a -> OpPresence a
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing a
t of
    OpPresent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    OpAbsent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STList t -> case Sing a -> OpPresence a
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing a
t of
    OpPresent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    OpAbsent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STSet a -> case Sing a -> OpPresence a
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing a
a of
    OpPresent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    OpAbsent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STOperation -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
  STContract t -> case Sing a -> OpPresence a
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing a
t of
    OpPresent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    OpAbsent -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STPair a b -> case (Sing a -> OpPresence a
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing a
a, Sing b -> OpPresence b
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing b
b) of
    (OpPresent, _) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    (_, OpPresent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    (OpAbsent, OpAbsent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STOr a b -> case (Sing a -> OpPresence a
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing a
a, Sing b -> OpPresence b
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing b
b) of
    (OpPresent, _) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    (_, OpPresent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    (OpAbsent, 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 a -> OpPresence a
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing a
k, Sing b -> OpPresence b
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing b
v) of
    (OpAbsent, OpAbsent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
    (OpPresent, _) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    (_, OpPresent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
  STBigMap k v -> case (Sing a -> OpPresence a
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing a
k, Sing b -> OpPresence b
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing b
v) of
    (OpAbsent, OpAbsent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
    (OpPresent, _) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
    (_, OpPresent) -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'True) => OpPresence t
OpPresent
  STInt -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STNat -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STString -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STBytes -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STMutez -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STBool -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STKeyHash -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STTimestamp -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent
  STAddress -> OpPresence ty
forall (t :: T). (ContainsOp t ~ 'False) => OpPresence t
OpAbsent

-- | Check at runtime whether the given type contains 'TContract'.
checkContractTypePresence :: Sing (ty :: T) -> ContractPresence ty
checkContractTypePresence :: Sing ty -> ContractPresence ty
checkContractTypePresence = \case
  STKey -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STSignature -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STChainId -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STUnit -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STOption t -> case Sing a -> ContractPresence a
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing a
t of
    ContractPresent -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    ContractAbsent -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STList t -> case Sing a -> ContractPresence a
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing a
t of
    ContractPresent -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    ContractAbsent -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STSet _ -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STOperation -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STContract _ -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
  STPair a b -> case (Sing a -> ContractPresence a
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing a
a, Sing b -> ContractPresence b
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing b
b) of
    (ContractPresent, _) -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    (_, ContractPresent) -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    (ContractAbsent, ContractAbsent) -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STOr a b -> case (Sing a -> ContractPresence a
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing a
a, Sing b -> ContractPresence b
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing b
b) of
    (ContractPresent, _) -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    (_, ContractPresent) -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    (ContractAbsent, 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 b -> ContractPresence b
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing b
v of
    ContractPresent -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    ContractAbsent -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STBigMap _ v -> case Sing b -> ContractPresence b
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing b
v of
    ContractPresent -> ContractPresence ty
forall (t :: T). (ContainsContract t ~ 'True) => ContractPresence t
ContractPresent
    ContractAbsent -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STInt -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STNat -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STString -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STBytes -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STMutez -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STBool -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STKeyHash -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STTimestamp -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent
  STAddress -> ContractPresence ty
forall (t :: T).
(ContainsContract t ~ 'False) =>
ContractPresence t
ContractAbsent

-- | Check at runtime whether the given type contains 'TBigMap'.
checkBigMapPresence :: Sing (ty :: T) -> BigMapPresence ty
checkBigMapPresence :: Sing ty -> BigMapPresence ty
checkBigMapPresence = \case
  -- More boilerplate to boilerplate god.
  STKey -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STSignature -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STChainId -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STUnit -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STOption t -> case Sing a -> BigMapPresence a
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing a
t of
    BigMapPresent -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
    BigMapAbsent -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STList t -> case Sing a -> BigMapPresence a
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing a
t of
    BigMapPresent -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
    BigMapAbsent -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STSet _ -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STOperation -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STContract t -> case Sing a -> BigMapPresence a
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing a
t of
    BigMapPresent -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
    BigMapAbsent -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STPair a b -> case (Sing a -> BigMapPresence a
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing a
a, Sing b -> BigMapPresence b
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing b
b) of
    (BigMapPresent, _) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
    (_, BigMapPresent) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
    (BigMapAbsent, BigMapAbsent) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STOr a b -> case (Sing a -> BigMapPresence a
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing a
a, Sing b -> BigMapPresence b
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing b
b) of
    (BigMapPresent, _) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
    (_, BigMapPresent) -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
    (BigMapAbsent, 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 b -> BigMapPresence b
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing b
v of
    BigMapPresent -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
    BigMapAbsent -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STBigMap _ _ ->
    BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'True) => BigMapPresence t
BigMapPresent
  STInt -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STNat -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STString -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STBytes -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STMutez -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STBool -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STKeyHash -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STTimestamp -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent
  STAddress -> BigMapPresence ty
forall (t :: T). (ContainsBigMap t ~ 'False) => BigMapPresence t
BigMapAbsent

-- | Check at runtime whether the given type contains 'TBigMap'.
checkNestedBigMapsPresence :: Sing (ty :: T) -> NestedBigMapsPresence ty
checkNestedBigMapsPresence :: Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence = \case
  -- More boilerplate to boilerplate god.
  STKey -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STSignature -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STChainId -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STUnit -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STOption t -> case Sing a -> NestedBigMapsPresence a
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing a
t of
    NestedBigMapsPresent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    NestedBigMapsAbsent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STList                   t -> case Sing a -> NestedBigMapsPresence a
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing a
t of
    NestedBigMapsPresent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    NestedBigMapsAbsent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STSet _ -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STOperation -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STContract t -> case Sing a -> NestedBigMapsPresence a
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing a
t of
    NestedBigMapsPresent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    NestedBigMapsAbsent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STPair a b -> case (Sing a -> NestedBigMapsPresence a
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing a
a, Sing b -> NestedBigMapsPresence b
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing b
b) of
    (NestedBigMapsPresent, _) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    (_, NestedBigMapsPresent) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    (NestedBigMapsAbsent, NestedBigMapsAbsent) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STOr a b -> case (Sing a -> NestedBigMapsPresence a
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing a
a, Sing b -> NestedBigMapsPresence b
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing b
b) of
    (NestedBigMapsPresent, _) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    (_, NestedBigMapsPresent) -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    (NestedBigMapsAbsent, 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 b -> NestedBigMapsPresence b
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing b
v of
    NestedBigMapsPresent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    NestedBigMapsAbsent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STBigMap _ v -> case Sing b -> BigMapPresence b
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing b
v of
    BigMapPresent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'True) =>
NestedBigMapsPresence t
NestedBigMapsPresent
    BigMapAbsent -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STInt -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STNat -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STString -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STBytes -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STMutez -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STBool -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STKeyHash -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STTimestamp -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent
  STAddress -> NestedBigMapsPresence ty
forall (t :: T).
(ContainsNestedBigMaps t ~ 'False) =>
NestedBigMapsPresence t
NestedBigMapsAbsent

-- | Check at runtime that the given type does not contain 'TOperation'.
opAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoOp t)
opAbsense :: Sing t -> Maybe (Dict $ HasNoOp t)
opAbsense s :: Sing t
s = case Sing t -> OpPresence t
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing t
s of
  OpPresent -> Maybe (Dict $ HasNoOp t)
forall a. Maybe a
Nothing
  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 the given type does not contain 'TContract'.
contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoContract t)
contractTypeAbsense :: Sing t -> Maybe (Dict $ HasNoContract t)
contractTypeAbsense s :: Sing t
s = case Sing t -> ContractPresence t
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing t
s of
  ContractPresent -> Maybe (Dict $ HasNoContract t)
forall a. Maybe a
Nothing
  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 the given type does not containt 'TBigMap'
bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoBigMap t)
bigMapAbsense :: Sing t -> Maybe (Dict $ HasNoBigMap t)
bigMapAbsense s :: Sing t
s = case Sing t -> BigMapPresence t
forall (ty :: T). Sing ty -> BigMapPresence ty
checkBigMapPresence Sing t
s of
  BigMapPresent -> Maybe (Dict $ HasNoBigMap t)
forall a. Maybe a
Nothing
  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 the given type does not contain nested 'TBigMap'
nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoNestedBigMaps t)
nestedBigMapsAbsense :: Sing t -> Maybe (Dict $ HasNoNestedBigMaps t)
nestedBigMapsAbsense s :: Sing t
s = case Sing t -> NestedBigMapsPresence t
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing t
s of
  NestedBigMapsPresent -> Maybe (Dict $ HasNoNestedBigMaps t)
forall a. Maybe a
Nothing
  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
  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 = \case
    BtNotComparable -> "is not comparable"
    BtIsOperation -> "has 'operation' type"
    BtHasBigMap -> "has 'big_map'"
    BtHasNestedBigMap -> "has nested 'big_map'"
    BtHasContract -> "has 'contract' type"

-- | Alias for constraints which Michelson applies to parameter.
type ParameterScope t =
  (KnownT t, HasNoOp t, HasNoNestedBigMaps t)

-- | Alias for constraints which Michelson applies to contract storage.
type StorageScope t =
  (KnownT 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 :: 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 KnownT t => CheckScope (ParameterScope t) where
  checkScope :: Either BadTypeForScope (Dict (ParameterScope t))
checkScope =
    (\Dict Dict -> Dict (ParameterScope t)
forall (a :: Constraint). a => Dict a
Dict)
      (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. 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 (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 KnownT t => CheckScope (StorageScope t) where
  checkScope :: Either BadTypeForScope (Dict (StorageScope t))
checkScope =
    (\Dict Dict Dict -> Dict (StorageScope t)
forall (a :: Constraint). a => Dict a
Dict)
      (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. 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 (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 KnownT t => CheckScope (ConstantScope t) where
  checkScope :: Either BadTypeForScope (Dict (ConstantScope t))
checkScope =
    (\Dict Dict Dict -> Dict (ConstantScope t)
forall (a :: Constraint). a => Dict a
Dict)
      (Dict (HasNoOp t)
 -> Dict (HasNoBigMap t)
 -> Dict (HasNoContract t)
 -> Dict (ConstantScope t))
-> Either BadTypeForScope (Dict (HasNoOp t))
-> Either
     BadTypeForScope
     (Dict (HasNoBigMap t)
      -> Dict (HasNoContract t) -> Dict (ConstantScope 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 (HasNoContract t) -> Dict (ConstantScope t))
-> Either BadTypeForScope (Dict (HasNoBigMap t))
-> Either
     BadTypeForScope (Dict (HasNoContract 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 (ConstantScope t))
-> Either BadTypeForScope (Dict (HasNoContract t))
-> Either BadTypeForScope (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)

instance KnownT t => CheckScope (PackedValScope t) where
  checkScope :: Either BadTypeForScope (Dict (PackedValScope t))
checkScope =
    (\Dict Dict -> Dict (PackedValScope t)
forall (a :: Constraint). a => Dict a
Dict)
      (Dict (HasNoOp t)
 -> Dict (HasNoBigMap t) -> Dict (PackedValScope t))
-> Either BadTypeForScope (Dict (HasNoOp t))
-> Either
     BadTypeForScope (Dict (HasNoBigMap t) -> Dict (PackedValScope 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 (PackedValScope t))
-> Either BadTypeForScope (Dict (HasNoBigMap t))
-> Either BadTypeForScope (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)

instance KnownT t => CheckScope (UnpackedValScope t) where
  checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t))
checkScope =
    (\Dict Dict -> Dict (UnpackedValScope t)
forall (a :: Constraint). a => Dict a
Dict)
      (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. Functor 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)

-- 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 =
  (KnownT t, ForbidOp t, ForbidNestedBigMaps t)

type ProperStorageBetterErrors t =
  (KnownT 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 :: 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

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

properUnpackedValEvi :: forall t. ProperUnpackedValBetterErrors t :- UnpackedValScope t
properUnpackedValEvi :: ProperUnpackedValBetterErrors t :- UnpackedValScope t
properUnpackedValEvi = ProperPackedValBetterErrors t :- PackedValScope t
forall (t :: T). ProperPackedValBetterErrors t :- PackedValScope t
properPackedValEvi @t (ProperPackedValBetterErrors t :- PackedValScope t)
-> ((SingI t, FailOnOperationFound (ContainsOp t),
     FailOnBigMapFound (ContainsBigMap t),
     FailOnContractFound (ContainsContract t))
    :- ConstantScope t)
-> ProperUnpackedValBetterErrors t :- UnpackedValScope t
forall (a :: Constraint) (b :: Constraint) (c :: Constraint)
       (d :: Constraint).
(a :- b) -> (c :- d) -> (a, c) :- (b, d)
C.*** (SingI t, FailOnOperationFound (ContainsOp t),
 FailOnBigMapFound (ContainsBigMap t),
 FailOnContractFound (ContainsContract t))
:- ConstantScope t
forall (t :: T). ProperConstantBetterErrors t :- ConstantScope t
properConstantEvi @t

properPrintedValEvi :: forall t. ProperPrintedValBetterErrors t :- PrintedValScope t
properPrintedValEvi :: ProperPrintedValBetterErrors t :- PrintedValScope t
properPrintedValEvi = (ProperPrintedValBetterErrors t => Dict (PrintedValScope t))
-> ProperPrintedValBetterErrors t :- PrintedValScope t
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((ProperPrintedValBetterErrors t => Dict (PrintedValScope t))
 -> ProperPrintedValBetterErrors t :- PrintedValScope t)
-> (ProperPrintedValBetterErrors t => Dict (PrintedValScope t))
-> ProperPrintedValBetterErrors t :- PrintedValScope t
forall a b. (a -> b) -> a -> b
$
  HasNoOp t => Dict (PrintedValScope t)
forall (a :: Constraint). a => Dict a
Dict (HasNoOp t => Dict (PrintedValScope t))
-> (ProperPrintedValBetterErrors t :- HasNoOp t)
-> Dict (PrintedValScope t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ProperPrintedValBetterErrors t :- HasNoOp t
forall (t :: T). (SingI t, ForbidOp t) :- HasNoOp t
forbiddenOpEvi @t