Unification under a forall doesn't allow full constraint solving

As mentioned on the glasgow-haskell-users mailinglist, I'm working on a new design of monad-control. However I get a type error I don't understand. Here's an isolated example:

{-# LANGUAGE UnicodeSyntax, RankNTypes, TypeFamilies #-}

class MonadTransControl t where
  type St t ∷ * → *

  liftControl ∷ Monad m ⇒ (Run t → m α) → t m α

  restore ∷ Monad o ⇒ St t γ → t o γ

type Run t = ∀ n β. Monad n ⇒ t n β → n (St t β)

foo :: (Monad m, MonadTransControl t) => (Run t -> m α) -> t m α
foo f = liftControl f

Type checking foo this gives the following error:

   Couldn't match expected type `Run t' with actual type `Run t'
   Expected type: Run t -> m α
     Actual type: Run t -> m α
   In the first argument of `liftControl', namely `f'
   In the expression: liftControl f

When I remove the type annotation of foo the program type checks. But when I ask ghci the type of foo it tells me it's the same type:

> :t foo
foo :: (Monad m, MonadTransControl t) => (Run t -> m α) -> t m α

Note that when I change the associated type synonym to a associated data type the error disappears.

Is this a bug in GHC?

I'm using ghc-7.2.1.

Trac metadata

Trac field	Value
Version	7.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture