id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc	os	architecture	failure	difficulty	testcase	blockedby	blocking	related
1807	type equality coercions not symmetric + order dependent	guest	chak	"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)
}}}"	bug	closed	normal	6.10 branch	Compiler (Type checker)	6.8	duplicate	type equality coercions symmetry order constraints	rturk@…	Unknown/Multiple	Unknown/Multiple		Unknown