[typeclasses] functionalize typeclass evar handling

This avoids all the side effects associated with the manipulation of an
unresolvable flag. In the new design:

- The evar_map stores a set of evars that are candidates for typeclass
  resolution, which can be retrieved and set.

  We maintain the invariant that it always contains only undefined
  evars.

- At the creation time of an evar (new_evar), we classify it as a
  potential candidate of resolution.

  - This uses a hook to test if the conclusion ends in a typeclass
    application. (hook set in typeclasses.ml)

  - This is an approximation if the conclusion is an existential (i.e.
    not yet determined). In that case we register the evar as
    potentially a typeclass instance, and later phases must consider
    that case, dropping the evar if it is not a typeclass.

  - One can pass the ~typeclass_candidate:false flag to new_evar to
    prevent classification entirely. Typically this is for new goals
    which should not ever be considered to be typeclass resolution
    candidates.

  - One can mark a subset of evars unresolvable later if
    needed. Typically for clausenv, and marking future goals as
    unresolvable even if they are typeclass goals. For clausenv for
    example, after turing metas into evars we first (optionally) try a
    typeclass resolution on the newly created evars and only then mark
    the remaining newly created evars as subgoals. The intent of the
    code looks clearer now.

  This should prevent keeping testing if undefined evars are classes
  all the time and crawling large sets when no typeclasses are present.

- Typeclass candidate evars stay candidates through
  restriction/evar-evar solutions.

- Evd.add uses ~typeclass_candidate:false to avoid recomputing if the new
  evar is a candidate. There's a deficiency in the API, in most use
  cases of Evd.add we should rather use a:

  `Evd.update_evar_info : evar_map -> Evar.t -> (evar_info -> evar_info)
  -> evar_map`

  Usually it is only about nf_evar'ing the evar_info's contents, which
  doesn't change the evar candidate status.

- Typeclass resolution can now handle the set of candidates
  functionally: it always starts from the set of candidates (and not the
  whole undefined_map) and a filter on it, potentially splitting it in
  connected components, does proof search for each component in an
  evar_map with an empty set of typeclass evars (allowing clean
  reentrancy), then reinstates the potential remaining unsolved
  components and filtered out typeclass evars at the end of
  resolution.

  This means no more marking of resolvability/unresolvability
  everywhere, and hopefully a more efficient implementation in general.

- This is on top of the cleanup of evar_info's currently but can
  be made independent.

[typeclasses] Fix cases.ml: none of the new_evars should be typeclass candidates

Solve bug in inheritance of flags in evar-evar solutions.

Renaming unresolvable to typeclass_candidate (positive) and fix maybe_typeclass_hook

6 files changed, 16 insertions, 33 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 7ebc789aa5..d25ae38c53 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -324,21 +324,21 @@ let adjust_meta_source evd mv = function
 *)
 
 let clenv_pose_metas_as_evars clenv dep_mvs =
-  let rec fold clenv = function
-  | [] -> clenv
+  let rec fold clenv evs = function
+  | [] -> clenv, evs
   | mv::mvs ->
       let ty = clenv_meta_type clenv mv in
       (* Postpone the evar-ization if dependent on another meta *)
       (* This assumes no cycle in the dependencies - is it correct ? *)
-      if occur_meta clenv.evd ty then fold clenv (mvs@[mv])
+      if occur_meta clenv.evd ty then fold clenv evs (mvs@[mv])
       else
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
         let evd = clenv.evd in
 	let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in
 	let clenv = clenv_assign mv evar {clenv with evd=evd} in
-	fold clenv mvs in
-  fold clenv dep_mvs
+        fold clenv (fst (destEvar evd evar) :: evs) mvs in
+  fold clenv [] dep_mvs
 
 (******************************************************************)
 
@@ -608,8 +608,7 @@ let make_evar_clause env sigma ?len t =
     else match EConstr.kind sigma t with
     | Cast (t, _, _) -> clrec (sigma, holes) n t
     | Prod (na, t1, t2) ->
-      let (sigma, ev) = new_evar env sigma t1 in
-      let sigma = Evd.set_resolvable_evar sigma (fst (destEvar sigma ev)) false in
+      let (sigma, ev) = new_evar env sigma ~typeclass_candidate:false t1 in
       let dep = not (noccurn sigma 1 t2) in
       let hole = {
         hole_evar = ev;
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index f9506290a0..03acb9e46e 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -72,7 +72,7 @@ val clenv_unique_resolver :
 
 val clenv_dependent : clausenv -> metavariable list
 
-val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
+val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv * Evar.t list
 
 (** {6 Bindings } *)
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 929443a969..77f5804665 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -62,37 +62,19 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv =
       (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
   clenv_pose_metas_as_evars clenv dep_mvs
 
-(** Use our own fast path, more informative than from Typeclasses *)
-let check_tc evd =
-  let has_resolvable = ref false in
-  let check ev evi =
-    let res = Evd.is_resolvable_evar evd ev in
-    if res then
-      let () = has_resolvable := true in
-      Typeclasses.is_class_evar evd evi
-    else false
-  in
-  let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in
-  (has_typeclass, !has_resolvable)
-
 let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
   (** ppedrot: a Goal.enter here breaks things, because the tactic below may
       solve goals by side effects, while the compatibility layer keeps those
       useless goals. That deserves a FIXME. *)
   Proofview.V82.tactic begin fun gl ->
-  let clenv = clenv_pose_dependent_evars ~with_evars clenv in
+  let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in
   let evd' =
     if with_classes then
-      let (has_typeclass, has_resolvable) = check_tc clenv.evd in
       let evd' =
-        if has_typeclass then
-          Typeclasses.resolve_typeclasses ~fast_path:false ~filter:Typeclasses.all_evars
+        Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
           ~fail:(not with_evars) ~split:false clenv.env clenv.evd
-        else clenv.evd
       in
-      if has_resolvable then
-        Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
-      else evd'
+      Typeclasses.make_unresolvables (fun x -> List.mem_f Evar.equal x evars) evd'
     else clenv.evd
   in
   let clenv = { clenv with evd = evd' } in
@@ -101,6 +83,9 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
     (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl
   end
 
+let clenv_pose_dependent_evars ?(with_evars=false) clenv =
+  fst (clenv_pose_dependent_evars ~with_evars clenv)
+
 open Unification
 
 let dft = default_unify_flags
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 6aff43f741..4e540de538 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -64,8 +64,7 @@ module V82 = struct
 		Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
                 Evd.evar_candidates = None }
     in
-    let (evars, evk) = Evarutil.new_pure_evar_full evars evi in
-    let evars = Evd.set_resolvable_evar evars evk false in
+    let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi in
     let evars = Evd.restore_future_goals evars prev_future_goals in
     let ctxt = Environ.named_context_of_val hyps in
     let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 70a08e4966..8220949856 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -386,7 +386,7 @@ let run_tactic env tac pr =
     (* Check that retrieved given up is empty *)
     if not (List.is_empty retrieved_given_up) then
       CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up.");
-    let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in
+    let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
     Proofview.tclUNIT retrieved
   in
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 05474d5f84..540a8bb420 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -105,7 +105,7 @@ let generic_refine ~typecheck f gl =
         | Some id -> Evd.rename evk id sigma
   in
   (** Mark goals *)
-  let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
+  let sigma = Proofview.Unsafe.mark_as_goals sigma comb in
   let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
   let trace () = Pp.(hov 2 (str"simple refine"++spc()++
                             Termops.Internal.print_constr_env env sigma c)) in