Rework typeclass resolution and control of backtracking.

Add a global option to check for multiple solutions and fail in that
case.
Add another flag to declare classes as having unique instances (not
checked but assumed correct, avoiding some backtracking).

10 files changed, 261 insertions, 179 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index c74ed19a8..a391a785c 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -20,6 +20,21 @@ open Typeclasses_errors
 open Libobject
 (*i*)
 
+let typeclasses_unique_solutions = ref false
+let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d
+let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions
+
+open Goptions
+
+let set_typeclasses_unique_solutions =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "check that typeclasses proof search returns unique solutions";
+      optkey   = ["Typeclasses";"Unique";"Solutions"];
+      optread  = get_typeclasses_unique_solutions;
+      optwrite = set_typeclasses_unique_solutions; }
+
 let (add_instance_hint, add_instance_hint_hook) = Hook.make ()
 let add_instance_hint id = Hook.get add_instance_hint id
 
@@ -32,10 +47,10 @@ let set_typeclass_transparency gr local c = Hook.get set_typeclass_transparency
 let (classes_transparent_state, classes_transparent_state_hook) = Hook.make ()
 let classes_transparent_state () = Hook.get classes_transparent_state ()
 
-let solve_instantiation_problem = ref (fun _ _ _ -> assert false)
+let solve_instantiation_problem = ref (fun _ _ _ _ -> assert false)
 
-let resolve_one_typeclass env evm t =
-  !solve_instantiation_problem env evm t
+let resolve_one_typeclass ?(unique=get_typeclasses_unique_solutions ()) env evm t =
+  !solve_instantiation_problem env evm t unique
 
 type direction = Forward | Backward
 
@@ -54,6 +69,8 @@ type typeclass = {
   cl_projs : (Name.t * (direction * int option) option * constant option) list;
   
   cl_strict : bool;
+
+  cl_unique : bool;
 }
 
 type typeclasses = typeclass Refmap.t
@@ -177,7 +194,8 @@ let subst_class (subst,cl) =
     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_strict = cl.cl_strict }
+    cl_strict = cl.cl_strict;
+    cl_unique = cl.cl_unique }
 
 let discharge_class (_,cl) =
   let repl = Lib.replacement_context () in
@@ -223,6 +241,7 @@ let discharge_class (_,cl) =
 	cl_props = props;
 	cl_projs = List.smartmap discharge_proj cl.cl_projs;
 	cl_strict = cl.cl_strict;
+	cl_unique = cl.cl_unique
       }
 
 let rebuild_class cl = 
@@ -409,36 +428,6 @@ let add_class cl =
 
 
 open Declarations
