Unification

[robrix]

This PR:

• [x] Implements dependent unification of types.
• [x] Uses dependent unification instead of α-equivalence of types when switching from checking mode to inference mode.
• [x] Replaces vforce, while still enabling nice error messages/pretty-printed types.
• Contextualizes unification failures with the part of the type that failed to match. Going to defer this to a future PR.
• [x] Implicitly generalizes type parameters in declarations.
• [x] Implicitly generalizes type parameters in the REPL.
• [x] Fixes #26.
• [x] Fixes #36.
• [x] Fixes #63.
• [x] Fixes #66.
• [x] Fixes #71.
• [x] Fixes #78.

There are some significant unknowns remaining:

• How can we integrate resource requirements into unification? Deferring this as well.

[robrix]

Well, the constraint solver infinite loops on Base.Vector and fails on Base.List, but I’m merging it anyway.