>> Your proposal appears to allow /incoherent/ instance selection.
>> This means that an expression can be well-typed in one module, and
>> well-typed in another module, but have different semantics in the
>> two modules. For example (drawing from above discussion) :
>>
>> module C where
>>
>> class F a b where f :: a -> b
>> class O a where o :: a
>>
>> module P where
>> import C
>>
>> instance F Bool Bool where f = not
>> instance O Bool where o = True
>> k :: Bool
>> k = f o
>>
>> module Q where
>> import C
>> instance F Int Bool where f = even
>> instance O Int where o = 0
>> k :: Bool
>> k = f o
>>
>> module Main where
>> import P
>> import Q
>> -- (here, all four instances are in scope)
>> main = do { print P.k ; print Q.k }
>> -- should result, according to your proposal, in
>> -- False
>> -- True
>> -- , am I correct?
>
> If qualified importation of k from both P and from Q was specified, we
> would have two *distinct* terms, P.k and Q.k.