Ambiguity check too eager with unconstrained type variable

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 (closed)) 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.

Trac metadata

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