Higher-rank types and constraint generation in GHC

Learn
1

Hi all, I’m trying to build an intuition for constraint generation as the primary mode of type inference / elaboration for a compiler that I’m working on. From what I’ve read in OutsideIn(X), GHC’s mechanisms for it remain untouched so I took a look:

8.2 Brief sketch of the implementation
[…] bidirectional propagation of type information needed to support higher-rank
inference remains untouched

My high-level understanding right now is that skolemisation (through topSkolemise) may or may not emit an implication constraint depending on if there were skolemised variables or “given” constraints. I was thinking about how it would look like in a program:

runST :: forall a. (forall r. ST r a) -> a
action :: forall r. ST r Int

-- check(runST action)
runST :: (forall r. ST r ?a) -> ?a
action :: ST ?r Int

ST ?r Int < forall r. ST r ?a

-- Generates the ff. implication constraint:
∀r. [] => [ ?r ~ r, ?a ~ Int ]

-- ?a ~ Int can be promoted, thus:
?a ~ Int
∀r. [] => [ ?r ~ r ]

What I’m not sure of is how the final constraint after floating can be solved… ?r is untouchable because its ambient level is lower than that of the implication constraint. One thought I have at the moment is that maybe I’m instantiating the r from action too eagerly, and that it could instead look more like:

-- Given the ambient level 1:

runST :: (forall r. ST r ?a[1]) -> ?a[1]
action :: forall r. ST r Int

-- In the following subsumption, we'll skolemise the RHS.
-- Skolemisation increases the ambient level from 1 to 2.
forall r. ST r Int < forall r. ST r ?a

-- Then, this subsumption would instantiate the LHS.
forall r. ST r Int < ST #r ?a

-- Thus, given the subsumption:
ST ?r[2] Int < ST #r ?a[1]

-- We'll generate the implication constraint:
∀r[2]. [] => [ ?r[2] ~ r, ?a[1] ~ Int ]

-- ?a[1] ~ Int can be promoted again:
?a[1] ~ Int 
∀r[2]. [] => [ ?r[2] ~ r ]

The final implication constraint can be solved as is because ?r has the same level as #r now.

1 Like
2

To infer the type of applications it is useful to have some bidirectional type inference going on. Purely constraint-generation-based type inference naively recurses into the subterms of an application, with the problematic consequence that you pointed out: we may end up generating unification variables in the wrong scope.

To type an application f x, we infer the type of the function f, which should be of the form t -> u, and we check x against t, which peels forall type variables off the top of t before coming back to descend into x.

On top of that basic idea, it’s convenient to view applications as an n-ary construct, fun x y z so that you can unify the result type of fun with the expected type of the whole application before checking the arguments.

You can see this in action in GHC, in the function tcApp, with the steps neatly spelled out (notably: splitting the application, getting the type of the head, and using it for checking the arguments).

The comments reference the QuickLook paper a lot, but the relevant typing rule in there is quite daunting, all to solve a different issue beyond just higher-rank types. The paper Practical type inference for arbitrary-rank types contains more digestible information about your problem.

5 Likes
3

Thanks for the pointers! I’m currently reading through that paper as well as the Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism paper.

I actually implemented a type checker based on the latter a while back and it wasn’t until I came across this problem that it clicked how proper scoping plays a role in checking higher rank polymorphism.

1 Like