[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 checker)    |          Version:  7.8.2
      Resolution:                             |         Keywords:
Operating System:  Unknown/Multiple           |     Architecture:
 Type of failure:  GHC rejects valid program  |  Unknown/Multiple
       Test Case:                             |       Difficulty:  Unknown
        Blocking:                             |       Blocked By:
                                              |  Related Tickets:
----------------------------------------------+----------------------------

Comment (by haasn):

 Here's an updated example that fails. It seems the issue is more
 complicated, GHC picks the right case in the latter examples (regardless
 of order), but it fails on either ‘bar’ or ‘foo’ depending on the order of
 the cases in the type family Bad.

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

 type family Bad a b where
   Bad (m a -> b) a = b
   Bad (a   -> b) a = b

 foo :: Monad m => (m a -> b) -> a -> Bad (m a -> b) a
 foo f a = f (return a)

 bar :: (a -> b) -> a -> Bad (a -> b) a
 bar f a = f a

 {-
 ctf.hs:11:11:
     Couldn't match expected type ‘Bad (a -> b) a’ with actual type ‘b’
       ‘b’ is a rigid type variable bound by
           the type signature for bar :: (a -> b) -> a -> Bad (a -> b) a
           at ctf.hs:10:8
     Relevant bindings include
       a :: a (bound at ctf.hs:11:7)
       f :: a -> b (bound at ctf.hs:11:5)
       bar :: (a -> b) -> a -> Bad (a -> b) a (bound at ctf.hs:11:1)
     In the expression: f a
     In an equation for ‘bar’: bar f a = f a
 Failed, modules loaded: none.
 -}

 -- But this type-checks just fine:

 type family Bad' a b where
   Bad' (m a -> b) a = True
   Bad' (a   -> b) a = False

 foo' :: (Monad m, Bad' (m a -> b) a ~ True) => (m a -> b) -> a -> b
 foo' f a = f (return a)

 bar' :: Bad' (a -> b) a ~ False => (a -> b) -> a -> b
 bar' f a = f a
 }}}

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