I am self-teaching myself Hindley-Milner type inference by writing my own implementation, separating tree traversal and constraint solving. The tutorials that I've been following only allow patterns that are variables, but I decided to implement pattern matching, and I've hit a wall concerning the separation of traversal and unification when inferring the pattern types.
My tree traversal phase maintains an "environment," a mapping of identifiers to polytypes. Patterns can introduce new bindings into the environment.
Given a let expression
let id = expr in body, the tutorials that I follow compute
id's polytype by generalizing
expr's type with the current typing context, quantifying over all tvars not defined in the environment.
However, if non-identifier patterns are allowed, unification must be done in order to give identifiers in the pattern type schemes. For example, given
let (a, b) = foo in body
a the tvar
b the tvar
foo some monotype
t3 must be unified with
(t0, t1) in order to give
b the correct monotypes to generalize, at least to my understanding. Is it possible to me to separate constraint collection and unification when supporting patterns in my language, and if so, how? Thank you in advance!
For context, I am a high-school student not formally educated in computer science.