Alias for constraints which Michelson applies to parameter.

Alias for constraints which Michelson applies to contract storage.

Alias for constraints which Michelson applies to pushed constants.

Alias for constraints which Michelson applies to packed values.

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.

Alias for constraints which are required for printing.

This is the type of entailment.

a :- b is read as a "entails" b.

With this we can actually build a category for Constraint resolution.

e.g.

Because Eq a is a superclass of Ord a, we can show that Ord a entails Eq a.

Because instance Ord a => Ord [a] exists, we can show that Ord a entails Ord [a] as well.

This relationship is captured in the :- entailment type here.

Since p :- p and entailment composes, :- forms the arrows of a Category of constraints. However, Category only became sufficiently general to support this instance in GHC 7.8, so prior to 7.8 this instance is unavailable.

But due to the coherence of instance resolution in Haskell, this Category has some very interesting properties. Notably, in the absence of IncoherentInstances, this category is "thin", which is to say that between any two objects (constraints) there is at most one distinguishable arrow.

This means that for instance, even though there are two ways to derive Ord a :- Eq [a], the answers from these two paths _must_ by construction be equal. This is a property that Haskell offers that is pretty much unique in the space of languages with things they call "type classes".

What are the two ways?

Well, we can go from Ord a :- Eq a via the superclass relationship, and then from Eq a :- Eq [a] via the instance, or we can go from Ord a :- Ord [a] via the instance then from Ord [a] :- Eq [a] through the superclass relationship and this diagram by definition must "commute".

Diagrammatically,

                   Ord a
               ins /     \ cls
                  v       v
            Ord [a]     Eq a
               cls \     / ins
                    v   v
                   Eq [a]

This safety net ensures that pretty much anything you can write with this library is sensible and can't break any assumptions on the behalf of library authors.

Constraint which ensures that bigmap does not appear in a given type.

Constraint which ensures that there are no nested bigmaps

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).

Constraint which ensures that contract type does not appear in a given type.

Whether this type contains TBigMap type.

Whether this type contains a type with nested TBigMaps .

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.

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.

Use it in our eDSL.

Report a human-readable error about TBigMap at a wrong place.

Report a human-readable error that TBigMap contains another TBigMap

Report a human-readable error about TOperation at a wrong place.

Whether the type contains TOperation, with proof.

Check at runtime whether the given type contains TOperation.

Check at runtime whether the given type contains TContract.

Check at runtime whether the given type contains TBigMap.

Check at runtime whether the given type contains TBigMap.

Check at runtime that the given type does not contain TOperation.

Check at runtime that the given type does not contain TContract.

Check at runtime that the given type does not containt TBigMap

Check at runtime that the given type does not contain nested TBigMap

Reify HasNoOp contraint from ForbidOp.

Left for backward compatibility.

Reify HasNoContract contraint from ForbidContract.

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