I know the standard arguments for class coherence (Set etc.), but I haven't found any of them convincing. Relying on two values coming from two different places to be the same indicates that the design of the code is wrong. It's like writing a function f x y but you must only ever call it with identical arguments x=y. The right thing to do then is to give f only one argument to begin with.
But aside of that, I'm not all that convinced of the importance of coherence in a dependent setting either! My intuition is that types should encode all the properties that we'd like to be able to use in instances. In other words, even if we don't get coherence, we can use types to constrain the implementation of instances as much as we like.
Highly ambiguous instance resolution (like a bunch of Monoid Int instances lying around) is a bit of a pain though, and there could be some "using instance" feature/syntax that locally throws out all instances except one.
Additionally, as of now there are no large production code bases that use Coq style type classes in a proper dependent language. There are very few sizable applications in dependent languages to begin with. So we don't know a lot about the practical caveats of that design, while there is a lot of experience and know-how about Haskell-style classes, which is one reason why we should at least consider salvaging coherence in future languages.
Generally, I think that type classes are a rather ugly and haphazard construction compared to the succinct elegance of the type theories of core languages; still, eventually type classes worm their way into languages (Agda, Coq) because people really like them and like to use them, so a language designer should consider them. I wish there was an elegant/general formal treatment that captures the essential features, in any case.
Tie the type definition to the point where the data is created. Default to the local definition, but have a way to select the other one if you need some particular interaction between modules. Wouldn't that solve the conflict?
At which point you have basically reinvented "newtype"
My concern is that this PhD-style development suffices for most Haskell users, but is not practical for any non-small project in the real world with more than one developer.
This is not my experience of working with Haskell in the real world on a non-non-small project with (many) more than one developer.