-
-let add_constant_class cst =
-  let ty = Universes.unsafe_type_of_global (ConstRef cst) in
-  let ctx, arity = decompose_prod_assum ty in
-  let tc = 
-    { cl_impl = ConstRef cst;
-      cl_context = (List.map (const None) ctx, ctx);
-      cl_props = [(Anonymous, None, arity)];
-      cl_projs = [];
-      cl_strict = false;
-    }
-  in add_class tc;
-    set_typeclass_transparency (EvalConstRef cst) false false
-      
-let add_inductive_class ind =
-  let mind, oneind = Global.lookup_inductive ind in
-  let k =
-    let ctx = oneind.mind_arity_ctxt in
-    let inst = Univ.UContext.instance mind.mind_universes in
-    let ty = Inductive.type_of_inductive_knowing_parameters
-      (push_rel_context ctx (Global.env ()))
-      ((mind,oneind),inst)
-      (Array.map (fun x -> lazy x) (Termops.extended_rel_vect 0 ctx))
-    in
-      { cl_impl = IndRef ind;
-	cl_context = List.map (const None) ctx, ctx;
-	cl_props = [Anonymous, None, ty];
-	cl_projs = [];
-	cl_strict = false }
-  in add_class k
       
 (*
  * interface functions
@@ -497,7 +486,7 @@ let is_instance = function
   | _ -> false
 
 let is_implicit_arg = function
-| Evar_kinds.GoalEvar _ -> false
+| Evar_kinds.GoalEvar -> false
 | _ -> true
   (* match k with *)
   (*     ImplicitArg (ref, (n, id), b) -> true *)
@@ -538,10 +527,10 @@ open Evar_kinds
 type evar_filter = existential_key -> Evar_kinds.t -> bool
 
 let all_evars _ _ = true
-let all_goals _ = function GoalEvar _ -> true | _ -> false
+let all_goals _ = function GoalEvar -> true | _ -> false
 let no_goals ev evi = not (all_goals ev evi)
 let no_goals_or_obligations _ = function
-  | GoalEvar _ | QuestionMark _ -> false
+  | GoalEvar | QuestionMark _ -> false
   | _ -> true
 
 let mark_resolvability filter b sigma =
@@ -560,15 +549,16 @@ let has_typeclasses filter evd =
   in
   Evar.Map.exists check (Evd.undefined_map evd)
 
-let solve_instantiations_problem = ref (fun _ _ _ _ _ -> assert false)
+let solve_instantiations_problem = ref (fun _ _ _ _ _ _ -> assert false)
 
-let solve_problem env evd filter split fail =
-  !solve_instantiations_problem env evd filter split fail
+let solve_problem env evd filter unique split fail =
+  !solve_instantiations_problem env evd filter unique split fail
 
 (** Profiling resolution of typeclasses *)
 (* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *)
 (* let solve_problem = Profile.profile5 solve_classeskey solve_problem *)
 
-let resolve_typeclasses ?(filter=no_goals) ?(split=true) ?(fail=true) env evd =
+let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
+    ?(split=true) ?(fail=true) env evd =
   if not (has_typeclasses filter evd) then evd
-  else solve_problem env evd filter split fail
+  else solve_problem env evd filter unique split fail
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index b1f816e65..447df1da1 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -37,6 +37,10 @@ type typeclass = {
 
   (** Whether we use matching or full unification during resolution *)
   cl_strict : bool; 
+
+  (** Whether we can assume that instances are unique, which allows 
+      no backtracking and sharing of resolution. *)
+  cl_unique : bool; 
 }
 
 type instance
@@ -47,10 +51,6 @@ val all_instances : unit -> instance list
 
 val add_class : typeclass -> unit
 
-val add_constant_class : constant -> unit
-
-val add_inductive_class : inductive -> unit
-
 val new_instance : typeclass -> int option -> bool -> Decl_kinds.polymorphic -> 
   global_reference -> instance
 val add_instance : instance -> unit
@@ -104,9 +104,9 @@ val mark_resolvable : evar_info -> evar_info
 val is_class_evar : evar_map -> evar_info -> bool
 val is_class_type : evar_map -> types -> bool
 
-val resolve_typeclasses : ?filter:evar_filter -> ?split:bool -> ?fail:bool ->
-  env -> evar_map -> evar_map
-val resolve_one_typeclass : env -> evar_map -> types -> open_constr
+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 -> types -> open_constr
 
 val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t
 val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
@@ -122,8 +122,8 @@ val add_instance_hint : global_reference_or_constr -> global_reference list ->
   bool -> int option -> Decl_kinds.polymorphic -> unit
 val remove_instance_hint : global_reference -> unit
 
-val solve_instantiations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> evar_map) ref
-val solve_instantiation_problem : (env -> evar_map -> types -> open_constr) ref
+val solve_instantiations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) ref
+val solve_instantiation_problem : (env -> evar_map -> types -> bool -> open_constr) ref
 
 val declare_instance : int option -> bool -> global_reference -> unit
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 61e934770..29cc6f51a 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -216,7 +216,8 @@ let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) evs (Evarutil.nf_
 let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l)
 
 type autoinfo = { hints : Auto.hint_db; is_evar: existential_key option;
-		  only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t;
+		  only_classes: bool; unique : bool;
+		  auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t;
 		  auto_path : global_reference option list;
 		  auto_cut : hints_path }
 type autogoal = goal * autoinfo
@@ -339,78 +340,100 @@ let normevars_tac : atac =
 let or_tac (x : 'a tac) (y : 'a tac) : 'a tac =
   { skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls }
 
