On Thu, May 20, 2010 at 11:54 AM, Daniel Fischer <daniel.is.fisc...@web.de>wrote:
> > 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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe