Improve type inference

[ethanuppal]

The current type inference and constraint setup is very limiting. In particular:

1. It doesn't carry through much lexical information, leading to less-than-ideal error messages (see #2).
2. It only allows constraints for type equality.

In fixing 2, there would be type classes and type/numeric parameters. The current setup with arrays and array literals involves a magic ARRAY_TYPE_UNKNOWN_SIZE constant. It would be better if an array was declared as a parametric type over its size. In order to handle type classes, the constraint system would need to extend to be able to prove derivation of a type or type class from another type class in addition to equality between types. (Side note: type classes as first class???)

[ethanuppal]

I aim to prove the following kinds of theorems (forgive the heterogenous notation):

• type $A$ is equal to type $B$ (unification algorithm)
• type $A$ is of class $\Gamma$
• where-clauses: e.g., "A[N] = B[M] where $N = M$", "A[N] where $N > 4$", etc. These should enable constraints on sub-terms as well, even theorems like "HashMap<A, B> where $A : \mathsf{Hash}$"
• and more!

I will likely have to do research into the algorithms that implement the latter kinds of proofs. It is also necessary to determine how to encode lexical context into these theorems for useful error messages. To start, I will read more of Static Program Analysis.