typing: defer failed-application classification (perf)

Operator selection reported every rejected candidate through
EcUnify.classify_application, which peels the argument list one type at a
time, head-normalising via `ty_hnorm (ty_subst (Tuni.subst (UniEnv.assubst
ue)) _)` at each step. UniEnv.assubst is subst_of_uf, materialising the
whole unifier by folding over UF.domain (every univar in the unienv), so
each candidate cost O(arity * |unienv|) instead of the O(arity)
incremental union-find of the previous single unification.

Overload resolution rejects candidates constantly on the *success* path
(any application of an overloaded name tries and drops the non-matching
instances), so this classification ran pervasively even though the
diagnostics it produces are only ever consumed when an application fails
outright and an error is raised. On a large formosa-keccak module this
turned a ~8s require into ~54s.

Defer the classification:

- EcUnify: select_outcome's KO now carries a `... Lazy.t`. select_op
  decides OK/KO with the cheap single `unify top texpected` and drops KO
  without ever forcing it; select_op_failures forces the thunks and is
  meant for the error path only. classify_application is unchanged.

- EcTyping.gen_select_op: the OK selection uses select_op; the failure
  list becomes a lazy closure (program-variable failures, which cost one
  unification, stay eager). tyerror_noop forces it only when building the
  UnappliedOp / UnknownVarOrOp error.

Diagnostics are byte-identical (candidate order preserved). Keccak
require back to 8.4s; tests/op-application-errors.ec passes; unit
(84/84) and stdlib (128/128) green.

Author: strub

src/ecTyping.ml

@@ -374,11 +374,9 @@ let gen_select_op
     (ue       : EcUnify.unienv)
     (psig     : EcTypes.dom * EcTypes.ty option)
 
-    : OpSelect.gopsel list * OpSelect.opfailure list
+    : OpSelect.gopsel list * OpSelect.opfailure list Lazy.t
 =
 
-  let opfailures = ref [] in
-
   let fpv me (pv, ty, ue) : OpSelect.gopsel =
     (`Pv (me, pv), ty, ue, (pv :> opmatch))
 
@@ -417,30 +415,24 @@ let gen_select_op
       |>  Option.to_list
     else [] in
 
+  (* Cheap: only program-variable failures, which cost a single unification.
+     Operator failures are classified lazily below, off the fast typing path. *)
+  let pvfailures = ref [] in
+
   let ops () : OpSelect.gopsel list =
-    let outcomes =
-      EcUnify.select_op_outcomes ~filter:ue_filter tvi env name ue psig in
-    let ops =
-      List.filter_map
-        (function EcUnify.OK r -> Some r | EcUnify.KO _ -> None) outcomes in
-    opfailures := !opfailures @
-      List.filter_map
-        (function
-          | EcUnify.KO (p, inst, ty, f) -> Some (`Op (p, inst, ty), f)
-          | EcUnify.OK _ -> None)
-        outcomes;
+    let ops = EcUnify.select_op ~filter:ue_filter tvi env name ue psig in
     let ops = opsc |> ofold (fun opsc -> List.mbfilter (by_scope opsc)) ops in
     let ops = match List.mbfilter by_current ops with [] -> ops | ops -> ops in
     let ops = match List.mbfilter by_tc ops with [] -> ops | ops -> ops in
     (List.map fop ops)
 
   and pvs () : OpSelect.gopsel list =
-    let me, (pvs, pvfailures) =
+    let me, (pvs, pvf) =
       match EcEnv.Memory.get_active_ss env, actonly with
       | None, true -> (None, ([], []))
       | me  , _    -> (  me, select_pv env me name ue tvi psig)
     in
-    opfailures := !opfailures @ pvfailures;
+    pvfailures := pvf;
     List.map (fpv me) pvs
   in
 
@@ -460,7 +452,18 @@ let gen_select_op
         else
           select [locals; pvs; ops]
   in
