[GHC] #2235: Bogus occurs check with type families

[GHC]

#2235: Bogus occurs check with type families
-------------------------+--------------------------------------------------
    Reporter:  simonpj   |       Owner:         
        Type:  bug       |      Status:  new    
    Priority:  normal    |   Milestone:         
   Component:  Compiler  |     Version:  6.8.2  
    Severity:  normal    |    Keywords:         
  Difficulty:  Unknown   |    Testcase:         
Architecture:  Unknown   |          Os:  Unknown
-------------------------+--------------------------------------------------
 Consider this program, using type families:
 {{{
     data Even; data Odd

     type family Flip a :: *
     type instance Flip Even = Odd
     type instance Flip Odd = Even

     data List a b where
        Nil  :: List a Even
        Cons :: a -> List a b -> List a (Flip b)

     tailList :: List a b -> List a (Flip b)
     tailList (Cons _ xs) = xs
 }}}
 I get the error (from the HEAD)
 {{{
     Occurs check: cannot construct the infinite type: b = Flip (Flip b)
     In the pattern: Cons _ xs
     In the definition of `tailList': tailList (Cons _ xs) = xs
 }}}
 There's a bug here -- reporting an occurs check is premature.  We should
 really be able to infer the type
 {{{
    tailList :: (b ~ Flip (Flip b)) => List a b -> List a (Flip b)
 }}}
 But we get the same bogus occurs-check error with this signature.

 This example also illustrates why we might want closed families.  If you
 look at the type constraints arising from tailList you'll see that you get
 `(c ~ Flip b, b ~ Flip c)`
 where c is the existential you get from the GADT match. Now, ''we'' know
 that `b = Flip (Flip b)` is always true, but GHC doesn't. After all, you
 could add new type instances
 {{{
         type instance Flip Int = Bool
         type instance Flip Bool = Char
 }}}
 and then the equation wouldn't hold. What we really want is a *closed*
 type family, like this
 {{{
         type family Flip a where
                 Flip Even = Odd
                 Flip Odd = Even
 }}}
 (preferably supported by kinds) and even *then* it's not clear whether
 it's reasonable to expect the compiler to solve the above problem by
 trying all possiblities.  This relates to #2101

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