Ambiguity check too eager in presence of RankNTypes and TypeFamilies

The following code compiles in 7.6.1 but not in 7.7:

{-# LANGUAGE TypeFamilies, RankNTypes #-}

type family F f a
type family G f

data Proxy a = P

sDFMap :: (forall a. Proxy f -> Proxy a -> Proxy (F f a)) -> Proxy (G f)
sDFMap _ = P

Here is the error message:

    Couldn't match type `G f0' with `G f'
    NB: `G' is a type function, and may not be injective
    The type variable `f0' is ambiguous
    Expected type: (forall a. Proxy f -> Proxy a -> Proxy (F f a))
                   -> Proxy (G f)
      Actual type: (forall a. Proxy f0 -> Proxy a -> Proxy (F f0 a))
                   -> Proxy (G f0)
    In the ambiguity check for:
      forall f.
      (forall a. Proxy f -> Proxy a -> Proxy (F f a)) -> Proxy (G f)
    In the type signature for `sDFMap':
      sDFMap :: (forall a. Proxy f -> Proxy a -> Proxy (F f a))
                -> Proxy (G f)

It is true that sDFMap is sometimes ambiguous, but it is not always ambiguous. For example, if we have

foo :: Proxy Bool -> Proxy a -> Proxy (F Bool a)
foo _ _ = P

bar = sDFMap foo

the call to sDFMap is well defined, with f ~ Bool. If the type signature for foo did not specify the value of f, the call to sDFMap would indeed be ambiguous and should be rejected. GHC 7.6.1 does catch the error when the type of foo uses a variable instead of Bool.

Trac metadata

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