(a) we can't specify that two types in an instance are not equal;
but we can use overlap resolution to ensure that equal types are handled by another, more specific instance ... permit type inequalities as guards in instance declarations:
<topdecls> -> .. | 'instance' [<ctxt> '=>'] <head> [ '|' <ineqs> ] [<body>]
<ineqs> -> <typevar> '/=' <type> [ ',' <ineqs>]
first, I need to point out an oversight of mine here: restricting the lhs of inequalities to typevars was meant to simplify the semantics, but if we do that, we also need disjunctions of inequalities (eg, the negation of (a,b)==(Int,Bool) is (a/=Int || b/= Bool) ). that is not an unnatural requirement, but no longer simpler than just stating the full inequality ( (a,b)/=(Int,Bool) ). so I'm no longer sure which alternative to prefer?
I'm afraid things might be a bit more complex. First of all, we may
great, a second reader!-) about time that someone started to raise issues. that can only be helpful. yes, there are different variations on equality and disequality. your examples on equalities seem to hinge on the question of whether or not to permit substitutions, so we'd get unification (substitutions on both sides), matching (substitution on one side), equality (no substitutions). you also mention the possibility of asking for substitutions that make two types unequal (instead of asking for substitutions that make two types equal, then negating the result), but I'll take that as a general remark (useful when one needs to demonstrate that two terms are separable by substitution), not as something specifically relevant for the present context. for negated equalities, the difference between permitting or not permitting variable substitutions in the equality check is reversed: unification equates more terms than syntactic equality, so negated unification rejects more term pairs than negated syntactic equality. however, we also need to take into account that in our current context syntactic equality should cause residuation rather than giving the answer false for terms involving variables: - consider a/=Int (that is: not (a=Int)). with negated unification, this guard fails, because a could be instantiated to Int, so a rule with this guard won't apply. but if a is later instantiated to Bool by some FD, the guard becomes Bool/=Int, which succeeds, so the rule is now applicable. if a is instead instantiated to Int, the guard becomes Int/=Int, which fails. with negated equality, this guard cannot be decided, so the decision is delayed (residuation). if a is later instantiated to Bool, the guard is woken up, and succeeds, so the rule is now applicable. if a is instead instantiated to Int, the guard is woken up, and fails, so the rule is no longer applicable. - consider a/=b (that is: not (a=b)). with negated unification, this guard fails, because either variable could be instantiated to the other, so a rule with this guard won't apply. if the variables are instantiated later, the guard will change, and rule applicability changes. with negated equality, this guard cannot be decided, so the decision is delayed. if a or b are instantiated later, the guard is woken up, and retried. comparisons of more complicated structures reduce to these and ground comparisons. so it looks as if there isn't that much difference, but we need to be careful about when rules are suspended/woken up, or fail and are retried, and when guards are decided. so we certainly need to be careful about which disequality to choose as default, even if we are only interested in replacing overlaps. I'm not yet decided about which one is the "right" default for our problem. (of course, one might want to permit others, but I'm only looking for one at the moment;-).
variables. Does 'a' equal to 'b'? It depends. We may define two types t1 and t2 dis-equal if in any possible interpretation (for any assignment to type variables that may occur free in t1 and t2) the types are syntactically dissimilar. Under this definition, 'a' is not equal to 'b'. OTH, we may say that two types are disequal if there exists an interpretation (i.e., an assignment to type variables) that makes the types dissimilar. Both definitions can be useful, in different circumstances.
these two variations appear to be the same, though?
The _full_ HList technical report discusses these issues in detail (Section 9 and Appendix D).
and many other issues relevant to the present discussion. I've already referred to it as being full of examples illustrating why the current situation is unacceptable, and had been hoping that the authors would be among those arguing in favour of searching a more consistent picture here and now, avoiding the need for such hacks. after all, that's what you wrote at the end of Appendix D, two years ago!-) cheers, claus btw, said appendix D compares typeCast :: TypeCast a b => a -> b (with FDs: a ->b, b -> a) to foo :: a -> b foo x = x which might be slightly misleading in that the former does not have two independent type variables (once either is determined, the other is, too), and the second has a complete type declaration that conflicts with the inferred type (if, on the other hand, the type declaration was partial, it could be refined to the inferred type). apart from that, I'd agree with the argument: there is a difference between FDs excluding type errors a priori and FDs determining types that may or may not match with the actual types they are compared with. the latter is often more expressive/useful.