unification via Eq does not work for Label/Tag

[GoogleCodeExporter]

Compile this snippet:

{{{
---------------------------------
mergeTags :: Tag ~> Tag ~> Tag
{mergeTags a a} = a

tryMergeLabels :: Label a -> Label b -> (Label a + Label {mergeTags a b})
tryMergeLabels a b = case labelEq a b of
                     Just eq -> L b -- (L a) works!
                     Nothing -> R undefined
---------------------------------
}}}

I get:

**** Near line: 6 column: 22
The supposedly polymorphic type variable: _c,
is forced by context to be: _d
The var _c arose from the prototype: tryMergeLabels::Label _d -> Label _c
-> ((Label _d)+(Label {mergeTags _d _c}))
where types have kinds:
   _d:Tag
   _c:Tag
The var _d arose from the prototype: tryMergeLabels::Label _d -> Label _c
-> ((Label _d)+(Label {mergeTags _d _c}))
where types have kinds:
   _d:Tag
   _c:Tag
near line: 5 column: 1
 (Rigid 24495:(Con Tag@2 %Ox)) =/= (Rigid 24494:(Con Tag@2 %Ox))

when I add "theorem" to read:

I get:

**** Near line: 6 column: 22
{{{
                     Just eq -> L b where theorem eq
}}}
In a rewrite rule, the lhs must be a type-function call (like {plus x y}) or
a type-constructor application (like (Even x)), otherwise it can't be
used as a rewrite rule. This is not the case for:
  Equal _c _d

Original issue reported on code.google.com by ggr...@gmail.com on 5 Mar 2010 at 12:55

[GoogleCodeExporter]

similarly here
{{{
tryMergeLabels :: Label a -> Label b -> Maybe (Label {mergeTags a b})
tryMergeLabels a b = case labelEq a b of
                     Just eq -> Just a -- (Just undefined) works!!
                     Nothing -> Nothing
}}}

The unification cannot see inside and infer (Label a == Label b) from (a == b):

While type checking in the scope of:
   (Just eq)
We need to prove:
   Equal _c {mergeTags _c _d}
From the truths:
And the rules:S,Z,S,Z,
But, The equations: (_c={mergeTags _c _d}) =>  have no solution

This is ignoring the fact that _c == _d as witnessed by eq.

Original comment by ggr...@gmail.com on 5 Mar 2010 at 1:05