How to reproduce GHC's type error for a rigid type variable escaping its scope?

Question

Here is the canonical example for a rigid type variable escaping its scope:

{-# LANGUAGE RankNTypes #-}
runST :: forall a. (forall s. ST s a) -> a
runST _ = undefined

newRef :: forall s a. a -> ST s (Ref s a)
newRef _ = undefined

runST (newRef 'x') -- type error (rigid a would escape its scope)

I tried to reproduce the error by doing the unification/subsumption manually:

-- goal: unify the expression `runST (newRef 'x')`
fun :: (forall a. (forall b. Foo b a) -> a)
arg :: (forall c. Foo c (Bar c Char))
(forall b. Foo b a0) -> a0 -- meta-ize all tvs bound by the outermost quantifier
Foo s0 (Bar s0 Char) -- skolemize all tvs bound by the outermost quantifier
-- subsumption judgement: offered `arg` is at least as polymorphic as fun's requested argument:
Foo s0 (Bar s0 Char) <: (forall b. Foo b a0)
Foo s0 (Bar s0 Char) <: Foo s1 a0 -- skolemize on the RHS
Foo ~ Foo -- generativity of Foo
s0 ~ s1 -- injectivity of Foo's arguments
-- REJECTED: cannot instantiate `s0` with `s1`
-- we don't even reach the point where the escape check is taken place:
a0 ~ (Bar s0 Char) -- would fail due to s0 ~ s1

To my knowledge a rigid type variable (skolem constant) can only be subsumed under itself or be unified with a meta (unification) type variable that doesn't allow the former to escape its scope, i.e. the meta tv must not be free in the scope where the rigid tv was initially skolemized. Consequently, s0 ~ s1 should be rejected, because two distinct skolems cannot be instantiated, right?

However, as I interpret the error message GHC reaches the escape check. Are my unification steps wrong or do I misinterpet the error message?

My only idea so far: Skolems behave differently during type inference/generalisation on the one hand and in the event of application.on the other hand. In the latter case they are less rigid, i.e. can be specialized. — Iven Marquardt
Not sure exactly what system this is, but it seems off to skolemise the argument in the application judgement. If you instantiate it instead, you end up checking e.g. Foo a1 (Bar a1 Char) against Foo s1 a0, which gives a1 = s1 and a0 = Bar a1 Char, and the error is that s1 occurs in the fully substituted Bar s1 Char. (There is no s0, I just left your names the same to avoid confusion.) — Jon Purdy
@Jon I agree, skolemization before subsumption has started doesn't make sense. Strangly enough, my algorithm worked for over 20 different unifications, that is obtained similar results as GHC. Thank you very much! — Iven Marquardt

Jon Purdy Jon Purdy · Accepted Answer · 2021-03-07T22:27:25

Writing my comment out as an answer since I guess it helped. :)

I believe your error was in skolemising the argument in the application; instead, it should be instantiated with a fresh metavariable (I’ll write a circumflex for metavars and bold for skolem constants):

fun : ∀a. (∀b. Foo b a) → a

arg : (∀c. Foo c (Bar c Char))

[â₀/a]((∀b. Foo b a) → a) = (∀b. Foo b â₀) → â₀

~~Foo c (Bar c Char)~~

[â₁/c](Foo c (Bar c Char)) = Foo â₁ (Bar â₁ Char)

Then, in the subtyping judgement:

… ⊢ Foo â₁ (Bar â₁ Char) ≤: ∀b. Foo b â₀

You still skolemise the ∀-bound variable on the right side as usual:

…, b ⊢ Foo â₁ (Bar â₁ Char) ≤: Foo b â₀

This gives Foo = Foo by generativity, but solves â₁ to b by injectivity, and solves â₀ to Bar â₁ Char. This then correctly gives an occurs check failure when exiting the scope of the quantifier, since the substituted type [â₁=b](Bar â₁ Char) = Bar b Char contains the skolem constant b.

I say “skolemise” because this does introduce a type constant, but it can also be thought of as just entering the scope of a quantifier (as in “Complete and Easy”), not necessarily performing deep skolemisation.

How to reproduce GHC's type error for a rigid type variable escaping its scope?

1 Answers