Either a b -> CoRec Identity [a,b] ?

[noinia]

I'm trying to write a function with the following type, which I seem unable to do:

fromEither :: Either a b -> CoRec Identity [a,b]

The following trivial implementation works, but I cannot get rid of the class constraint that b is an element of [a,b]:

fromEither           :: b  ∈ [a,b] => Either a b -> CoRec Identity [a,b]
fromEither (Left x)  = Col . Identity $ x
fromEither (Right x) = Col . Identity $ x

After fiddling a bit, it seems GHC has issues proving that.

RIndex b [a,b] ~ (S Z)

When we add that as a class constraint. GHC is clever enough to figure out the details. Also note that for concrete types a and b it can also figure out the details. However, for the polymorphic case it cannot. Any ideas on how to convince GHC to convert an Either to a CoRec without the class constraint?

[acowley]

One guess is that the trouble is due to GHC not knowing that a is not equal to b. The constraint on RIndex that you've worked out implies this. I'm not sure how to improve the situation.

[noinia]

Hmm that might be the case. I'll see if I can get something like ((a == b) == False ) as the constraint instead. Not that that improves the situation for the fromEither directly, but it might help in the underlying use case I have :).