Injective type families?

[Conal Elliott]

Is there a way to declare a type family to be injective?

I have

> data Z
> data S n

> type family n :+: m
> type instance Z   :+: m = m
> type instance S n :+: m = S (n :+: m)

My intent is that (:+:) really is injective in each argument (holding the
other as fixed), but I don't know how to persuade GHC, leading to some
compilation errors like the following:

    Couldn't match expected type `m :+: n'
           against inferred type `m :+: n1'
      NB: `:+:' is a type function, and may not be injective

I realize that someone could add more type instances for (:+:), breaking
injectivity.

Come to think of it, I don't know how GHC could even figure out that the two
instances above do not overlap on the right-hand sides.

Since this example is fairly common, I wonder: does anyone have a trick for
avoiding the injectivity issue?

Thanks,  - Conal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20110214/0799904a/attachment.htm>