Isn't this what data families (as opposed to type families) do? John
On Mon, Feb 14, 2011 at 1:28 PM, Conal Elliott <co...@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@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users