Injective type families?
conal at conal.net
Mon Feb 14 22:28:37 CET 2011
Is there a way to declare a type family to be injective?
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Glasgow-haskell-users