TC: drain pending TC-constraints before [try_delta]'s tc_reduce check

Closes the parametric-Path-B witness encoding gap that left class-
lemma applications at parametric carriers ([apply (addrC<:c poly>)]
inside [section ; declare type c <: comring]) unusable.

**The bug.** [opentvi] creates a [TCIUni] for each opened tparam's TC
bound and posts a [`TcCtt] problem, but doesn't itself drain the
queue. The TCIUni stays parked in [tcenv.problems] until something
else triggers [unify_core]. Meanwhile a proof-term carrying
[(+)<:c poly[TCIUni #a [0;0]]>] arrives at the matcher's [try_delta],
which tries [Op.tc_reducible env (+) tys] — and [tc_core_reduce]
raises [NotReducible] on TCIUni witnesses, since it can only walk
[TCIConcrete]/[TCIAbstract] forms. So [try_delta] falls through to
[default]'s [is_conv], which doesn't TC-reduce either; matching
fails, [pf_form_match] raises MatchFailure, [t_apply] reports "the
given proof-term proves: ... it does not apply to the goal".

**The fix.** Two changes:

1. [EcUnify.UniEnv.flush_tc_problems env ue] (new): runs
   [Unify.unify_core] on a trivial-true [`TyUni] problem, which
   re-pushes every parked [`TcCtt] in [tcenv.problems] and lets the
   strategy dispatcher resolve them. After the call, the resolution
   map contains a witness for every [TCIUni] that any strategy
   (Modes #1..#6) could pin.

2. In [EcMatching.f_match_core]'s [try_delta]: before destructuring
   the heads, call [flush_tc_problems env ue] and re-normalise both
   sides via [norm]. The substitution machinery in [tcw_subst]
   (ecCoreSubst.ml:209) dereferences resolved TCIUnis through
   [fs_tw_uni], so after [norm] both forms carry the concrete
   witness; [tc_reducible] then succeeds and [doit_tc_reduce]
   produces the renamed structural op (e.g. [polyD] for poly's
   addgroup-via-class-(+)), which conv'ing against the goal
   succeeds.

Combined with the earlier framework fixes [0dd7d21] (infer-via-
abs-decl) and [c182895] (alpha-equivalent chain reuse), this lets
[apply (addrC<:c poly> p q)] and [apply (mulrA<:c poly> p q r)]
inside a [c <: comring] section discharge directly, without
requiring users to fall back to the underlying [polyD_addrC<:c>] /
[polyM_mulrA] structural lemmas. The TcPoly port's structural-form
workaround in Phase 6 / Phase 7 / smoke test stays as-is for the
already-written code, but new code can use the natural class form.

Validates: tcalgebra suite (TcMonoid/TcRing/TcInt/TcBigop/TcBigalg/
TcNumber/TcPoly/TcPolySmokeTest) all pass; the parametric Path B
reproducer at /tmp/repro_pathb.ec now closes [test_path_b] via
[apply (addrC<:c poly>)] without admit.

Author: strub

src/ecMatching.ml

@@ -1217,6 +1217,16 @@ let f_match_core opts hyps (ue, ev) f1 f2 =
       let try_delta () =
         if not opts.fm_delta then
           failure ();
+        (* Drain pending TC constraints before checking [tc_reducible]:
+           a [TCIUni] witness on a TC op-head needs to be committed in
+           the resolution map (and then dereferenced via [norm]) for
+           [tc_core_reduce] to fire. Without this drain, a parametric-
+           carrier proof-term carrying an unresolved [TCIUni] would
+           fail to reduce here even when the carrier's TC instance is
+           registered in the env.                                       *)
+        EcUnify.UniEnv.flush_tc_problems env ue;
+        let f1 = norm f1 in
+        let f2 = norm f2 in
         match fst_map f_node (destr_app f1),
               fst_map f_node (destr_app f2)
         with

src/ecUnify.ml

@@ -999,6 +999,20 @@ module UniEnv = struct
     Unify.check_closed (!ue).ue_uc;
     assubst ue
 
+  (* Drain the pending TcCtt queue: invokes [Unify.unify_core] on a
+     trivially-true [TyUni] problem, which causes the unifier to first
+     re-process every parked [TcCtt] in [tcenv.problems]. After this,
+     any constraint that the strategies (Mode #1 .. #6) can resolve is
+     committed to [tcenv.resolution]. Constraints that defer (ambiguous
+     or carrier-with-univars) stay parked.                              *)
+  let flush_tc_problems (env : EcEnv.env) (ue : unienv) : unit =
+    if not (TcUni.Muid.is_empty (!ue).ue_uc.tcenv.problems) then
+      try
+        let trig = tunit in
+        let uc = Unify.unify_core env (!ue).ue_uc (`TyUni (trig, trig)) in
+        ue := { !ue with ue_uc = uc }
+      with UnificationFailure _ -> ()
+
   let tparams (ue : unienv) =
     let close = Unify.close (!ue).ue_uc in
     let deref_tc (tc : typeclass) : typeclass =

src/ecUnify.mli

@@ -59,6 +59,12 @@ module UniEnv : sig
   val assubst    : unienv -> ty TyUni.Muid.t
   val tw_assubst : unienv -> tcwitness TcUni.Muid.t
   val tparams    : unienv -> ty_params
+
+  (* Drain the pending TC-constraint queue, attempting to resolve every
+     [TcCtt] problem currently parked. Useful before TC-op reduction
+     attempts (e.g. in matcher's [try_delta]) where a [TCIUni] witness
+     needs to be committed before [tc_core_reduce] can fire.            *)
+  val flush_tc_problems : EcEnv.env -> unienv -> unit
 end
 
 val unify        : EcEnv.env -> unienv -> ty -> ty -> unit