Rigid vars allowed to escape their scope

[iitalics]

Rigid variables can escape their scope:

#lang hackett
(def weird
  (λ (x)
    (: (λ (y) (if True x y))
       (∀ (A) (-> A A)))))
;;;
> (#:type weird)
: (forall (A1618) {A9 -> A1618 -> A1618})

Weird scenarios can arise when rigid variables escape their scope. Here, A9 refers to a out-of-scope rigid variable. It will fail to unify with anything else but it is clearly not bound by the final forall.

The algorithm in Complete and Easy Bidirectional Typechecking prevents this by keeping a close eye on the scopes of rigid and solver variables.

[lexi-lambda]

I dropped the skolem escape check from the previous implementation because I clearly wasn’t doing it correctly, but I wasn’t sure precisely how to do it properly. I agree that it’s a bug that Hackett doesn’t properly check for skolem escapes. However, I’m not completely sure when it’s appropriate to perform the check.

A simple check that would catch your program would be to ensure rigid variables are never quantified over during generalization, but this seems like it might be too permissive? I’ve struggled to find a good treatment in the literature of the problem of skolem escape.

[iitalics]

The way that Complete and Easy Bidirectional Typechecking handles this is by having rigid variables and solver variables in the same ordered context, and maintaining the invariant that solver variables are never instantiated to variables introduced after them; an attempt to do so results in a type error.

Granted, I'm not sure where this error comes up without intentionally provoking the typechecker.

[lexi-lambda]

My interpretation of the Complete and Easy paper is that the ordered context is quite useful for proving properties of their system, which they care a lot about. It does not seem very useful for actually implementing a practical type system because maintaining the necessary invariants is somewhat fragile in the face of extension. The paper takes great care to insert into the context in specific places, which I imagine they spent a great deal thinking about and picking to make their proofs as easy to specify as possible, but a real language is more complicated, and it doesn’t seem worth the balancing act.

Other typecheckers, such as GHC and PureScript, perform skolemization and check for skolem escape without the use of an ordered context. I think it would be worth understanding what they do in more detail. I’ve looked at the PureScript code before, but I did not feel like I fully understood the details. That said, perhaps what was in Hackett before is actually not too far from the right thing, and it should just be reinstated in a more careful way.