On Thu, May 20, 2010 at 11:54 AM, Daniel Fischer
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 ... 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. ... 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?
Then (F a b, O a)=>Bool is ambiguous. There are two substitutions that unify (F a b, O a) with instances in the current context.
Using the available instances to resolve overloading is a tricky thing, it's very easy to make things break that way.
Using the available instances is the natural, in fact the only way, to resolve overloading. Our proposal cannot make any well-typed program break, any program whatsoever. What it can do is to make programs that *were not well-typed* --- because there existed an ambiguity error --- to be either: i) well-typed (because overloading is resolved), or ii) not well-typed (because overloading cannot in fact be resolved), and in this case the ambiguity error may be deferred, to the point where the unreachability occurs, if there was a FD annotated. Cheers, Carlos