-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 s concl in
-      let rec aux i foundone = function
-	| (tac, _, b, name, pp) :: tl ->
-	  let derivs = path_derivate info.auto_cut name in
-	  let res =
-            try
-		if path_matches derivs [] then None else Some (tac tacgl)
-	    with e when catchable e -> None
-	  in
-	    (match res with
-	       | None -> aux i foundone tl
-	       | Some {it = gls; sigma = s';} ->
-	    	   if !typeclasses_debug then
-		     msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
-			    ++ str" on" ++ spc () ++ pr_ev s gl);
-		   let fk =
-		     (fun () -> if !typeclasses_debug then msg_debug (str"backtracked after " ++ Lazy.force pp);
-			aux (succ i) true tl)
-		   in
-		   let sgls =
-		     evars_to_goals
-		       (fun evm ev evi ->
-			  if Typeclasses.is_resolvable evi &&
-			    (not info.only_classes || Typeclasses.is_class_evar evm evi)
-			  then Typeclasses.mark_unresolvable evi, true
-			  else evi, false) s'
-		   in
-		   let newgls, s' =
-		     let gls' = List.map (fun g -> (None, g)) gls in
-		       match sgls with
-		       | None -> gls', s'
-		       | Some (evgls, s') ->
-			 (* Reorder with dependent subgoals. *)
-			 (gls' @ List.map (fun (ev, x) -> Some ev, x) evgls, s')
-		   in
-		   let gls' = List.map_i
-		     (fun j (evar, g) ->
-			let info =
-			  { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp;
-			      is_evar = evar;
-			      hints =
-			      if b && not (Environ.eq_named_context_val (Goal.V82.hyps s' g) (Goal.V82.hyps s' gl))
-			      then make_autogoal_hints info.only_classes
-				~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s';}
-			      else info.hints;
-			      auto_cut = derivs }
-			in g, info) 1 newgls in
-		   let glsv = {it = gls'; sigma = s';} in
-		     sk glsv fk)
-	| [] ->
-	  if not foundone && !typeclasses_debug then
-	    msg_debug (pr_depth info.auto_depth ++ str": no match for " ++
-		     Printer.pr_constr_env (Goal.V82.env s gl) s concl ++
-		     spc () ++ int (List.length poss) ++ str" possibilities");
-	  fk ()
-    in aux 1 false poss }
-
-let isProp env sigma concl =
+let is_Prop env sigma concl =
   let ty = Retyping.get_type_of env sigma concl in
   match kind_of_term ty with
   | Sort (Prop Null) -> true
   | _ -> false
 
-let needs_backtrack only_classes env evd oev concl =
-  if Option.is_empty oev || isProp env evd concl then
-    not (Evar.Set.is_empty (Evarutil.evars_of_term concl))
+let is_unique env concl = 
+  try 
+    let (cl,u), args = dest_class_app env concl in
+      cl.cl_unique
+  with _ -> false
+
+let needs_backtrack env evd oev concl =
+  if Option.is_empty oev || is_Prop env evd concl then
+    occur_existential concl
   else true
 
+let hints_tac hints =
+  { skft = fun sk fk {it = gl,info; sigma = s;} ->
+      let env = Goal.V82.env s gl in
+      let concl = Goal.V82.concl s gl in
+      let tacgl = {it = gl; sigma = s;} in
+      let poss = e_possible_resolve hints info.hints s concl in
+      let unique = is_unique env concl in
+      let rec aux i foundone = function
+      | (tac, _, b, name, pp) :: tl ->
+	let derivs = path_derivate info.auto_cut name in
+	let res =
+          try
+	    if path_matches derivs [] then None else Some (tac tacgl)
+	  with e when catchable e -> None
+	in
+	  (match res with
+	  | None -> aux i foundone tl
+	  | Some {it = gls; sigma = s';} ->
+	    if !typeclasses_debug then
+	      msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
+			 ++ str" on" ++ spc () ++ pr_ev s gl);
+	    let sgls =
+	      evars_to_goals
+		(fun evm ev evi ->
+		  if Typeclasses.is_resolvable evi &&
+		    (not info.only_classes || Typeclasses.is_class_evar evm evi)
+		  then Typeclasses.mark_unresolvable evi, true
+		  else evi, false) s'
+	    in
+	    let newgls, s' =
+	      let gls' = List.map (fun g -> (None, g)) gls in
+		match sgls with
+		| None -> gls', s'
+		| Some (evgls, s') ->
+		  (* Reorder with dependent subgoals. *)
+		  (gls' @ List.map (fun (ev, x) -> Some ev, x) evgls, s')
+	    in
+	    let gls' = List.map_i
+	      (fun j (evar, g) ->
+		let info =
+		  { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp;
+		    is_evar = evar;
+		    hints =
+		      if b && not (Environ.eq_named_context_val (Goal.V82.hyps s' g) 
+				     (Goal.V82.hyps s' gl))
+		      then make_autogoal_hints info.only_classes
+			~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s';}
+		      else info.hints;
+		    auto_cut = derivs }
+		in g, info) 1 newgls in
+	    let glsv = {it = gls'; sigma = s';} in
+	    let fk' =
+	      (fun () ->
+		let do_backtrack =
+		  if unique then occur_existential concl
+		  else if info.unique then true
+		  else if List.is_empty gls' then 
+		    needs_backtrack env s' info.is_evar concl
+		  else true
+		in
+		  if !typeclasses_debug then
+		    msg_debug 
+		      ((if do_backtrack then str"Backtracking after "
+			else str "Not backtracking after ")
+		       ++ Lazy.force pp);
+		  if do_backtrack then aux (succ i) true tl
+		  else fk ())
+	    in
+	      sk glsv fk')
+      | [] ->
+	if not foundone && !typeclasses_debug then
+	  msg_debug (pr_depth info.auto_depth ++ str": no match for " ++
+		       Printer.pr_constr_env (Goal.V82.env s gl) s concl ++
+		       spc () ++ str ", " ++ int (List.length poss) ++ str" possibilities");
+	fk ()
+      in aux 1 false poss }
+
 let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
   let rec aux s (acc : autogoal list list) fk = function
     | (gl,info) :: gls ->
@@ -418,21 +441,8 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk
 	 | Some ev when Evd.is_defined s ev -> aux s acc fk gls
 	 | _ ->
 	     second.skft
-	       (fun {it=gls';sigma=s'} fk' ->
-		  let needs_backtrack =
-		    if List.is_empty gls' then
- 		      needs_backtrack info.only_classes
-		        (Goal.V82.env s gl) s' info.is_evar (Goal.V82.concl s gl)
-		    else true
-		  in
-		  let fk'' =
-		    if not needs_backtrack then
-		      (if !typeclasses_debug then
-			  msg_debug (str"no backtrack on " ++ pr_ev s gl ++
-				     str " after " ++ Lazy.force info.auto_last_tac);
-		       fk)
-		    else fk'
-		  in aux s' (gls'::acc) fk'' gls)
+	       (fun {it=gls';sigma=s'} fk' -> 
+		 aux s' (gls'::acc) fk' gls)
 	       fk {it = (gl,info); sigma = s; })
     | [] -> Somek2 (List.rev acc, s, fk)
   in fun {it = gls; sigma = s; } fk ->
@@ -466,9 +476,9 @@ let rec fix_limit limit (t : 'a tac) : 'a tac =
   if Int.equal limit 0 then fail_tac
   else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk }
 
-let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) cut ev g =
+let make_autogoal ?(only_classes=true) ?(unique=false) ?(st=full_transparent_state) cut ev g =
   let hints = make_autogoal_hints only_classes ~st g in
-    (g.it, { hints = hints ; is_evar = ev;
+    (g.it, { hints = hints ; is_evar = ev; unique = unique;
 	     only_classes = only_classes; auto_depth = []; auto_last_tac = lazy (str"none");
 	     auto_path = []; auto_cut = cut })
 
@@ -476,10 +486,12 @@ let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) cut ev g =
 let cut_of_hints h =
   List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h
 
-let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) hints gs evm' =
+let make_autogoals ?(only_classes=true) ?(unique=false) 
+    ?(st=full_transparent_state) hints gs evm' =
   let cut = cut_of_hints hints in
   { it = List.map_i (fun i g ->
-    let (gl, auto) = make_autogoal ~only_classes ~st cut (Some (fst g)) {it = snd g; sigma = evm'; } in
+    let (gl, auto) = make_autogoal ~only_classes ~unique 
+      ~st cut (Some (fst g)) {it = snd g; sigma = evm'; } in
       (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm'; }
 
 let get_result r =
@@ -487,11 +499,12 @@ let get_result r =
   | Nonek -> None
   | Somek (gls, fk) -> Some (gls.sigma,fk)
 
-let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm hints tac =
+let run_on_evars ?(only_classes=true) ?(unique=false) ?(st=full_transparent_state) p evm hints tac =
   match evars_to_goals p evm with
   | None -> None (* This happens only because there's no evar having p *)
   | Some (goals, evm') ->
-      let res = run_list_tac tac p goals (make_autogoals ~only_classes ~st hints goals evm') in
+      let res = run_list_tac tac p goals 
+	(make_autogoals ~only_classes ~unique ~st hints goals evm') in
 	match get_result res with
 	| None -> raise Not_found
 	| Some (evm', fk) -> 
@@ -512,25 +525,22 @@ let eauto ?(only_classes=true) ?st ?limit hints g =
     | Some {it = goals; sigma = s; } ->
 	{it = List.map fst goals; sigma = s;}
 
-let real_eauto st ?limit hints p evd =
-  let rec aux evd fails =
-    let res, fails =
-      try run_on_evars ~st p evd hints (eauto_tac ?limit hints), fails
-      with Not_found ->
-	List.fold_right (fun fk (res, fails) ->
-	  match res with
-	  | Some r -> res, fk :: fails
-	  | None -> get_result (fk ()), fails)
-	  fails (None, [])
-    in
-      match res with
-      | None -> evd
-      | Some (evd', fk) -> aux evd' (fk :: fails)
-  in aux evd []
-
-let resolve_all_evars_once debug limit p evd =
+let real_eauto ?limit unique st hints p evd =
+  let res =
+    run_on_evars ~st ~unique p evd hints (eauto_tac ?limit hints)
+  in
+    match res with
+    | None -> evd
+    | Some (evd', fk) -> 
+      if unique then
+	(match get_result (fk ()) with
+	| Some (evd'', fk') -> error "Typeclass resolution gives multiple solutions"
+	| None -> evd')
+      else evd'
+    
+let resolve_all_evars_once debug limit unique p evd =
   let db = searchtable_map typeclasses_db in
-    real_eauto ?limit (Hint_db.transparent_state db) [db] p evd
+    real_eauto ?limit unique (Hint_db.transparent_state db) [db] p evd
 
 (** We compute dependencies via a union-find algorithm.
     Beware of the imperative effects on the partition structure,
@@ -552,7 +562,7 @@ let evar_dependencies evm p =
       in Intpart.union_set evars p)
     evm ()
 
-let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
+let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
   let nc, gl, subst, _, _ = Evarutil.push_rel_context_to_named_context env gl in
   let (gl,t,sigma) =
     Goal.V82.mk_goal sigma nc gl Store.empty in
@@ -567,7 +577,8 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
     evd, term
 
 let _ =
-  Typeclasses.solve_instantiation_problem := (fun x y z -> resolve_one_typeclass x ~sigma:y z)
+  Typeclasses.solve_instantiation_problem := 
+    (fun x y z w -> resolve_one_typeclass x ~sigma:y z w)
 
 (** [split_evars] returns groups of undefined evars according to dependencies *)
 
@@ -658,7 +669,7 @@ let revert_resolvability oevd evd =
 
 exception Unresolved
 
-let resolve_all_evars debug m env p oevd do_split fail =
+let resolve_all_evars debug m unique env p oevd do_split fail =
   let split = if do_split then split_evars oevd else [Evar.Set.empty] in
   let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true
   in
@@ -667,7 +678,7 @@ let resolve_all_evars debug m env p oevd do_split fail =
     | comp :: comps ->
       let p = select_and_update_evars p oevd (in_comp comp) in
       try
-	 let evd' = resolve_all_evars_once debug m p evd in
+	 let evd' = resolve_all_evars_once debug m unique p evd in
 	 if has_undefined p oevd evd' then raise Unresolved;
 	 docomp evd' comps
       with Unresolved | Not_found ->
@@ -684,16 +695,16 @@ let initial_select_evars filter =
     filter ev (snd evi.Evd.evar_source) &&
     Typeclasses.is_class_evar evd evi
 
-let resolve_typeclass_evars debug m env evd filter split fail =
+let resolve_typeclass_evars debug m unique env evd filter split fail =
   let evd =
     try Evarconv.consider_remaining_unif_problems
       ~ts:(Typeclasses.classes_transparent_state ()) env evd
     with e when Errors.noncritical e -> evd
   in
-    resolve_all_evars debug m env (initial_select_evars filter) evd split fail
+    resolve_all_evars debug m unique env (initial_select_evars filter) evd split fail
 
-let solve_inst debug depth env evd filter split fail =
-  resolve_typeclass_evars debug depth env evd filter split fail
+let solve_inst debug depth env evd filter unique split fail =
+  resolve_typeclass_evars debug depth unique env evd filter split fail
 
 let _ =
   Typeclasses.solve_instantiations_problem :=
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 8b25a9ebe..2972fbbb5 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -840,8 +840,6 @@ let apply_rule unify loccs : ('a * int) pure_strategy =
     else not (List.mem occ occs) 
   in
     fun (hypinfo, occ) env avoid t ty cstr evars ->
-      (* if not (eq_env !hypinfo.cl.env env) then *)
-      (* 	hypinfo := refresh_hypinfo env (goalevars evars) !hypinfo; *)
       let unif = unify hypinfo env evars t in
 	match unif with
 	| None -> ((hypinfo, occ), Fail)
diff --git a/test-suite/typeclasses/backtrack.v b/test-suite/typeclasses/backtrack.v
new file mode 100644
index 000000000..d3e21898d
--- /dev/null
+++ b/test-suite/typeclasses/backtrack.v
@@ -0,0 +1,41 @@
+Set Typeclasses Strict Resolution.
+
+(* Set Typeclasses Unique Instances *)
+(** This lets typeclass search assume that instance heads are unique,
+    so if one matches no other need to be tried,
+    avoiding backtracking (even in unique solutions mode) 
+    This is on a class-by-class basis.
+ *)
+
+(* Non unique *)
+Class B.
+Class A.
+Set Typeclasses Unique Instances.
+(* Unique *)
+Class D.
+Class C (A : Type) := c : A.
+Unset Typeclasses Unique Instances.
+Instance : B -> D -> C nat := fun _ _ => 0.
+Instance : A -> D -> C nat := fun _ _ => 0.
+Instance : B -> C bool := fun _ => true.
+
+Instance : forall A, C A -> C (option A) := fun A _ => None.
+
+Set Typeclasses Debug.
+
+Set Typeclasses Unique Solutions.
+(** This forces typeclass resolution to fail if at least two solutions 
+   exist to a given set of constraints. This is a global setting.
+   For constraints involving assumed unique instances, it will not fail
+   if two such instances could apply, however it will fail if two different
+   instances of a unique class could apply.
+ *)
+Fail Definition foo (d d' : D) (b b' : B) (a' a'' : A) := c : nat.
+Definition foo (d d' : D) (b b' : B) (a' : A) := c : nat.
+
+Fail Definition foo' (b b' : B) := _ : B.
+Unset Typeclasses Unique Solutions.
+Definition foo' (b b' : B) := _ : B.
+
+Set Typeclasses Unique Solutions.
+Definition foo'' (d d' : D) := _ : D.
\ No newline at end of file
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 3c29c5fcb..ad6c4236e 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -44,14 +44,7 @@ let _ =
   Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
   Hook.set Typeclasses.classes_transparent_state_hook
     (fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db))
-    
-let declare_class g =
-  match global g with
-  | ConstRef x -> Typeclasses.add_constant_class x
-  | IndRef x -> Typeclasses.add_inductive_class x
-  | _ -> user_err_loc (loc_of_reference g, "declare_class", 
-		      Pp.str"Unsupported class type, only constants and inductives are allowed")
-    
+        
 (** TODO: add subinstances *)
 let existing_instance glob g pri =
   let c = global g in
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 489f2aa5f..f0932c826 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -20,10 +20,6 @@ val mismatched_params : env -> constr_expr list -> rel_context -> 'a
 
 val mismatched_props : env -> constr_expr list -> rel_context -> 'a
 
-(** Post-hoc class declaration. *)
-
-val declare_class : reference -> unit
-
 (** Instance declaration *)
 
 val existing_instance : bool -> reference -> int option -> unit
diff --git a/toplevel/record.ml b/toplevel/record.ml
index d23338930..177aa1cd6 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -49,6 +49,16 @@ let _ =
       optread  = (fun () -> !typeclasses_strict);
       optwrite = (fun b -> typeclasses_strict := b); }
 
+let typeclasses_unique = ref false
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "unique typeclass instances";
+      optkey   = ["Typeclasses";"Unique";"Instances"];
+      optread  = (fun () -> !typeclasses_unique);
+      optwrite = (fun b -> typeclasses_unique := b); }
+
 let interp_fields_evars env evars impls_env nots l =
   List.fold_left2
     (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
@@ -431,6 +441,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity fieldim
   let k =
     { cl_impl = impl;
       cl_strict = !typeclasses_strict;
+      cl_unique = !typeclasses_unique;
       cl_context = ctx_context;
       cl_props = fields;
       cl_projs = projs }
@@ -440,6 +451,46 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity fieldim
 (*       k.cl_projs coers priorities; *)
   add_class k; impl
 
+
+let add_constant_class cst =
+  let ty = Universes.unsafe_type_of_global (ConstRef cst) in
+  let ctx, arity = decompose_prod_assum ty in
+  let tc = 
+    { cl_impl = ConstRef cst;
+      cl_context = (List.map (const None) ctx, ctx);
+      cl_props = [(Anonymous, None, arity)];
+      cl_projs = [];
+      cl_strict = !typeclasses_strict;
+      cl_unique = !typeclasses_unique
+    }
+  in add_class tc;
+    set_typeclass_transparency (EvalConstRef cst) false false
+      
+let add_inductive_class ind =
+  let mind, oneind = Global.lookup_inductive ind in
+  let k =
+    let ctx = oneind.mind_arity_ctxt in
+    let inst = Univ.UContext.instance mind.mind_universes in
+    let ty = Inductive.type_of_inductive_knowing_parameters
+      (push_rel_context ctx (Global.env ()))
+      ((mind,oneind),inst)
+      (Array.map (fun x -> lazy x) (Termops.extended_rel_vect 0 ctx))
+    in
+      { cl_impl = IndRef ind;
+	cl_context = List.map (const None) ctx, ctx;
+	cl_props = [Anonymous, None, ty];
+	cl_projs = [];
+	cl_strict = !typeclasses_strict;
+	cl_unique = !typeclasses_unique }
+  in add_class k
+
+let declare_existing_class g =
+  match g with
+  | ConstRef x -> add_constant_class x
+  | IndRef x -> add_inductive_class x
+  | _ -> user_err_loc (Loc.dummy_loc, "declare_existing_class", 
+		      Pp.str"Unsupported class type, only constants and inductives are allowed")
+
 open Vernacexpr
 
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 873e1ff0c..befa5f72c 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -40,3 +40,5 @@ val definition_structure :
   inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * lident with_coercion * local_binder list *
   (local_decl_expr with_instance with_priority with_notation) list *
   Id.t * constr_expr option -> global_reference
+
+val declare_existing_class : global_reference -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 97f7ace0d..490addddb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -792,7 +792,7 @@ let vernac_declare_instances locality ids pri =
   List.iter (fun id -> Classes.existing_instance glob id pri) ids
 
 let vernac_declare_class id =
-  Classes.declare_class id
+  Record.declare_existing_class (Nametab.global id)
 
 (***********)
 (* Solving *)