typing: defer failed-application classification (perf)

src/ecTyping.ml

@@ -334,11 +334,15 @@ let select_pv env side name ue tvi (psig, retty)
     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)])
+      let expected = toarrow psig (ofdfl (fun () -> UE.fresh subue) retty) in
+      try
+        EcUnify.unify env subue ty expected;
+        ([(pv, ty, subue)], [])
+      with EcUnify.UnificationFailure _ ->
+        let subue = UE.copy ue in
+        let f = oget (EcUnify.classify_application env subue ty psig retty) in
+        let pv0 = match pv with `Var p -> p | `Proj (p, _) -> p in
+        ([], [(`Pv (pv0, ty), f)])
     with EcEnv.LookupFailure _ -> ([], [])
 
 (* -------------------------------------------------------------------- *)
@@ -374,11 +378,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 +419,22 @@ let gen_select_op
       |>  Option.to_list
     else [] in
 
+  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 +454,15 @@ let gen_select_op
         else
           select [locals; pvs; ops]
   in
-  (selected, !opfailures)
+
+  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 +477,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,40 +434,53 @@ 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
+    (* [select] builds a [KO] only after unification rejected the candidate. *)
+    let f = oget (classify_application env subue top psig retty) in
+    let instance =
+      List.combine op.D.op_tparams tvs
+      |> List.filter_map (fun (tp, tv) ->
+           match (resolve tv).ty_node with
+           | Tunivar _ -> None
+           | _         -> Some (tp, resolve tv))
+    in
+    (path, instance, op.D.op_ty, f)
+  in
 
-    match failure with
-    | Some f ->
-        let instance =
-          List.combine op.D.op_tparams tvs
-          |> List.filter_map (fun (tp, tv) ->
-               match (resolve tv).ty_node with
-               | 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)
+  let select (path, op) =
+    let subue = UniEnv.copy ue in
 
-          | _ -> None
+    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
 
-        in OK ((path, tvs), top, subue, bd)
+    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 +495,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