[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, 12 insertions, 10 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 69830960a9..4e1636e321 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -405,12 +405,13 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ =
 
 let default_source = Loc.tag @@ Evar_kinds.InternalHole
 
-let new_pure_evar_full evd evi =
-  let (evd, evk) = Evd.new_evar evd evi in
+let new_pure_evar_full evd ?typeclass_candidate evi =
+  let (evd, evk) = Evd.new_evar evd ?typeclass_candidate evi in
   let evd = Evd.declare_future_goal evk evd in
   (evd, evk)
 
-let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?(principal=false) sign evd typ =
+let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?typeclass_candidate
+    ?(principal=false) sign evd typ =
   let default_naming = IntroAnonymous in
   let naming = Option.default default_naming naming in
   let name = match naming with
@@ -429,21 +430,22 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?
     evar_source = src;
     evar_candidates = candidates }
   in
-  let (evd, newevk) = Evd.new_evar evd ?name evi in
+  let typeclass_candidate = if principal then Some false else typeclass_candidate in
+  let (evd, newevk) = Evd.new_evar evd ?name ?typeclass_candidate evi in
   let evd =
     if principal then Evd.declare_principal_goal newevk evd
     else Evd.declare_future_goal newevk evd
   in
   (evd, newevk)
 
-let new_evar_instance ?src ?filter ?candidates ?naming ?principal sign evd typ instance =
+let new_evar_instance ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ instance =
   let open EConstr in
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
-  let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?principal typ in
+  let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal typ in
   evd, mkEvar (newevk,Array.of_list instance)
 
-let new_evar_from_context ?src ?filter ?candidates ?naming ?principal sign evd typ =
+let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ =
   let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
   let instance =
     match filter with
@@ -453,7 +455,7 @@ let new_evar_from_context ?src ?filter ?candidates ?naming ?principal sign evd t
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
-let new_evar ?src ?filter ?candidates ?naming ?principal ?hypnaming env evd typ =
+let new_evar ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal ?hypnaming env evd typ =
   let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in
   let map c = csubst_subst subst c in
   let candidates = Option.map (fun l -> List.map map l) candidates in
@@ -461,11 +463,11 @@ let new_evar ?src ?filter ?candidates ?naming ?principal ?hypnaming env evd typ
     match filter with
     | None -> instance
     | Some filter -> Filter.filter_list filter instance in
-  new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?principal instance
+  new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal instance
 
 let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
   let (evd', s) = new_sort_variable rigid evd in
-  let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in
+  let (evd', e) = new_evar env evd' ?src ?filter ?naming ~typeclass_candidate:false ?principal ?hypnaming (EConstr.mkSort s) in
   evd', (e, s)
 
 let new_Type ?(rigid=Evd.univ_flexible) evd =