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).

2 files changed, 41 insertions, 51 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