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

5 files changed, 55 insertions, 13 deletions

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