[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

1 files changed, 66 insertions, 30 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 3a01706063..3a77a2b440 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -413,7 +413,7 @@ type goal_kind = ToShelve | ToGiveUp
 type evar_flags =
   { obligation_evars : Evar.Set.t;
     restricted_evars : Evar.t Evar.Map.t;
-    unresolvable_evars : Evar.Set.t }
+    typeclass_evars : Evar.Set.t }
 
 type evar_map = {
   (** Existential variables *)
@@ -444,44 +444,44 @@ type evar_map = {
   extras : Store.t;
 }
 
+let get_is_maybe_typeclass, (is_maybe_typeclass_hook : (evar_map -> constr -> bool) Hook.t) = Hook.make ~default:(fun evd c -> false) ()
+
+let is_maybe_typeclass sigma c = Hook.get get_is_maybe_typeclass sigma c
+
 (*** Lifting primitive from Evar.Map. ***)
 
 let rename evk id evd =
   { evd with evar_names = EvNames.rename evk id evd.evar_names }
 
-let add_with_name ?name d e i = match i.evar_body with
+let add_with_name ?name ?(typeclass_candidate = true) d e i = match i.evar_body with
 | Evar_empty ->
   let evar_names = EvNames.add_name_undefined name e i d.evar_names in
-  { d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
+  let evar_flags =
+    if typeclass_candidate && is_maybe_typeclass d i.evar_concl then
+      let flags = d.evar_flags in
+      { flags with typeclass_evars = Evar.Set.add e flags.typeclass_evars }
+    else d.evar_flags
+  in
+  { d with undf_evars = EvMap.add e i d.undf_evars; evar_names; evar_flags }
 | Evar_defined _ ->
   let evar_names = EvNames.remove_name_defined e d.evar_names in
   { d with defn_evars = EvMap.add e i d.defn_evars; evar_names }
 
-let add d e i = add_with_name d e i
+(** Evd.add is a low-level function mainly used to update the evar_info
+    associated to an evar, so we prevent registering its typeclass status. *)
+let add d e i = add_with_name ~typeclass_candidate:false d e i
 
-(*** Evar flags: resolvable, restricted or obligation flag *)
+(*** Evar flags: typeclasses, restricted or obligation flag *)
 
-let set_resolvable_evar evd evk b =
-  let flags = evd.evar_flags in
-  let unresolvable_evars = flags.unresolvable_evars in
-  let unresolvable_evars =
-    if b then Evar.Set.remove evk unresolvable_evars
-    else Evar.Set.add evk unresolvable_evars
-  in
-  { evd with evar_flags = { flags with unresolvable_evars } }
+let get_typeclass_evars evd = evd.evar_flags.typeclass_evars
 
-let is_resolvable_evar evd evk =
+let set_typeclass_evars evd tcs =
   let flags = evd.evar_flags in
-  not (Evar.Set.mem evk flags.unresolvable_evars)
+  { evd with evar_flags = { flags with typeclass_evars = tcs } }
 
-let inherit_unresolvable_evar evar_flags evk evk' =
-  let evk_unres = Evar.Set.mem evk evar_flags.unresolvable_evars in
-  let unresolvable_evars = Evar.Set.remove evk evar_flags.unresolvable_evars in
-  let unresolvable_evars =
-    if evk_unres then Evar.Set.add evk' unresolvable_evars else unresolvable_evars
-  in { evar_flags with unresolvable_evars }
-
-let unresolvable_evars evd = evd.evar_flags.unresolvable_evars
+let is_typeclass_evar evd evk =
+  let flags = evd.evar_flags in
+  Evar.Set.mem evk flags.typeclass_evars
 
 let set_obligation_evar evd evk =
   let flags = evd.evar_flags in
@@ -492,8 +492,31 @@ let is_obligation_evar evd evk =
   let flags = evd.evar_flags in
   Evar.Set.mem evk flags.obligation_evars
 
+(** Inheritance of flags: for evar-evar and restriction cases *)
+
+let inherit_evar_flags evar_flags evk evk' =
+  let evk_typeclass = Evar.Set.mem evk evar_flags.typeclass_evars in
+  let evk_obligation = Evar.Set.mem evk evar_flags.obligation_evars in
+  if not (evk_obligation || evk_typeclass) then evar_flags
+  else
+    let typeclass_evars =
+      if evk_typeclass then
+        let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in
+        Evar.Set.add evk' typeclass_evars
+      else evar_flags.typeclass_evars
+    in
+    let obligation_evars =
+      if evk_obligation then
+        let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in
+        Evar.Set.add evk' obligation_evars
+      else evar_flags.obligation_evars
+    in
+    { evar_flags with obligation_evars; typeclass_evars }
+
+(** Removal: in all other cases of definition *)
+
 let remove_evar_flags evk evar_flags =
-  { unresolvable_evars = Evar.Set.remove evk evar_flags.unresolvable_evars;
+  { typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars;
     obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
     (** Restriction information is kept. *)
     restricted_evars = evar_flags.restricted_evars }
@@ -506,9 +529,9 @@ let evar_counter_summary_name = "evar counter"
 let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name
 let new_untyped_evar () = incr evar_ctr; Evar.unsafe_of_int !evar_ctr
 
-let new_evar evd ?name evi =
+let new_evar evd ?name ?typeclass_candidate evi =
   let evk = new_untyped_evar () in
-  let evd = add_with_name evd ?name evk evi in
+  let evd = add_with_name evd ?name ?typeclass_candidate evk evi in
   (evd, evk)
 
 let remove d e =
@@ -630,7 +653,7 @@ let create_evar_defs sigma = { sigma with
 let empty_evar_flags =
   { obligation_evars = Evar.Set.empty;
     restricted_evars = Evar.Map.empty;
-    unresolvable_evars = Evar.Set.empty }
+    typeclass_evars = Evar.Set.empty }
 
 let empty = {
   defn_evars = EvMap.empty;
@@ -698,16 +721,26 @@ let define_aux def undef evk body =
   EvMap.add evk newinfo def, EvMap.remove evk undef
 
 (* define the existential of section path sp as the constr body *)
-let define evk body evd =
+let define_gen evk body evd evar_flags =
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   let last_mods = match evd.conv_pbs with
   | [] ->  evd.last_mods
   | _ -> Evar.Set.add evk evd.last_mods
   in
   let evar_names = EvNames.remove_name_defined evk evd.evar_names in
-  let evar_flags = remove_evar_flags evk evd.evar_flags in
   { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags }
 
+(** By default, the obligation and evar tag of the evar is removed *)
+let define evk body evd =
+  let evar_flags = remove_evar_flags evk evd.evar_flags in
+  define_gen evk body evd evar_flags
+
+(** In case of an evar-evar solution, the flags are inherited *)
+let define_with_evar evk body evd =
+  let evk' = fst (destEvar body) in
+  let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
+  define_gen evk body evd evar_flags
+
 let is_restricted_evar evd evk =
   try Some (Evar.Map.find evk evd.evar_flags.restricted_evars)
   with Not_found -> None
@@ -715,6 +748,9 @@ let is_restricted_evar evd evk =
 let declare_restricted_evar evar_flags evk evk' =
   { evar_flags with restricted_evars = Evar.Map.add evk evk' evar_flags.restricted_evars }
 
+(* In case of restriction, we declare the restriction and inherit the obligation
+   and typeclass flags. *)
+
 let restrict evk filter ?candidates ?src evd =
   let evk' = new_untyped_evar () in
   let evar_info = EvMap.find evk evd.undf_evars in
@@ -731,7 +767,7 @@ let restrict evk filter ?candidates ?src evd =
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
-  let evar_flags = inherit_unresolvable_evar evar_flags evk evk' in
+  let evar_flags = inherit_evar_flags evar_flags evk evk' in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
     defn_evars; last_mods; evar_names; evar_flags }, evk'