type equality coercions not symmetric + order dependent

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)

Trac metadata

Trac field	Value
Version	6.8
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	rturk@science.uva.nl
Operating system	Unknown
Architecture	Unknown