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 |