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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe