morley-1.7.1: 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.

Example: `morley typecheck --contract auction.tz`.

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