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?

Using the available instances to resolve overloading is a tricky thing,
it's very easy to make things break that way.