Set of constraints that Michelson applies to pushed constants.

Not just a type alias in order to be able to partially apply it

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: ConstantScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `operation`, `big_map`, `contract`, `ticket` or `sapling_state`. Perhaps you need to add
... ConstantScope t0
... constraint? You can also try adding a type annotation.
...

Alias for constraints which Michelson requires in DUP instruction.

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: DupableScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `ticket`. Perhaps you need to add
... DupableScope t0
... constraint? You can also try adding a type annotation.
...

Set of constraints that Michelson applies to contract storage.

Not just a type alias in order to be able to partially apply it

Produces human-readable error messages:

>>> () :: StorageScope (TContract TOperation) => ()
...
... Type `operation` found in
... 'TOperation
... is not allowed in this scope
...
... Type `contract` found in
... 'TContract 'TOperation
... is not allowed in this scope
...
>>> () :: StorageScope TUnit => ()
()

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: StorageScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `operation`, nested `big_map`s or `contract`. Perhaps you need to add
... StorageScope t0
... constraint? You can also try adding a type annotation.
...

Set of constraints that Michelson applies to packed values.

Not just a type alias in order to be able to partially apply it.

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: PackedValScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `operation`, `big_map`, `ticket` or `sapling_state`. Perhaps you need to add
... PackedValScope t0
... constraint? You can also try adding a type annotation.
...

Set of constraints that Michelson applies to parameters.

Not just a type alias in order to be able to partially apply it

Produces human-readable error messages:

