# Morley Typechecker In Morley, we have a typechecker for the core Michelson language, i. e. without macros. It is located in `Michelson.TypeCheck` and designed in the following way: * It takes a core Michelson contract extended with `EXT` instruction to support additional instructions described in the [`morleyInstructions.md`](language/morleyInstructions.md) document. * The contract passed to the typechecker uses [untyped representation](./michelsonTypes.md). * During typechecking, we verify that instructions are well-typed and provide evidence to the compiler that allows us to convert instructions into [typed representation](./michelsonTypes.md). If the contract is ill-typed, the typechecking process fails with an error. * The typechecker can check a whole contract or a standalone value (for example, a lambda). In the former case it needs to know the parameter type of the contract (to check `SELF`). ## CLI End users can use the `typecheck` command to execute the typechecker. It parses the contract, performs macro expansion, and passes it to the typechecker which says that the contract is well-typed or produces an error message. Additionally, one can specify a `--verbose` option to print stack types between instructions which is useful for debugging. Example: `morley typecheck --contract auction.tz --verbose`. ## Internals An internal structure of the typechecker is pretty well described in Haddock comments. Two main modules are: * [`Michelson.TypeCheck.Value`](/code/morley/src/Michelson/TypeCheck/Value.hs) contains logic for checking Michelson values. * [`Michelson.TypeCheck.Instr`](/code/morley/src/Michelson/TypeCheck/Instr.hs) contains logic for checking Michelson instructions and the whole contract. Their functionality is re-exported from the [`Michelson.TypeCheck`](/code/morley/src/Michelson/TypeCheck.hs) module along with some auxiliary types and functions.