Is there a way to declare a type family to be injective?<br><br>I have<br><br>> data Z<br>> data S n<br><br>> type family n :+: m<br>> type instance Z :+: m = m<br>> type instance S n :+: m = S (n :+: m)<br>
<br>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:<br><br> Couldn't match expected type `m :+: n'<br>
against inferred type `m :+: n1'<br> NB: `:+:' is a type function, and may not be injective<br><br>I realize that someone could add more type instances for (:+:), breaking injectivity.<br><br>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.<br>
<br>Since this example is fairly common, I wonder: does anyone have a trick for avoiding the injectivity issue?<br><br>Thanks, - Conal<br>