Duplicated Typeclass Instances
Recently I come across the following flag for Coq
(* When a typeclass resolution is launched we ensure that
it has a single solution or fail. This flag ensures
that the resolution is canonical, but can make proof
search much more expensive. *)
Set Typeclasses Unique Solutions.
As far as I understand, it disables possibility to keep two instances of the same typeclass. I tried this flag in a random place and immediately found type-class duplication.
Require Export prosa.analysis.facts.preemption.job.nonpreemptive. (* Introduces non-preemptive preem. policy. *)
<...>
Context '{JobPreemptable Job}. (* Introduces an arbitrary preemption policy. *)
Hypothesis H_valid_preemption_model : (* Picks whatever it wants. *)
valid_preemption_model arr_seq sched.
With the proposed flag, Coq reports an error. Do we need this?