[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

4 files changed, 48 insertions, 47 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 54e847988b..164f5ab96d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -296,8 +296,7 @@ let inductive_template env sigma tmloc ind =
             let ty = EConstr.of_constr ty in
 	    let ty' = substl subst ty in
             let sigma, e =
-                Evarutil.new_evar env ~src:(hole_source n)
-                sigma ty'
+              Evarutil.new_evar env ~src:(hole_source n) ~typeclass_candidate:false sigma ty'
             in
             (sigma, e::subst,e::evarl,n+1)
 	| LocalDef (na,b,ty) ->
@@ -1698,7 +1697,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
 	    (fun i _ ->
               try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
               1 (rel_context !!env) in
-        let sigma, ev' = Evarutil.new_evar ~src !!env sigma ty in
+        let sigma, ev' = Evarutil.new_evar ~src ~typeclass_candidate:false !!env sigma ty in
         begin match solve_simple_eqn (evar_conv_x full_transparent_state) !!env sigma (None,ev,substl inst ev') with
         | Success evd -> evdref := evd
         | UnifFailure _ -> assert false
@@ -1734,7 +1733,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
           (named_context !!extenv) in
       let filter = Filter.make (rel_filter @ named_filter) in
       let candidates = List.rev (u :: List.map mkRel vl) in
-      let sigma, ev = Evarutil.new_evar !!extenv ~src ~filter ~candidates sigma ty in
+      let sigma, ev = Evarutil.new_evar !!extenv ~src ~filter ~candidates ~typeclass_candidate:false sigma ty in
       let () = evdref := sigma in
       lift k ev
   in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 9422a96f21..674f6846ae 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1239,26 +1239,21 @@ let check_evar_instance evd evk1 body conv_algo =
   | UnifFailure _ -> raise (IllTypedInstance (evenv,ty, evi.evar_concl))
 
 let update_evar_info ev1 ev2 evd =
+  (* We update the source of obligation evars during evar-evar unifications. *)
   let loc, evs2 = evar_source ev2 evd in
-  let evd =
-    (* We keep the obligation evar flag during evar-evar unifications *)
-    if is_obligation_evar evd ev2 then
-      let evi = Evd.find evd ev1 in
-      let evd = Evd.add evd ev1 {evi with evar_source = loc, evs2} in
-      Evd.set_obligation_evar evd ev1
-    else evd
-  in
-  (** [ev1] inherits the unresolvability status from [ev2] *)
-  if not (Evd.is_resolvable_evar evd ev2) then
-    Evd.set_resolvable_evar evd ev1 false
-  else evd
+  let evi = Evd.find evd ev1 in
+  Evd.add evd ev1 {evi with evar_source = loc, evs2}
 
 let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
   try
     let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in
-    let evd' = Evd.define evk2 body evd in
-    let evd' = update_evar_info (fst (destEvar evd body)) evk2 evd' in
-      check_evar_instance evd' evk2 body g
+    let evd' = Evd.define_with_evar evk2 body evd in
+    let evd' =
+      if is_obligation_evar evd evk2 then
+        update_evar_info evk2 (fst (destEvar evd' body)) evd'
+      else evd'
+    in
+    check_evar_instance evd' evk2 body g
   with EvarSolvedOnTheFly (evd,c) ->
     f env evd pbty ev2 c
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 07821f03e5..4aea2c3db9 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -166,6 +166,21 @@ let rec is_class_type evd c =
 let is_class_evar evd evi =
   is_class_type evd evi.Evd.evar_concl
 
+let is_class_constr sigma c =
+  try let gr, u = Termops.global_of_constr sigma c in
+    GlobRef.Map.mem gr !classes
+  with Not_found -> false
+
+let rec is_maybe_class_type evd c =
+  let c, _ = Termops.decompose_app_vect evd c in
+    match EConstr.kind evd c with
+    | Prod (_, _, t) -> is_maybe_class_type evd t
+    | Cast (t, _, _) -> is_maybe_class_type evd t
+    | Evar _ -> true
+    | _ -> is_class_constr evd c
+
+let () = Hook.set Evd.is_maybe_typeclass_hook (fun evd c -> is_maybe_class_type evd (EConstr.of_constr c))
+
 (*
  * classes persistent object
  *)
@@ -481,36 +496,29 @@ let instances r =
 let is_class gr = 
   GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
 
-let mark_resolvability_undef evm evk b =
-  let resolvable = Evd.is_resolvable_evar evm evk in
-  if b == resolvable then evm
-  else Evd.set_resolvable_evar evm evk b
-
 open Evar_kinds
-type evar_filter = Evar.t -> Evar_kinds.t -> bool
+type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool
+
+let make_unresolvables filter evd =
+  let tcs = Evd.get_typeclass_evars evd in
+  Evd.set_typeclass_evars evd (Evar.Set.filter (fun x -> not (filter x)) tcs)
 
 let all_evars _ _ = true
-let all_goals _ = function VarInstance _ | GoalEvar -> true | _ -> false
+let all_goals _ source =
+  match Lazy.force source with
+  | VarInstance _ | GoalEvar -> true
+  | _ -> false
+
 let no_goals ev evi = not (all_goals ev evi)
-let no_goals_or_obligations _ = function
+let no_goals_or_obligations _ source =
+  match Lazy.force source with
   | VarInstance _ | GoalEvar | QuestionMark _ -> false
   | _ -> true
 
-let mark_resolvability filter b sigma =
-  let map ev evi evm =
-    if filter ev (snd evi.evar_source) then mark_resolvability_undef evm ev b
-    else evm
-  in
-  Evd.fold_undefined map sigma sigma
-
-let mark_unresolvables ?(filter=all_evars) sigma = mark_resolvability filter false sigma
-let mark_resolvables ?(filter=all_evars) sigma = mark_resolvability filter true sigma
-
 let has_typeclasses filter evd =
-  let check ev evi =
-    filter ev (snd evi.evar_source) && Evd.is_resolvable_evar evd ev && is_class_evar evd evi
-  in
-  Evar.Map.exists check (Evd.undefined_map evd)
+  let tcs = get_typeclass_evars evd in
+  let check ev = filter ev (lazy (snd (Evd.find evd ev).evar_source)) in
+  Evar.Set.exists check tcs
 
 let get_solve_all_instances, solve_all_instances_hook = Hook.make ()
 
@@ -521,7 +529,7 @@ let solve_all_instances env evd filter unique split fail =
 (* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *)
 (* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *)
 
-let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
+let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
     ?(split=true) ?(fail=true) env evd =
-  if fast_path && not (has_typeclasses filter evd) then evd
+  if not (has_typeclasses filter evd) then evd
   else solve_all_instances env evd filter unique split fail
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index de9a99a868..ee9c83dad3 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -93,7 +93,7 @@ val instance_constructor : typeclass EConstr.puniverses -> EConstr.t list ->
   EConstr.t option * EConstr.t
 
 (** Filter which evars to consider for resolution. *)
-type evar_filter = Evar.t -> Evar_kinds.t -> bool
+type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool
 val all_evars : evar_filter
 val all_goals : evar_filter
 val no_goals : evar_filter
@@ -107,13 +107,12 @@ val no_goals_or_obligations : evar_filter
     An unresolvable evar is an evar the type-class engine will NOT try to solve
 *)
 
-val mark_unresolvables : ?filter:evar_filter -> evar_map -> evar_map
-val mark_resolvables   : ?filter:evar_filter -> evar_map -> evar_map
+val make_unresolvables : (Evar.t -> bool) -> evar_map -> evar_map
 
 val is_class_evar : evar_map -> evar_info -> bool
 val is_class_type : evar_map -> EConstr.types -> bool
 
-val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool ->
+val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool ->
   ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map
 val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> evar_map * EConstr.constr