Oh then you're right: my very goal was to propose something incoherant! That's the restriction that I don't like!
I'm not even sure of this, upon reflexion. If the language gives up global coherance, to remain sound I think it is sufficient (and necessary) to desugarize type bounds in function signatures or in type parameters as being plain instances of the said bounds.
Just to make things clear I suppose we have a function + on instances that merges the two instances so that if Inst1: Trait1 and Inst2: Trait2 then Inst1 + Inst2: Trait1 + Trait2 and also I'll use Trait<Self=T> to have a syntax a bit more logical for constraining the implicit Self parameter.
So naming things completely (remember, you can specify things like this but you could also implicit use and have the same lightweight code as before with local canonicity), a particular instance of the type HashMap<K: Eq + Hash, V> could be HashMap<String::eq + String::hash, V> where String::eq: Eq<Self=String> and String::hash: Hash<Self=String> are the named instances of the traits for String.
The thing is that it changes a bit the story for function, because the current syntax:
fn foo<K: Eq + Hash, V>(&K, &HashMap<K, V>) -> Option<&V>
would actually under the hood mean
fn foo<K, V, eq_hash_k: Eq<Self=K> + Hash<Self=K>>(&K, &HashMap<eq_hash_k, V>) -> Option<&V>
Notice how because K has bounds, the meaning of K on the right hand side is changed to be an instance iff the place where it is has bounds too. The first syntax is really more succint and I don't think it's that bad to have it mean something slightly different, we can still think of K as being a type bundled together with the instances satisfying the bounds. Maybe the error message for bound fail would need a slight rephrasing to satisfy expert users (from the trait Foo is not implemented for Bar to no instance of Foo found for Bar).
I never really touched to the rustc codebase so I don't know how this would be doable (here I'm still in the context of would it be doable, not do we want to do this), but it seems to me that this is just a matter of uniquely naming instances (just like types). There would be a few things to look after when coding the equality judgement between instances -- the paper modular implicits has a section on this p.21 -- mainly that if you include/extend an instance Inst1 of Trait1 to an instance of Inst2 of Trait2: Trait1, the inner part of Inst2 pointing at Inst1 should still be equal to the original Inst1. Anyway if done carefully they say a simple definitional equality is sufficient so this doesn't seem unsurmontable.
As a side remark, I wonder why the definition of Hash isn't trait Hash: Eq { ... }, in the language I suggest this would definitely be required (because you can't just compose any Hash and Eq, they have to be compatible and you can't be compatible with every possible instance of Eq), but also in the real Rust I can't see why there would be a valid reason to have Hash without Eq (if you want a weird Hash without garantees you can just have &T: Into<u64>).
Also thanks for linking the modular implicits paper I forgot to provide links, I updated the OP with links to other relevant papers too (scala, agda).