Improving GHC's constraint solving

So I’ve been here at MSR Cambridge for almost two weeks now (!), working in the Programming Principles and Tools Group with Simon Peyton-Jones and Dimitrios Vytiniotis — and also collaborating with Stephanie Weirich and Steve Zdancewic, who are also in Cambridge. So, what have I been doing?

This week, Simon, Dimitris, and I have been having a major GHC hacking session, implementing the new constraint-solving type inference engine described in their new OutsideIn(X) paper. It’s been a lot of fun — I’ve never hacked on GHC before, and it’s quite a new experience hacking on such a large (and amazing) piece of software. I’ve been working on the constraint canonicaliser, which puts constraints into canonical forms appropriate for the constraint simplifier to work with. As a simple example, the equality constraint (Int, a) ~ (b, Char) gets decomposed into the primitive constraints Int ~ b and a ~ Char. It’s also responsible for flipping and flattening equality constraints so that type function applications only happen on the left-hand side: for example, the constraint F a b ~ G Int (where both F and G are type families), gets rewritten to a pair of constraints F a b ~ c, G Int ~ c, where c is a fresh variable. If we didn’t do this it would lead to problems with termination: for example, the constraint a ~ [F a] could lead to infinite rewriting of a to [F a] to [F [F a]] to… (And before you protest that we ought to just throw out a ~ [F a] on the grounds that it is recursive, note that F a may not mention a at all; for example, perhaps F is defined by F [x] = Int.)

Constraints also include type class constraints and implicit parameter constraints, although there’s much less work to do with those as far as canonicalisation is concerned.

Next week, I’ll likely get back to our other, more ambitious research project, but I’ll write more about that next time. In the meantime, if you’re in or near Cambridge and want to meet up, just drop me a note!