Injective type families?

[John Meacham]

Isn't this what data families (as opposed to type families) do?

    John

On Mon, Feb 14, 2011 at 1:28 PM, Conal Elliott <conal at conal.net> wrote:
> 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
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>