Maxime Dénès

> I.e. what would prevent it from picking the more general but also less efficient version? I guess you can use priorities for that.

@RalfJung @robbertkrebbers so what should I do about this? I guess we could make the documentation of this option clearer. As for your use case, do you need #6285, #7661,...

> I'm not very convinced that the current `Set Typeclasses Unique Instances` is useful You mean we should extend it to also cover scenario 1 above?

@robbertkrebbers ping

@robbertkrebbers Would you mind giving it a try, so that we can schedule some work on this if required? Thanks!

> with the long-long-term goal of obtaining expressive and convenient languages as intuitive as natural languages Is this already not debatable? One could certainly want to make tactic languages as...

I share the concerns expressed above about syntactic pollution. I would like to see use cases, i.e. large enough proof using this to judge if the trade-off is good. So...

Sorry, but I was interested in a discussion on this. I don't recall seeing a presentation at any working group since this PR was opened, so I don't see why...

The last bunch of warnings is easy to remove by passing the appropriate flags to OCaml, I'll do it. The ones before are printed by extraction, which is much less...

Done for the last kind of warnings.