morley-1.8.0: docs/morleyTypechecker.md

<!--
SPDX-FileCopyrightText: 2020 Tocqueville Group

SPDX-License-Identifier: LicenseRef-MIT-TQ
-->

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