Evd/evarsolve: add an abstraction field to evars for unification

Named evar_abstract_arguments, this field indicates if the evar
arguments corresponding to certain hypothesis can be immitated during
inversion or not. If the argument comes from an abstraction (the evar
was of arrow type), then imitation is disallowed as it gives unnatural
solutions, and lambda abstraction is preferred.

1 files changed, 10 insertions, 6 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index d70c009c6d..840c14b241 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -424,8 +424,8 @@ let new_pure_evar_full evd ?typeclass_candidate evi =
   let evd = Evd.declare_future_goal evk evd in
   (evd, evk)
 
-let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?typeclass_candidate
-    ?(principal=false) sign evd typ =
+let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.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
@@ -441,6 +441,7 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?
     evar_concl = typ;
     evar_body = Evar_empty;
     evar_filter = filter;
+    evar_abstract_arguments = abstract_arguments;
     evar_source = src;
     evar_candidates = candidates }
   in
@@ -452,11 +453,12 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?
   in
   (evd, newevk)
 
-let new_evar_instance ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ instance =
+let new_evar_instance ?src ?filter ?abstract_arguments ?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 ?typeclass_candidate ?principal typ in
+  let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in
   evd, mkEvar (newevk,Array.of_list instance)
 
 let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ =
@@ -469,7 +471,8 @@ let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate
 
 (* [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 ?typeclass_candidate ?principal ?hypnaming env evd typ =
+let new_evar ?src ?filter ?abstract_arguments ?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
@@ -477,7 +480,8 @@ let new_evar ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal ?h
     match filter with
     | None -> instance
     | Some filter -> Filter.filter_list filter instance in
-  new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal instance
+  new_evar_instance sign evd typ' ?src ?filter ?abstract_arguments ?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