Unexpected behavior involving closed type families and repeat occurrences of variables

I'd expect both of these to work fine, but GHC always picks the instance that is mentioned first:

{-# LANGUAGE TypeFamilies, DataKinds #-}

type family Bad a b where
  Bad (f a) a = False
  Bad a     a = True

bad :: ( Bad (f a) a ~ False
       , Bad a     a ~ True
       ) => ()
bad = ()

-- Swapping the lines around does not change the behavior much:

type family Bad' a b where
  Bad' a     a = True
  Bad' (f a) a = False

bad' :: ( Bad' (f a) a ~ False
        , Bad' a     a ~ True
        ) => ()
bad' = ()

{-

ctf.hs:7:8:
    Could not deduce (Bad a0 a0 ~ 'True)
    from the context (Bad (f a) a ~ 'False, Bad a a ~ 'True)
      bound by the type signature for
                 bad :: (Bad (f a) a ~ 'False, Bad a a ~ 'True) => ()
      at ctf.hs:(7,8)-(9,14)
    The type variable ‘a0’ is ambiguous
    In the ambiguity check for:
      forall (f :: * -> *) a.
      (Bad (f a) a ~ 'False, Bad a a ~ 'True) =>
      ()
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In the type signature for ‘bad’:
      bad :: (Bad (f a) a ~ False, Bad a a ~ True) => ()

ctf.hs:18:9:
    Could not deduce (Bad' (f0 a0) a0 ~ 'False)
    from the context (Bad' (f a) a ~ 'False, Bad' a a ~ 'True)
      bound by the type signature for
                 bad' :: (Bad' (f a) a ~ 'False, Bad' a a ~ 'True) => ()
      at ctf.hs:(18,9)-(20,14)
    The type variables ‘f0’, ‘a0’ are ambiguous
    In the ambiguity check for:
      forall (f :: * -> *) a.
      (Bad' (f a) a ~ 'False, Bad' a a ~ 'True) =>
      ()
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In the type signature for ‘bad'’:
      bad' :: (Bad' (f a) a ~ False, Bad' a a ~ True) => ()

-}

Trying to turn this into an open type family instead somewhat hints at the issue:

type family Bad'' a b :: Bool
type instance Bad'' a     a = True
type instance Bad'' (f a) a = False

{-

ctf.hs:58:15:
    Conflicting family instance declarations:
      Bad'' a a -- Defined at ctf.hs:58:15
      Bad'' (f a) a -- Defined at ctf.hs:59:15

-}

It seems like GHC thinks these two family definitions conflict, yet to me they seem distinct - as a type that would match both would imply f a ~ a and hence be infinite.

Can anybody offer insight into this issue?

Trac metadata

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