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

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?

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]((∀b. Foo b a) → a) = (∀b. Foo b â₀) → â₀

Foo c (Bar c Char)

[â₁/c](Foo c (Bar c Char)) = Foo â₁ (Bar â₁ Char)

Then, in the subtyping judgement:

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

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

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

This gives Foo = Foo by generativity, but solves â₁ to b by injectivity, and solves â₀ to Bar â₁ Char. This then correctly gives an occurs check failure when exiting the scope of the quantifier, since the substituted type [â₁=b](Bar â₁ 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.