[GHC] #7804: Ambiguity check too eager in presence of RankNTypes and TypeFamilies

[GHC]

#7804: Ambiguity check too eager in presence of RankNTypes and TypeFamilies
--------------------------------------+-------------------------------------
Reporter:  goldfire                   |          Owner:                  
    Type:  bug                        |         Status:  new             
Priority:  normal                     |      Component:  Compiler        
 Version:  7.7                        |       Keywords:  AmbiguityCheck  
      Os:  Unknown/Multiple           |   Architecture:  Unknown/Multiple
 Failure:  GHC rejects valid program  |      Blockedby:                  
Blocking:                             |        Related:                  
--------------------------------------+-------------------------------------
 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}}}.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7804>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler