Implement a proper bidirectional algorithm

[yannham]

Is your feature request related to a problem? Please describe.
The current implementation of the typechecker is more or less based on a bidirectional typechecking algorithm, but mixes both inference, checking and a third nickel-specific mode, the non-strict mode (where we just walk the AST looking for the next statically typed block to handle). The information flow is not always clear, the algorithm is hard to extend, and some edge cases are not handled well (higher rank types checking and polymorphic type instantiation, mainly). A proper bidirectional algorithm would make it easier to add subtyping as well, with the relation induced by T <: Dyn, for example. The walking phase is also wasteful: we continue to generate unification variable, but just don't actually unify them.

Describe the solution you'd like
Have a formal bidirectional formulation of the type system on paper. Implement it and break the type_check_ function into three mutually recursive functions (or, constraints generating function later, if this is too stack-hungry), walk, infer and check, with clear roles and information flow.

Additional context
Such an enterprise was already tried in #392, but it hit some non-trivial issues with polymorphic instantiation and order of arguments (dubbed the "tabby-first problem" in section 5.1 of Krishnaswami and Dunfield). A first step could be to forget about Dyn-induced subtying for now, and adapt Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism, which doesn't have this issue.

[yannham]

I'm setting the milestone to 1.0, which doesn't mean "implement RFC004", but rather refactor and clarify a bit the algorithm around clear notion of inference and checking modes.

[yannham]

Post-poned to after 1.0. Variable levels are non trivial to implement and the feature is not critical.