- The types are too expressive (see previous post)
- Since the types are so complex, the solver gets hit with constraints leading to tens of thousands of type variables. This is mostly triggered by large initialization expressions like parser tables. Waiting 20 seconds to type a 40K file is not cool.
- I need to get back to work, i.e. I need to make some progress.
So after plugging away for a week or so, I've now run into a new problem - the value restriction. Something I've put off dealing with for a long time. Turns out the problem is classically triggered by type constructors for things like empty lists. For example, this types without any problems:
(cons 'a list)
(let ((l0 (list:nil)))
(set! l0 (list:cons 34 l0))
(list:cons #f l0)
[Note that the last line glues together a "list(bool)" onto a "list(int)"]
The solution is to restrict the polymorphism of assigned variables, hence the Value Restriction.