Statically ensure that all TC evars are a subset of undefined evars.

The Evd.set_typeclass_evars primitive was making the assumption that all
callers were respecting this invariant. Rather than exporting an unsafe API
that can mess with the expected invariants of the evarmap data structure,
we simply check at runtime that all evar arguments are indeed undefined.

Fixes coq#19587: Error: Anomaly "Uncaught exception Not_found."

engine/evd.ml

@@ -774,6 +774,7 @@ let get_typeclass_evars evd = evd.evar_flags.typeclass_evars
 
 let set_typeclass_evars evd tcs =
   let flags = evd.evar_flags in
+  let tcs = Evar.Set.filter (fun evk -> Evar.Map.mem evk evd.undf_evars) tcs in
   { evd with evar_flags = { flags with typeclass_evars = tcs } }
 
 let is_typeclass_evar evd evk =

test-suite/bugs/bug_19587.v

@@ -0,0 +1,31 @@
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+
+Class ring α := { rng_zero : α; }.
+Class field := { }.
+
+Parameter lap_eq : forall {α} {r : ring α}, list α -> list α -> Prop.
+
+Declare Instance lap_eq_equiv : forall {α} {r : ring α}, Equivalence lap_eq.
+
+Axiom lap_eq_0 : forall (α : Type) (r : ring α), lap_eq (cons rng_zero nil) nil.
+
+Definition puiseux_series (α : Type) := nat -> α.
+
+Definition ps_zero {α} {r : ring α} : puiseux_series α := fun i => rng_zero.
+
+Definition ps_ring α (R : ring α) (K : field) : ring (puiseux_series α) :=
+  {| rng_zero := ps_zero; |}.
+
+Canonical Structure ps_ring.
+
+Theorem glop : forall
+  (α : Type) (R : ring α) (K : field),
+  @lap_eq (puiseux_series α) (@ps_ring α R K)
+     (@cons (puiseux_series α) (@ps_zero α R) (@nil (puiseux_series α)))
+     nil.
+Proof.
+intros.
+Check 1%nat.
+rewrite lap_eq_0.
+Check 1%nat.
+Abort.