[GHC] #1807: type equality coercions not symmetric + order dependent

[GHC]

#1807: type equality coercions not symmetric + order dependent
--------------------------------------+-------------------------------------
  Reporter:  guest                    |          Owner:                                                    
      Type:  bug                      |         Status:  new                                               
  Priority:  normal                   |      Milestone:                                                    
 Component:  Compiler (Type checker)  |        Version:  6.8                                               
  Severity:  normal                   |       Keywords:  type equality coercions symmetry order constraints
Difficulty:  Unknown                  |             Os:  Unknown                                           
  Testcase:                           |   Architecture:  Unknown                                           
--------------------------------------+-------------------------------------
 I'm not entirely sure this is a bug, but it seems pretty weird behaviour:

 `a ~ b` cannot always be replaced by `b ~ a`

 `a ~ b, c ~ d` cannot always be replaced by `c ~ d, a ~ b`

 {{{
 {-# LANGUAGE TypeFamilies, GADTs #-}
 module Test where

 data List n where
     -- Works
     --Cons :: (Maybe n ~ n') => List n -> List n'
     --Cons :: (Maybe n ~ n', n' ~ Maybe n) => List n -> List n'

     -- Fails
     Cons :: (n' ~ Maybe n) => List n -> List n'
     --Cons :: (n' ~ Maybe n, Maybe n ~ n') => List n -> List n'

 class Snoc i where
     snoc :: List i -> List (Maybe i)

 instance Snoc i => Snoc (Maybe i) where
     snoc (Cons xs) = Cons (snoc xs)
 }}}

 This module compiles fine with both 6.8.0.20071025 and 6.9.20071025 using
 one of the first two Constructors. With either of the last two
 constructors both versions say:

 {{{
     Could not deduce (Snoc n) from the context ()
       arising from a use of `snoc' at Test.hs:17:27-33
     Possible fix: add (Snoc n) to the context of the constructor `Cons'
     In the first argument of `Cons', namely `(snoc xs)'
     In the expression: Cons (snoc xs)
     In the definition of `snoc': snoc (Cons xs) = Cons (snoc xs)
 }}}

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