>>> () :: ParameterScope (TBigMap TUnit (TBigMap TUnit TOperation)) => ()
...
... Type `operation` found in
... 'TBigMap 'TUnit ('TBigMap 'TUnit 'TOperation)
... is not allowed in this scope
...
... Nested `big_map`s found in
... 'TBigMap 'TUnit ('TBigMap 'TUnit 'TOperation)
... are not allowed
...
>>> () :: ParameterScope (TBigMap TInt TNat) => ()
()

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: ParameterScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `operation` or nested `big_map`s. Perhaps you need to add
... ParameterScope t0
... constraint? You can also try adding a type annotation.
...

Alias for constraints which are required for untyped representation.

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: UntypedValScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `operation`. Perhaps you need to add
... UntypedValScope t0
... constraint? You can also try adding a type annotation.
...

Set of constraints that Michelson applies to unpacked values. Same as ConstantScope.

Not just a type alias in order to show better errors on ambiguity or missing constraint.

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: UnpackedValScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `operation`, `big_map`, `contract`, `ticket` or `sapling_state`. Perhaps you need to add
... UnpackedValScope t0
... constraint? You can also try adding a type annotation.
...

Set of constraints that Michelson applies to argument type and return type of views. All info related to views can be found in TZIP.

Not just a type alias in order to be able to partially apply it.

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: ViewableScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `operation`, `big_map` or `ticket`. Perhaps you need to add
... ViewableScope t0
... constraint? You can also try adding a type annotation.
...

Alias for comparable types.

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: ComparabilityScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains non-comparable types. Perhaps you need to add
... ComparabilityScope t0
... constraint? You can also try adding a type annotation.
...

Returns whether the type is dupable.

Should be present for common scopes.

Allows using a scope that can be proven true with a De Morgan law.

Many scopes are defined as not a (or rather a ~ 'False) where a is a negative property we want to avoid as a Constraint. The negative constraints are implemented with a type family that for some combination types resolves to itself applied to the type arguments in an or, e.g. A pair l r has x if l or r contain x.

Because of the De Morgan laws not (a or b) implies (not a) and (not b) or in our case: pair does not contain x -> a and b don't contain x.

Simpler version of withDeMorganScope for ForbidT constraints.

Produce ComparabilityImplies on demand. Carrying it as Comparable superclasses turns out to be a little expensive, considering we can produce evidence on demand in O(1).

This class encodes Michelson rules w.r.t where it requires comparable types. Earlier we had a dedicated type for representing comparable types CT. But then we integreated those types into T. This meant that some of the types that could be formed with various combinations of T would be illegal as per Michelson typing rule. Using this class, we inductively enforce that a type and all types it contains are well typed as per Michelson's rules.

Error type for when a value is not well-typed.

Constraint for classes forbidding type presence based on predicate defined by TPredicateSym.

Not just a type alias in order to be able to partially apply it (e.g. in Each).

Reports errors when a type does not satisfy predicate:

>>> () :: ForbidT PSOp TOperation => ()
...
... Type `operation` found in
... 'TOperation
... is not allowed in this scope
...
>>> () :: ForbidT PSContract (TContract TUnit) => ()
...
... Type `contract` found in
... 'TContract 'TUnit
... is not allowed in this scope
...
>>> () :: ForbidT PSTicket (TTicket TUnit) => ()
...
... Type `ticket` found in
... 'TTicket 'TUnit
... is not allowed in this scope
...
>>> () :: ForbidT PSBigMap (TBigMap TUnit TUnit) => ()
...
... Type `big_map` found in
... 'TBigMap 'TUnit 'TUnit
... is not allowed in this scope
...
>>> () :: ForbidT PSSaplingState (TSaplingState Z) => ()
...
... Type `sapling_state` found in
... 'TSaplingState 'Z
... is not allowed in this scope
...
>>> () :: ForbidT PSNestedBigMaps (TBigMap TUnit (TBigMap TUnit TUnit)) => ()
...
... Nested `big_map`s found in
... 'TBigMap 'TUnit ('TBigMap 'TUnit 'TUnit)
... are not allowed
...

When the type is ambiguous or polymorphic, suggests adding the corresponding constraint:

>>> (const () :: ForbidOp t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `operation`. Perhaps you need to add
... ForbidT 'PSOp t0
... constraint? You can also try adding a type annotation.
...

This constraint implies ContainsT ~ False:

>>> :{
foo :: ForbidT p t => ContainsT p t :~: False
foo = Refl
:}

Whether a value of this type _may_ contain a type defined by TPredicateSym.

Type-level symbol for type predicates used in ContainsT

Check for presence of type defined by TPredicateSym at runtime. Use TPredicateSym singletons (i.e. SingTPredicateSym) as the first parameter, e.g.:

>>> checkTPresence SPSOp STOperation
TPresent
>>> checkTPresence SPSOp STUnit
TAbsent

To only prove absence of some type, it is more efficient to use deMorganForbidT or withDeMorganScope.

Check if type is comparable or not at runtime. This traverses the singleton, so it has a considerable runtime cost. If you just need to convince GHC, you may be looking for comparableImplies, or perhaps withDeMorganScope.

>>> checkComparability STOperation
CannotBeCompared
>>> checkComparability STAddress
CanBeCompared

Check if type is comparable or not at runtime. This is a Dict version of checkComparability, so the same caveats apply.

>>> comparabilityPresence STOperation
Nothing
>>> comparabilityPresence STAddress
Just Dict

Given a type, provide evidence that it is well typed w.r.t to the Michelson rules regarding where comparable types are required.

>>> either pretty print $ getWTP @'TUnit
Dict
>>> either pretty print $ getWTP @('TSet 'TOperation)
Given type is not well typed because 'operation' is not comparable
>>> type Pairs a = 'TPair a a
>>> type Pairs2 = Pairs (Pairs 'TUnit)
>>> either pretty print $ getWTP @('TSet ('TPair Pairs2 'TOperation))
Given type is not well typed because
  pair (pair (pair unit unit) unit unit) operation
is not comparable

Version of getWTP that accepts Sing at term-level.

From a Dict, takes a value in an environment where the instance witnessed by the Dict is in scope, and evaluates it.

Essentially a deconstruction of a Dict into its continuation-style form.

Can also be used to deconstruct an entailment, a :- b, using a context a.

withDict :: Dict c -> (c => r) -> r
withDict :: a => (a :- c) -> (c => r) -> r

A SingI constraint is essentially an implicitly-passed singleton. If you need to satisfy this constraint with an explicit singleton, please see withSingI or the Sing pattern synonym.