Mind blown today: Constraint generation + solving is *not* a requirement for implementing Hindley-Milner type checkers — metavariables + unification is enough!
Conversation
After a bit of digging by , it seems like one reason the approach of generating constraints was introduced was as a way to improving error messages. See “Generalizing Hindley-Milner Type Inference
Algorithms”, for example: cs.uu.nl/research/techr
1
1
9
Sadly constraint generation + solving has been a significant stumbling block for me when learning to implement type inference over the years. It shows up in many tutorials about type checking, which had led me to think it was somehow necessary for implementing it!
1
1
5
According to , constraint generation can also stop working for dependent type checking, as problems can pile up exponentially. Instead we should aim to get rid of unsolved problems as fast as possible.
1
3
Thanks for clearing up my original misconception! If you want to see some examples of implementing type inference for dependent types I highly recommend checking out Andras' elaboration-zoo repository:
