Add a flag for restricting resolution of typeclasses to

matching (i.e. no instanciation of the goal evars).
Classes defined when [Set Typeclasses Strict Resolution] is on
use the restricted resolution for all their instances (except
for Hint Extern's).

4 files changed, 61 insertions, 29 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index b9c2bd1bb3..a3bd06ed5d 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -52,6 +52,8 @@ type typeclass = {
 
   (* The method implementaions as projections. *)
   cl_projs : (Name.t * (direction * int option) option * constant option) list;
+  
+  cl_strict : bool;
 }
 
 type typeclasses = typeclass Refmap.t
@@ -174,7 +176,8 @@ let subst_class (subst,cl) =
   { cl_impl = do_subst_gr cl.cl_impl;
     cl_context = do_subst_context cl.cl_context;
     cl_props = do_subst_ctx cl.cl_props;
-    cl_projs = do_subst_projs cl.cl_projs; }
+    cl_projs = do_subst_projs cl.cl_projs;
+    cl_strict = cl.cl_strict }
 
 let discharge_class (_,cl) =
   let repl = Lib.replacement_context () in
@@ -214,10 +217,13 @@ let discharge_class (_,cl) =
     let ctx, subst = rel_of_variable_context ctx in
     let context = discharge_context ctx subst cl.cl_context in
     let props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props in
-    { cl_impl = cl_impl';
-      cl_context = context;
-      cl_props = props;
-      cl_projs = List.smartmap (fun (x, y, z) -> x, y, Option.smartmap Lib.discharge_con z) cl.cl_projs }
+    let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in
+      { cl_impl = cl_impl';
+	cl_context = context;
+	cl_props = props;
+	cl_projs = List.smartmap discharge_proj cl.cl_projs;
+	cl_strict = cl.cl_strict;
+      }
 
 let rebuild_class cl = 
   try 
@@ -411,7 +417,8 @@ let add_constant_class cst =
     { cl_impl = ConstRef cst;
       cl_context = (List.map (const None) ctx, ctx);
       cl_props = [(Anonymous, None, arity)];
-      cl_projs = []
+      cl_projs = [];
+      cl_strict = false;
     }
   in add_class tc;
     set_typeclass_transparency (EvalConstRef cst) false false
@@ -429,7 +436,8 @@ let add_inductive_class ind =
       { cl_impl = IndRef ind;
 	cl_context = List.map (const None) ctx, ctx;
 	cl_props = [Anonymous, None, ty];
-	cl_projs = [] }
+	cl_projs = [];
+	cl_strict = false }
   in add_class k
       
 (*
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 7c3d2be09b..b1f816e651 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -34,6 +34,9 @@ type typeclass = {
       no name is provided. The [int option option] indicates subclasses whose hint has
       the given priority. *)
   cl_projs : (Name.t * (direction * int option) option * constant option) list;
+
+  (** Whether we use matching or full unification during resolution *)
+  cl_strict : bool; 
 }
 
 type instance
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index e298c31cb1..286ae7696b 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -52,7 +52,7 @@ open Auto
 
 open Unification
 
-let auto_core_unif_flags st = {
+let auto_core_unif_flags st freeze = {
   modulo_conv_on_closed_terms = Some st;
   use_metas_eagerly_in_conv_on_closed_terms = true;
   modulo_delta = st;
@@ -60,18 +60,19 @@ let auto_core_unif_flags st = {
   check_applied_meta_types = false;
   use_pattern_unification = true;
   use_meta_bound_pattern_unification = true;
-  frozen_evars = Evar.Set.empty;
+  frozen_evars = freeze;
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = true;
   modulo_eta = false;
 }
 
-let auto_unif_flags st = {
-  core_unify_flags = auto_core_unif_flags st;
-  merge_unify_flags = auto_core_unif_flags st;
-  subterm_unify_flags = auto_core_unif_flags st;
-  allow_K_in_toplevel_higher_order_unification = false;
-  resolve_evars = false
+let auto_unif_flags freeze st = 
+  let fl = auto_core_unif_flags st freeze in
+  { core_unify_flags = fl;
+    merge_unify_flags = fl;
+    subterm_unify_flags = fl;
+    allow_K_in_toplevel_higher_order_unification = false;
+    resolve_evars = false
 }
 
 let rec eq_constr_mod_evars x y =
@@ -115,7 +116,8 @@ let unify_resolve poly flags (c,clenv) gls =
   let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
   let clenv' = connect_clenv gls clenv' in
   let clenv' = clenv_unique_resolver ~flags clenv' gls in
-  Proofview.V82.of_tactic (Clenvtac.clenv_refine false(*uhoh, was true*) ~with_classes:false clenv') gls
+  Proofview.V82.of_tactic 
+    (Clenvtac.clenv_refine false ~with_classes:false clenv') gls
 
 let clenv_of_prods poly nprods (c, clenv) gls =
   if poly || Int.equal nprods 0 then Some clenv
@@ -143,22 +145,31 @@ let rec e_trivial_fail_db db_list local_db goal =
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
           (e_trivial_fail_db db_list
 	      (Hint_db.add_list hintl local_db) g'))) ::
-    (List.map (fun (x,_,_,_,_) -> x) (e_trivial_resolve db_list local_db (pf_concl goal)))
+    (List.map (fun (x,_,_,_,_) -> x) 
+     (e_trivial_resolve db_list local_db (project goal) (pf_concl goal)))
   in
   tclFIRST (List.map tclCOMPLETE tacl) goal
 
-and e_my_find_search db_list local_db hdc complete concl =
+and e_my_find_search db_list local_db hdc complete sigma concl =
   let hdc = head_of_constr_reference hdc in
   let prods, concl = decompose_prod_assum concl in
   let nprods = List.length prods in
+  let freeze = 
+    try
+      let cl = Typeclasses.class_info hdc in
+	if cl.cl_strict then
+	  Evarutil.evars_of_term concl
+	else Evar.Set.empty
+    with _ -> Evar.Set.empty
+  in
   let hintl =
     List.map_append
       (fun db ->
 	if Hint_db.use_dn db then
-	  let flags = auto_unif_flags (Hint_db.transparent_state db) in
+	  let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in
 	    List.map (fun x -> (flags, x)) (Hint_db.map_auto (hdc,concl) db)
 	else
-	  let flags = auto_unif_flags (Hint_db.transparent_state db) in
+	  let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in
 	    List.map (fun x -> (flags, x)) (Hint_db.map_all hdc db))
       (local_db::db_list)
   in
@@ -174,9 +185,7 @@ and e_my_find_search db_list local_db hdc complete concl =
 	        (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)
 	  | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])
 	  | Extern tacast ->
-(* 	    tclTHEN *)
-(* 	      (fun gl -> Refiner.tclEVARS (mark_unresolvables (project gl)) gl) *)
-	      Proofview.V82.of_tactic (conclPattern concl p tacast)
+	    Proofview.V82.of_tactic (conclPattern concl p tacast)
       in
       let tac = if complete then tclCOMPLETE tac else tac in
 	match t with
@@ -186,16 +195,16 @@ and e_my_find_search db_list local_db hdc complete concl =
 	    (tac,b,false, name, lazy (pr_autotactic t))
   in List.map tac_of_hint hintl
 
-and e_trivial_resolve db_list local_db gl =
+and e_trivial_resolve db_list local_db sigma concl =
   try
     e_my_find_search db_list local_db
-    (head_constr_bound gl) true gl
+     (head_constr_bound concl) true sigma concl
   with Bound | Not_found -> []
 
-let e_possible_resolve db_list local_db gl =
+let e_possible_resolve db_list local_db sigma concl =
   try
     e_my_find_search db_list local_db
-      (head_constr_bound gl) false gl
+      (head_constr_bound concl) false sigma concl
   with Bound | Not_found -> []
 
 let catchable = function
@@ -334,7 +343,7 @@ let hints_tac hints =
   { skft = fun sk fk {it = gl,info; sigma = s;} ->
       let concl = Goal.V82.concl s gl in
       let tacgl = {it = gl; sigma = s;} in
-      let poss = e_possible_resolve hints info.hints concl in
+      let poss = e_possible_resolve hints info.hints s concl in
       let rec aux i foundone = function
 	| (tac, _, b, name, pp) :: tl ->
 	  let derivs = path_derivate info.auto_cut name in
@@ -759,7 +768,8 @@ let is_ground c gl =
   else tclFAIL 0 (str"Not ground") gl
 
 let autoapply c i gl =
-  let flags = auto_unif_flags (Auto.Hint_db.transparent_state (Auto.searchtable_map i)) in
+  let flags = auto_unif_flags Evar.Set.empty 
+    (Auto.Hint_db.transparent_state (Auto.searchtable_map i)) in
   let cty = pf_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
   unify_e_resolve false flags (c,ce) gl
diff --git a/toplevel/record.ml b/toplevel/record.ml
index f3565a721d..2c8fa52b92 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -39,6 +39,16 @@ let _ =
       optread  = (fun () -> !primitive_flag) ;
       optwrite = (fun b -> primitive_flag := b) }
 
+let typeclasses_strict = ref false
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "strict typeclass resolution";
+      optkey   = ["Typeclasses";"Strict";"Resolution"];
+      optread  = (fun () -> !typeclasses_strict);
+      optwrite = (fun b -> typeclasses_strict := b); }
+
 let interp_fields_evars evars env impls_env nots l =
   List.fold_left2
     (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
@@ -420,6 +430,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity fieldim
   in
   let k =
     { cl_impl = impl;
+      cl_strict = !typeclasses_strict;
       cl_context = ctx_context;
       cl_props = fields;
       cl_projs = projs }