Morley.Michelson.Typed.Scope.Internal.WellTyped

Documentation

data BadTypeForScope

Constructors

BtNotComparable

BtIsOperation

BtHasBigMap

BtHasNestedBigMap

BtHasContract

BtHasTicket

BtHasSaplingState

Instances

Generic BadTypeForScope

Defined in Morley.Michelson.Typed.Scope.Internal.WellTyped

Associated Types

type Rep BadTypeForScope :: Type -> Type

Methods

from :: BadTypeForScope -> Rep BadTypeForScope x

to :: Rep BadTypeForScope x -> BadTypeForScope

Show BadTypeForScope

Defined in Morley.Michelson.Typed.Scope.Internal.WellTyped

Methods

showsPrec :: Int -> BadTypeForScope -> ShowS

show :: BadTypeForScope -> String

showList :: [BadTypeForScope] -> ShowS

NFData BadTypeForScope

Defined in Morley.Michelson.Typed.Scope.Internal.WellTyped

Methods

rnf :: BadTypeForScope -> ()

Eq BadTypeForScope

Defined in Morley.Michelson.Typed.Scope.Internal.WellTyped

Methods

(==) :: BadTypeForScope -> BadTypeForScope -> Bool

(/=) :: BadTypeForScope -> BadTypeForScope -> Bool

Buildable BadTypeForScope

Defined in Morley.Michelson.Typed.Scope.Internal.WellTyped

Methods

build :: BadTypeForScope -> Doc

buildList :: [BadTypeForScope] -> Doc

type Rep BadTypeForScope

Defined in Morley.Michelson.Typed.Scope.Internal.WellTyped

type Rep BadTypeForScope = D1 ('MetaData "BadTypeForScope" "Morley.Michelson.Typed.Scope.Internal.WellTyped" "morley-1.20.0-inplace" 'False) ((C1 ('MetaCons "BtNotComparable" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BtIsOperation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BtHasBigMap" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BtHasNestedBigMap" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BtHasContract" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BtHasTicket" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BtHasSaplingState" 'PrefixI 'False) (U1 :: Type -> Type))))

class (SingI t, RecSuperC WellTyped t, WellTypedConstraints t) => WellTyped t

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

Defined in Morley.Michelson.Typed.Scope.Internal.WellTyped

SingI t => CheckScope (WellTyped t)

Defined in Morley.Michelson.Typed.Scope.Internal.CheckScope

Methods

checkScope :: Either BadTypeForScope (Dict (WellTyped t))

data NotWellTyped

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

Constructors

NotWellTyped

Fields

• nwtBadType :: T
• nwtCause :: BadTypeForScope

Instances

Buildable NotWellTyped

Defined in Morley.Michelson.Typed.Scope.Internal.WellTyped

Methods

build :: NotWellTyped -> Doc

buildList :: [NotWellTyped] -> Doc

type family WellTypedConstraints t where ...

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

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

getWTP' :: Sing t -> Either NotWellTyped (Dict (WellTyped t))

Version of getWTP that accepts Sing at term-level.