Bidirectional type checking for LIGO

type:changed

This MR aims to replace LIGO's existing type checker and type inference implementation with a more principled theoretical approach based on "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism" [0]. The working formalisation for LIGO's type system (based on this approach) can be found here: https://gitlab.com/alistair.obrien/ligo-type-system/-/blob/main/main.pdf.

Benefits:

• A theoretical grounding of LIGO's type system and it's implementation. This will provide useful documentation for the type checker and aid in the transition to dependent types.
• Lays the foundation for a bidirectional type checker for the dependent calculus that will be used in the future.
• Aims to reduce the number of redundant annotations required by LIGO programs.

[0] https://www.cl.cam.ac.uk/~nk480/bidir.pdf

Changelog details:

Re-implement LIGO's type checker using bidirectional type checking.