Michelson.TypeCheck.Instr

Module, providing functions for conversion from instruction and value representation from Michelson.Type module to strictly-typed GADT-based representation from Michelson.Value module.

This conversion is labeled as type check because that's what we are obliged to do on our way.

Type check algorithm relies on the property of Michelson language that each instruction on a given input stack type produces a definite output stack type. Michelson contract defines concrete types for storage and parameter, from which input stack type is deduced. Then this type is being combined with each subsequent instruction, producing next stack type after each application.

Function typeCheck takes list of instructions and returns value of type Instr inp out along with HST inp and HST out all wrapped into SomeInstr data type. This wrapping is done to satsify Haskell type system (which has no support for dependent types). Functions typeCheckInstr, typeCheckValue behave similarly.

When a recursive call is made within typeCheck, typeCheckInstr or typeCheckValue, result of a call is unwrapped from SomeInstr and type information from HST inp and HST out is being used to assert that recursive call returned instruction of expected type (error is thrown otherwise).

Documentation

typeCheckContract :: TcOriginatedContracts -> Contract -> Either TCError SomeContract

typeCheckValue :: forall t. SingI t => Value -> TypeCheckInstr (Value t)

Function typeCheckValue converts a single Michelson value given in representation from Michelson.Untyped module hierarchy to representation in strictly typed GADT.

typeCheckValue is polymorphic in the expected type of value.

Type checking algorithm pattern-matches on parse value representation, expected type t and constructs Val t value.

If there was no match on a given pair of value and expected type, that is interpreted as input of wrong type and type check finishes with error.

typeCheckList :: Typeable inp => [ExpandedOp] -> HST inp -> TypeCheck (SomeInstr inp)

Function typeCheckList converts list of Michelson instructions given in representation from Michelson.Type module to representation in strictly typed GADT.

Types are checked along the way which is neccessary to construct a strictly typed value.

As a second argument, typeCheckList accepts input stack type representation.

typeVerifyTopLevelType :: (SingI t, HasCallStack) => TcOriginatedContracts -> Value -> Either TCError (Value t)

typeCheckTopLevelType :: HasCallStack => TcOriginatedContracts -> Type -> Value -> Either TCError SomeValue