Injective type families?
john at repetae.net
Mon Feb 14 22:41:17 CET 2011
Isn't this what data families (as opposed to type families) do?
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
> 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
More information about the Glasgow-haskell-users