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, for the
  error path only. classify_application is unchanged.

- EcTyping.gen_select_op: the OK selection uses select_op; the failure
  list is a lazy closure forced only by tyerror_noop when building the
  UnappliedOp / UnknownVarOrOp error. select_pv likewise decides with a
  single unification and defers its own failure classification.

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

Author: strub

src/ecTyping.ml

@@ -324,22 +324,28 @@ let select_local env (qs,s) =
   else None
 
 (* -------------------------------------------------------------------- *)
-(* The program variable [name] if it applies to [psig]/[retty], else the
-   reason it does not. *)
+(* The program variable [name] if it applies to [psig]/[retty], else (lazily)
+   the reason it does not. *)
 let select_pv env side name ue tvi (psig, retty)
-    : (_ * ty * EcUnify.unienv) list * (appcand * EcUnify.op_failure) list =
+    : (_ * ty * EcUnify.unienv) list * (appcand * EcUnify.op_failure) list Lazy.t =
   if   tvi <> None
-  then ([], [])
+  then ([], lazy [])
   else
     try
       let (pv, ty) = EcEnv.Var.lookup_progvar ?side name env in
       let subue = UE.copy ue in
-      match EcUnify.classify_application env subue ty psig retty with
-      | None   -> ([(pv, ty, subue)], [])
-      | Some f ->
-          let pv0 = match pv with `Var p -> p | `Proj (p, _) -> p in
-          ([], [(`Pv (pv0, ty), f)])
-    with EcEnv.LookupFailure _ -> ([], [])
+      let expected = toarrow psig (ofdfl (fun () -> UE.fresh subue) retty) in
+      match EcUnify.unify env subue ty expected with
+      | () -> ([(pv, ty, subue)], lazy [])
+      | exception EcUnify.UnificationFailure _ ->
+          ([], lazy (
+            let subue = UE.copy ue in
+            match EcUnify.classify_application env subue ty psig retty with
+            | None   -> []
+            | Some f ->
+                let pv0 = match pv with `Var p -> p | `Proj (p, _) -> p in
+                [(`Pv (pv0, ty), f)]))
+    with EcEnv.LookupFailure _ -> ([], lazy [])
 
 (* -------------------------------------------------------------------- *)
 module OpSelect = struct
@@ -374,11 +380,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 +421,22 @@ let gen_select_op
       |>  Option.to_list
     else [] in
 
+  let pvfailures = ref (lazy []) 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, ([], []))
+      | None, true -> (None, ([], lazy []))
       | me  , _    -> (  me, select_pv env me name ue tvi psig)
     in
-    opfailures := !opfailures @ pvfailures;
+    pvfailures := pvf;
     List.map (fpv me) pvs
   in
 
@@ -460,7 +456,15 @@ let gen_select_op
         else
           select [locals; pvs; ops]
   in
-  (selected, !opfailures)
+
+  let opfailures = lazy (
+    Lazy.force !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 +479,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,7 +342,7 @@ type op_instance = (EcIdent.t * ty) list
 
 type select_outcome =
   | OK of select_result
-  | KO of EcPath.path * op_instance * ty * op_failure
+  | KO of (EcPath.path * op_instance * ty * op_failure) Lazy.t
     (* operator path, partial instantiation, declared operator type, reason *)
 
 (* -------------------------------------------------------------------- *)
@@ -434,17 +434,31 @@ 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
+
+  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 +467,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 +499,15 @@ 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. *)
+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,12 @@ val select_op :
   -> dom * ty option
   -> select_result list
 
-val select_op_outcomes :
+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