Start Solving For Type Variables (Locally)

[CodaFi]

Adds two new forms of shorthand for closures. This necessitated modeling type variables and starting the most rudimentary of solvers in the TypeChecker.

YOUR PARSER MAKES TYPE VARIABLES, I HOPE YOU'RE HAPPY

[CodaFi]

Hm, so this removes the ability to "coerce".

[segiddins]

Can you also add an example to demonstrate what this will allow?

[segiddins]

Pardon my ignorance, but what's the benefit of propagating the canonical types directly?

[CodaFi]

Propagating sugar down the context is better for debugging, but means every access to the type needs to be guarded by a canonicalize call. Really, it's a modeling problem. We should be able to retain annotated types and all their sugar, solve constraint systems with canonical types, then apply and get rid of the propagation call.

[harlanhaskins]

I actually think we should remove that. It makes type checker errors worse by stripping the sugar in diagnostics.

[harlanhaskins]

I eventually want to be able to say:

error: cannot convert value of type 'Foo' (aka 'Array<(Int, String)>') to type 'Bar' (aka String)

[CodaFi]

Starting work on the solver. We're going OutsideIn light (no GADTs, no existentials, no generalization).

[CodaFi]

@segiddins I appreciate the review, but nothing here works yet!

[segiddins]

Understood, just trying to understand it 😅