First of all, Coq does not have a single idiomatic style — but “using typeclasses” is one of the main styles used by respected authors.
Using canonical structures is another, used by other respected authors, but with subtle tradeoffs.
Other people are much more qualified than me on this topic, but since you come from the Haskell world, I figured I could sketch a comparison from my experience in Haskell and Coq (I’ve also used Scala).
TLDR: concerns exist, but IME they seem mostly disjoint from what you discuss. It’s also much less clear how typeclasses should behave in a proof assistant, how they behave in Coq, and how exactly the two align.
Coq typeclasses for Haskellers
I haven’t really seen typeclass issues affect correctness, once the code compiles — typically, correctness proofs should catch any problems, since they can guarantee so much more than plain non-dependent typechecking.
Typeclass Search Performance
The main concern is keeping instance search fast enough: when possible, you make typeclass search “syntax directed” by creating instance carefully. If an instance is too generic, you can turn it into a normal lemma and apply it by hand, or write a custom Hint Extern that can use arbitrary Ltac to decide whether it’s safe to apply it. When I make mistakes, I often can fix it as soon as it causes problems.
but the lack of overlap checking seems very dangerous
I’ve never seen that cause problems in practice because of conflicting instances. And if it did, I guess you’d likely notice when your proofs break.
Ecosystem size and structure
Maybe I haven’t seen this because I’ve never combined two independent libraries that use the same typeclasses; at best, I’ve seen libraries use some of the few typeclasses from the Coq stdlib. Probably things are different in the CompCert ecosystem, since many different projects use it?
Actual conflicts between libraries
Combining two libraries absolutely can cause problems in Coq, but mostly for different reasons: you can’t Import together two libraries with conflicting notations (but you can at least load them via Require, and use them in different scopes). And as soon as you load a library via Require, it can change global mutable state in Coq itself (say via flags), which affects code that is processed later. That’s far from elegant, and an actual problem, but I’m afraid it’s pretty baked-in in Coq. As a workaround, you can always try to change again those flags.
Now such global flags can affect how typeclass search proceeds in some cases — they can change which algorithm is used, or whether certain definitions should be expanded or not during search.
In Haskell, instead, definitions are either always expanded (type synonyms, type functions) or never expanded (datatypes, classes themselves).
Instances are imported transitively
As a special case, typeclass instances are made available upon Require, not Import. In other words, the instances in scope are usually all those defined by transitive imports. That’s far from ideal, but also hard to change.
Except ones that somebody removes — that’s possible too, via Remove Hints, whenever you realize somebody else provided a questionable instance — but I can only remember one use of this.
Why orphan instances are fine: No global uniqueness of instances is needed
Let me point out that one concern from Haskell can be avoided (even tho it doesn’t seem you mentioned it): having non-unique instances is safer, so “orphan instances” are much more acceptable (and in fact, they’re often necessary). If you are defining a type of FinSet T that depends on an instance o of Ord T, you can use dependent types to prevent mixing FinSet T that use different orders — the actual type will be @FinSet T o (tho the o itself will likely be kept implicit, so you’ll just write FinSet T) so mixing @FinSet T o1 with @FinSet T o2 will lead to a type error.
Combining multiple instances of Ord T for the same T is still likely to lead to confusion, but that will be caught by the typechecker.
I checked std++ (my go-to typeclass-using library) for examples; while it avoids order-based data structures there, its main general-purpose collections (gset and gmap) are indexed by an encoding function, represented via typeclass Countable.
Why orphans are currently necessary in Coq in practice
Orphans aren’t forbidden or discouraged, and the typeclasses in use are not standardized. So as soon as you combine a typeclass TC from a library A with a definition D from library B, and you need an instance for TC D, it’s likely it appears in neither library — but luckily, you can write it yourself or provide it in a glue library. And yes, forbidding orphans might force people to work around this, tho it’s not clear there’s a good way to do that (even in Haskell).