[GHC] #7812: Ambiguity check too eager with unconstrained type variable

[GHC]

#7812: Ambiguity check too eager with unconstrained type variable
-----------------------------+----------------------------------------------
Reporter:  goldfire          |          Owner:                         
    Type:  bug               |         Status:  new                    
Priority:  normal            |      Component:  Compiler (Type checker)
 Version:  7.7               |       Keywords:  AmbiguityCheck         
      Os:  Unknown/Multiple  |   Architecture:  Unknown/Multiple       
 Failure:  None/Unknown      |      Blockedby:                         
Blocking:                    |        Related:                         
-----------------------------+----------------------------------------------
 Consider the following code:

 {{{
 {-# LANGUAGE TypeFamilies, DataKinds, GADTs #-}

 type family F (b :: Bool) a
 type instance F False a = a
 type instance F True a = Int

 data SBool :: Bool -> * where
   SFalse :: SBool False
   STrue :: SBool True

 foo :: SBool b -> [F b a]
 foo _ = []
 }}}

 GHC 7.6.1 compiles this code without a problem, and both {{{foo STrue}}}
 and {{{foo SFalse}}} are well typed and evaluate to {{{[]}}}. HEAD (even
 after yesterday's ambiguity patch for #7804) does not compile this code,
 complaining about ambiguity. Here is the error:

 {{{
     Couldn't match type ‛F b a0’ with ‛F b a’
     NB: ‛F’ is a type function, and may not be injective
     The type variable ‛a0’ is ambiguous
     Expected type: SBool b -> [F b a]
       Actual type: SBool b -> [F b a0]
     In the ambiguity check for:
       forall (b :: Bool) a. SBool b -> [F b a]
     In the type signature for ‛foo’: foo :: SBool b -> [F b a]
 }}}

 This is admittedly a weird corner case, but it's one I've run into in
 real(ish) code. On first glance, the type variable {{{a}}} really is
 ambiguous in the type signature for {{{foo}}}. But, it turns out that this
 is a benign ambiguity, because the variable is either ignored or, after
 type family simplification, appears in an inferrable location within the
 type.

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