| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Morley.Michelson.Typed.Scope.Internal.WellTyped
Synopsis
- data BadTypeForScope
- class (SingI t, RecSuperC WellTyped t, WellTypedConstraints t) => WellTyped t
- data NotWellTyped = NotWellTyped {}
- type family WellTypedConstraints t where ...
- getWTP :: forall t. SingI t => Either NotWellTyped (Dict (WellTyped t))
- getWTP' :: Sing t -> Either NotWellTyped (Dict (WellTyped t))
Documentation
data BadTypeForScope Source #
Constructors
| BtNotComparable | |
| BtIsOperation | |
| BtHasBigMap | |
| BtHasNestedBigMap | |
| BtHasContract | |
| BtHasTicket | |
| BtHasSaplingState |
Instances
class (SingI t, RecSuperC WellTyped t, WellTypedConstraints t) => WellTyped t Source #
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.
Instances
| (SingI t, RecSuperC WellTyped t, WellTypedConstraints t) => WellTyped t Source # | |
| SingI t => CheckScope (WellTyped t) Source # | |
Defined in Morley.Michelson.Typed.Scope.Internal.CheckScope Methods checkScope :: Either BadTypeForScope (Dict (WellTyped t)) Source # | |
data NotWellTyped Source #
Error type for when a value is not well-typed.
Constructors
| NotWellTyped | |
Fields
| |
Instances
| Buildable NotWellTyped Source # | |
type family WellTypedConstraints t where ... Source #
Additional (non-recursive) constraints on type arguments for specific types
Equations
| WellTypedConstraints ('TSet t) = Comparable t | |
| WellTypedConstraints ('TContract t) = (ForbidOp t, ForbidNestedBigMaps t) | |
| WellTypedConstraints ('TTicket t) = Comparable t | |
| WellTypedConstraints ('TMap k _) = Comparable k | |
| WellTypedConstraints ('TBigMap k v) = (Comparable k, ForbidBigMap v, ForbidOp v) | |
| WellTypedConstraints _ = () |
getWTP :: forall t. SingI t => Either NotWellTyped (Dict (WellTyped t)) Source #
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 @'TUnitDict>>>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