On Thursday 20 May 2010 16:34:17, Carlos Camarao wrote:
In the context of MPTCs, this rule alone is not enough. Consider, for example (Example 1):
class F a b where f:: a->b class O a where o:: a and k = f o:: (C a b,O a) => b
Type forall a b. (C a b,O a) => b can be considered to be not ambiguos, since overloading resolution can be defined so that instantiation of "b" can "determine" that "a" should also be instantiated (as FD b|->a does), thus resolving the overloading.
<snip>
Our proposal is: consider unreachability not as indication of ambiguity but as a condition to trigger overloading resolution (in a similar way that FDs trigger overloading resolution): when there is at least one unreachable variable and overloading is found not to be resolved, then we have ambiguity. Overloading is resolved iff there is a unique substitution that can be used to specialize the constraint set to one, available in the current context, such that the specialized constraint does not contain unreachable type variables. (A formal definition, with full details, is in the cited SBLP'09 paper.)
Consider, in Example 1, that we have a single instance of F and O, say:
instance F Bool Bool where f = not instance O Bool where o = True
and consider also that "k" is used as in e.g.:
kb = not k
According to our proposal, kb is well-typed. Its type is Bool. This occurs because (F a b, O a)=>Bool can be simplified to Bool, since there exists a single substitution that unifies the constraints with instances (F Bool Bool) and (O Bool) available in the current context, namely S = (a|->Bool,b|->Bool).
But then somebody defines instance F Int Bool where f = even instance O Int where o = 0 What then? Using the available instances to resolve overloading is a tricky thing, it's very easy to make things break that way.