What is the cause of this mysterious Haskell type error involving reflection?

Question

I was playing with the Haskell reflection package, and I ran into a type error I do not fully understand. First, I tried to write the following function, which happily typechecks:

{-# LANGUAGE TypeApplications #-}

reifyGood :: (forall s. Reifies s a => Proxy a) -> ()
reifyGood p = reify undefined (\(_ :: Proxy t) -> p @t `seq` ())

Interestingly, however, this slightly different program does not typecheck:

reifyBad :: (forall s. Reifies s s => Proxy s) -> ()
reifyBad p = reify undefined (\(_ :: Proxy t) -> p @t `seq` ())

• Could not deduce (Reifies s s) arising from a use of ‘p’
  from the context: Reifies s a0
    bound by a type expected by the context:
               Reifies s a0 => Proxy s -> ()
• In the first argument of ‘seq’, namely ‘p @t’
  In the expression: p @t `seq` ()
  In the second argument of ‘reify’, namely
    ‘(\ (_ :: Proxy t) -> p @t `seq` ())’

The expressions are identical, but note the difference between the type signatures:

reifyGood :: (forall s. Reifies s a => Proxy a) -> ()
reifyBad  :: (forall s. Reifies s s => Proxy s) -> ()

I find this curious. At first glance, this is invalid because, in the second example, the skolem s would escape its scope. However, this is not actually true—the error message never mentions skolem escape, in contrast with this slightly different program:

reifyBad' :: (forall s. Reifies s s => Proxy s) -> ()
reifyBad' p = reify undefined (\(_ :: Proxy t) -> p @t) `seq` ()

• Couldn't match expected type ‘t0’ with actual type ‘Proxy s’
    because type variable ‘s’ would escape its scope
  This (rigid, skolem) type variable is bound by
    a type expected by the context:
      Reifies s a0 => Proxy s -> t0
• In the expression: p @t
  In the second argument of ‘reify’, namely
    ‘(\ (_ :: Proxy t) -> p @t)’
  In the first argument of ‘seq’, namely
    ‘reify undefined (\ (_ :: Proxy t) -> p @t)’

So perhaps something else is at play here.

Examining the type of reify, it becomes a little clear that something is amiss:

reify :: forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r

The scopes of a and s are clearly different, so it seems to make sense that GHC would not allow them to unify. However, it seems something about the local equality constraint introduced by the functional dependency on Reifies causes some sort of odd behavior. Interestingly, this pair of functions typechecks:

foo :: forall a r. Proxy a -> (forall s. (s ~ a) => Proxy s -> r) -> r
foo _ f = f Proxy

bar :: (forall a. Proxy a) -> ()
bar p = let p' = p in foo p' (\(_ :: Proxy s) -> (p' :: Proxy s) `seq` ())

…but removing the equality constraint in the type signature of foo makes them fail to typecheck, producing a skolem escape error:

• Couldn't match type ‘a0’ with ‘s’
    because type variable ‘s’ would escape its scope
  This (rigid, skolem) type variable is bound by
    a type expected by the context:
      Proxy s -> ()
  Expected type: Proxy s
    Actual type: Proxy a0
• In the first argument of ‘seq’, namely ‘(p' :: Proxy s)’
  In the expression: (p' :: Proxy s) `seq` ()
  In the second argument of ‘foo’, namely
    ‘(\ (_ :: Proxy s) -> (p' :: Proxy s) `seq` ())’

At this point, I’m perplexed. I have a couple (highly related) questions.

1. Why does reifyBad fail to typecheck in the first place?

2. More specifically, why does it produce a missing instance error?

Moreover, is this behavior expected and well-defined, or is it merely a strange edge case of the typechecker that happens to produce this particular result?

Answer 1

reify :: forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r

The skolem requirement essentially states that r in the type above can not depend on the s which is being quantified in the second argument. Otherwise, indeed it would "escape" its scope since reify returns r.

In

reifyBad :: (forall s. Reifies s s => Proxy s) -> ()
reifyBad p = reify undefined (\(_ :: Proxy t) -> p @t `seq` ())

we see that the second argument of reify is \(_ :: Proxy t) -> p @t `seq` (), so the type r would be return type of that function, which is (). Since r ~ () does not depend on s, there's no escaping problem here.

However, p @t according to the type of p requires Reifies t t. Since reify will choose t ~ s, the constraint is the same as Reifies s s. Instead, reify only provides Reifies s a where a is the type of undefined.

The subtle point here is that, while undefined can produce any type a, the type checker can not unify s and a. This is because a function with the same type as reify is entitled to receive only one value of a fixed (rigid) type a, and then choose as many types s as wanted. Unifying all such ss with a single a would be wrong, effectively constraining the choice of s by reify.

Instead, in the variant

reifyBad' :: (forall s. Reifies s s => Proxy s) -> ()
reifyBad' p = reify undefined (\(_ :: Proxy t) -> p @t) `seq` ()

here r is inferred to be the return type of \(_ :: Proxy t) -> p @t, which is Proxy t, where t ~ s. Since r ~ Proxy s does depend on s, we trigger a skolem error.