[GHC] #9082: Unexpected behavior involving closed type families and repeat occurrences of variables

[GHC]

#9082: Unexpected behavior involving closed type families and repeat occurrences
of variables
-------------------------------------+-------------------------------------
       Reporter:  haasn              |             Owner:
           Type:  bug                |            Status:  new
       Priority:  normal             |         Milestone:
      Component:  Compiler (Type     |           Version:  7.8.2
  checker)                           |  Operating System:  Unknown/Multiple
       Keywords:                     |   Type of failure:  GHC rejects
   Architecture:  Unknown/Multiple   |  valid program
     Difficulty:  Unknown            |         Test Case:
     Blocked By:                     |          Blocking:
Related Tickets:                     |
-------------------------------------+-------------------------------------
 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?

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