-  (selected, !opfailures)
+
+  (* Reasons the named candidates fail to apply. Only inspected when nothing was
+     selected (i.e. an error is being reported), so the expensive per-argument
+     operator classification stays off the fast typing path. *)
+  let opfailures = lazy (
+    !pvfailures
+    @ List.map
+        (fun (p, inst, ty, f) -> (`Op (p, inst, ty), f))
+        (EcUnify.select_op_failures ~filter:ue_filter tvi env name ue psig)
+  ) in
+
+  (selected, opfailures)
 
 (* -------------------------------------------------------------------- *)
 let select_exp_op env mode opsc name ue tvi psig =
@@ -475,10 +478,11 @@ let select_form_op env mode ~forcepv opsc name ue tvi psig =
 (* -------------------------------------------------------------------- *)
 (* [UnappliedOp] when candidates of that name exist but fail, else
    [UnknownVarOrOp]. *)
-let tyerror_noop env loc name esig retty (opfailures : OpSelect.opfailure list) =
-  match opfailures with
+let tyerror_noop env loc name esig retty
+    (opfailures : OpSelect.opfailure list Lazy.t) =
+  match Lazy.force opfailures with
   | [] -> tyerror loc env (UnknownVarOrOp (name, esig))
-  | _  -> tyerror loc env (UnappliedOp (name, esig, retty, opfailures))
+  | opfailures -> tyerror loc env (UnappliedOp (name, esig, retty, opfailures))
 
 (* -------------------------------------------------------------------- *)
 let select_proj env opsc name ue tvi recty =

src/ecUnify.ml

@@ -342,8 +342,10 @@ type op_instance = (EcIdent.t * ty) list
 
 type select_outcome =
   | OK of select_result
-  | KO of EcPath.path * op_instance * ty * op_failure
-    (* operator path, partial instantiation, declared operator type, reason *)
+  | KO of (EcPath.path * op_instance * ty * op_failure) Lazy.t
+    (* operator path, partial instantiation, declared operator type, reason.
+       Deferred: classifying the failure is expensive and only needed when an
+       error is reported, so [select_op] can drop it without ever forcing it. *)
 
 (* -------------------------------------------------------------------- *)
 (* [None] if [top] applies to [psig] (and [retty]), updating [ue]; otherwise
@@ -434,17 +436,34 @@ let select_op_outcomes
       filter oppath op && filter_on_tvi op
   in
 
-  let select (path, op) =
+  let mk_ok (path, op) tip tvs top subue =
+    let bd =
+      match op.D.op_kind with
+      | OB_nott nt ->
+         let substnt () =
+           let xs = List.map (snd_map (ty_subst tip)) nt.D.ont_args in
+           let es = e_subst tip in
+           let bd = es nt.D.ont_body in
+           (xs, bd)
+         in Some (Lazy.from_fun substnt)
+
+      | _ -> None
+
+    in OK ((path, tvs), top, subue, bd)
+  in
+
+  (* Precise (but expensive) classification of why [op] fails to apply. Called
+     lazily, only when an error message is actually built, so its per-argument
+     head-normalisation never runs on the fast typing path. *)
+  let classify (path, op) =
     let subue = UniEnv.copy ue in
 
     let (tip, tvs) = UniEnv.openty_r subue op.D.op_tparams tvi in
     let top = ty_subst tip op.D.op_ty in
 
     let resolve ty = ty_subst (Tuni.subst (UniEnv.assubst subue)) ty in
 
-    let failure = classify_application env subue top psig retty in
-
-    match failure with
+    match classify_application env subue top psig retty with
     | Some f ->
         let instance =
           List.combine op.D.op_tparams tvs
@@ -453,21 +472,24 @@ let select_op_outcomes
                | Tunivar _ -> None
                | _         -> Some (tp, resolve tv))
         in
-        KO (path, instance, op.D.op_ty, f)
-    | None ->
-        let bd =
-          match op.D.op_kind with
-          | OB_nott nt ->
-             let substnt () =
-               let xs = List.map (snd_map (ty_subst tip)) nt.D.ont_args in
-               let es = e_subst tip in
-               let bd = es nt.D.ont_body in
-               (xs, bd)
-             in Some (Lazy.from_fun substnt)
+        (path, instance, op.D.op_ty, f)
 
-          | _ -> None
+    (* Unreachable: [select] only builds a [KO] once the fast unification has
+       already rejected the candidate, and the two solve the same problem. *)
+    | None -> assert false
+  in
 
-        in OK ((path, tvs), top, subue, bd)
+  let select (path, op) =
+    let subue = UniEnv.copy ue in
+
+    let (tip, tvs) = UniEnv.openty_r subue op.D.op_tparams tvi in
+    let top = ty_subst tip op.D.op_ty in
+
+    let texpected = tfun_expected subue ?retty psig in
+
+    match unify env subue top texpected with
+    | () -> mk_ok (path, op) tip tvs top subue
+    | exception UnificationFailure _ -> KO (lazy (classify (path, op)))
 
   in
     List.map select (EcEnv.Op.all ~check:filter ~name env)
@@ -482,3 +504,17 @@ let select_op
   List.filter_map
     (function OK r -> Some r | KO _ -> None)
     (select_op_outcomes ?hidden ?filter tvi env name ue sig_)
+
+(* -------------------------------------------------------------------- *)
+(* The candidates of that name that fail to apply, with the reason why. This
+   runs the (expensive) per-argument classification and is meant to be called
+   only when building an error message — never on the fast typing path. *)
+let select_op_failures
+  ?hidden ?filter (tvi : tvar_inst option)
+  (env : EcEnv.env) (name : qsymbol) (ue : unienv)
+  (sig_ : ty list * ty option)
+  : (EcPath.path * op_instance * ty * op_failure) list
+=
+  List.filter_map
+    (function KO lz -> Some (Lazy.force lz) | OK _ -> None)
+    (select_op_outcomes ?hidden ?filter tvi env name ue sig_)

src/ecUnify.mli

@@ -50,11 +50,6 @@ type op_failure =
 (* Constrained type parameters of an operator (those bound while applying it). *)
 type op_instance = (EcIdent.t * ty) list
 
-type select_outcome =
-  | OK of select_result
-  | KO of EcPath.path * op_instance * ty * op_failure
-    (* operator path, partial instantiation, declared operator type, reason *)
-
 (* [None] if [top] applies to [psig] (and [retty]), updating [ue]; otherwise
    [Some] of the first argument/result/arity failure. *)
 val classify_application :
@@ -70,12 +65,13 @@ val select_op :
   -> dom * ty option
   -> select_result list
 
-val select_op_outcomes :
+(* Expensive: classifies every failing candidate. Call only on the error path. *)
+val select_op_failures :
      ?hidden:bool
   -> ?filter:(path -> operator -> bool)
   -> tvi
   -> EcEnv.env
   -> qsymbol
   -> unienv
   -> dom * ty option
-  -> select_outcome list
+  -> (path * op_instance * ty * op_failure) list