Move UnsatisfiableConstraints to a pretype error.

9 files changed, 100 insertions, 108 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 934e7bdbb..cad0beabf 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -51,6 +51,8 @@ type pretype_error =
   | NotProduct of constr
   | TypingError of type_error
   | CannotUnifyOccurrences of subterm_unification_error
+  | UnsatisfiableConstraints of
+    (existential_key * Evar_kinds.t) option * Evar.Set.t option
 
 exception PretypeError of env * Evd.evar_map * pretype_error
 
@@ -150,3 +152,20 @@ let error_not_product_loc loc env sigma c =
 
 let error_var_not_found_loc loc s =
   raise_pretype_error (loc, empty_env, Evd.empty, VarNotFound s)
+
+(*s Typeclass errors *)
+
+let unsatisfiable_constraints env evd ev comp =
+  match ev with
+  | None ->
+    let err = UnsatisfiableConstraints (None, comp) in
+    raise (PretypeError (env,evd,err))
+  | Some ev ->
+    let loc, kind = Evd.evar_source ev evd in
+    let err = UnsatisfiableConstraints (Some (ev, kind), comp) in
+    Loc.raise loc (PretypeError (env,evd,err))
+
+let unsatisfiable_exception exn =
+  match exn with
+  | PretypeError (_, _, UnsatisfiableConstraints _) -> true
+  | _ -> false
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index e816463e7..cc1443162 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -52,6 +52,9 @@ type pretype_error =
   | NotProduct of constr
   | TypingError of type_error
   | CannotUnifyOccurrences of subterm_unification_error
+  | UnsatisfiableConstraints of
+    (existential_key * Evar_kinds.t) option * Evar.Set.t option
+    (** unresolvable evar, connex component *)
 
 exception PretypeError of env * Evd.evar_map * pretype_error
 
@@ -134,3 +137,11 @@ val error_not_product_loc :
 (** {6 Error in conversion from AST to glob_constr } *)
 
 val error_var_not_found_loc : Loc.t -> Id.t -> 'b
+
+(** {6 Typeclass errors } *)
+
+val unsatisfiable_constraints : env -> Evd.evar_map -> Evd.evar option ->
+  Evar.Set.t option -> 'a
+
+val unsatisfiable_exception : exn -> bool
+
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index b16f000d4..816f03321 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -21,9 +21,6 @@ type contexts = Parameters | Properties
 type typeclass_error =
     | NotAClass of constr
     | UnboundMethod of global_reference * Id.t Loc.located (* Class name, method *)
-    | NoInstance of Id.t Loc.located * constr list
-    | UnsatisfiableConstraints of
-      evar_map * (existential_key * Evar_kinds.t) option * Evar.Set.t option
     | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
@@ -34,21 +31,4 @@ let not_a_class env c = typeclass_error env (NotAClass c)
 
 let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
 
-let no_instance env id args = typeclass_error env (NoInstance (id, args))
-
-let unsatisfiable_constraints env evd ev comp =
-  match ev with
-  | None ->
-    let err = UnsatisfiableConstraints (evd, None, comp) in
-    raise (TypeClassError (env, err))
-  | Some ev ->
-    let loc, kind = Evd.evar_source ev evd in
-    let err = UnsatisfiableConstraints (evd, Some (ev, kind), comp) in
-    Loc.raise loc (TypeClassError (env, err))
-
 let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
-
-let unsatisfiable_exception exn =
-  match exn with
-  | TypeClassError (_, UnsatisfiableConstraints _) -> true
-  | _ -> false
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index b3cfb37fa..c2a295bbc 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -20,10 +20,6 @@ type contexts = Parameters | Properties
 type typeclass_error =
   | NotAClass of constr
   | UnboundMethod of global_reference * Id.t located (** Class name, method *)
-  | NoInstance of Id.t located * constr list
-  | UnsatisfiableConstraints of
-    evar_map * (existential_key * Evar_kinds.t) option * Evar.Set.t option
-    (** evar map, unresolvable evar, connex component *)
   | MismatchedContextInstance of contexts * constr_expr list * rel_context (** found, expected *)
 
 exception TypeClassError of env * typeclass_error
@@ -32,11 +28,5 @@ val not_a_class : env -> constr -> 'a
 
 val unbound_method : env -> global_reference -> Id.t located -> 'a
 
-val no_instance : env -> Id.t located -> constr list -> 'a
-
-val unsatisfiable_constraints : env -> evar_map -> evar option ->
-  Evar.Set.t option -> 'a
-
 val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a
 
-val unsatisfiable_exception : exn -> bool
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ed01c6b7b..5f7e2916b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1337,7 +1337,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
        if closed0 cl && not (isEvar cl)
        then
 	 (try w_typed_unify env evd CONV flags op cl,cl
-	  with ex when Typeclasses_errors.unsatisfiable_exception ex ->
+	  with ex when Pretype_errors.unsatisfiable_exception ex ->
 	    bestexn := Some ex; error "Unsat")
        else error "Bound 1"
      with ex when precatchable_exception ex ->
diff --git a/proofs/logic.ml b/proofs/logic.ml
index dc8f31859..a7538193b 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -54,7 +54,8 @@ let is_unification_error = function
 | NoOccurrenceFound _ | CannotUnifyBindingType _
 | ActualTypeNotCoercible _ | UnifOccurCheck _
 | CannotFindWellTypedAbstraction _ | WrongAbstractionType _
-| UnsolvableImplicit _| AbstractionOverMeta _ -> true
+| UnsolvableImplicit _| AbstractionOverMeta _
+| UnsatisfiableConstraints _ -> true
 | _ -> false
 
 let catchable_exception = function
@@ -64,9 +65,7 @@ let catchable_exception = function
   (* reduction errors *)
   | Tacred.ReductionTacticError _ -> true
   (* unification and typing errors *)
-  | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e
-  | Typeclasses_errors.TypeClassError
-      (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
+  | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e 
   | _ -> false
 
 let error_no_such_hypothesis id = raise (RefinerError (NoSuchHyp id))
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 7c9aa59b6..9cf5aec04 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -602,8 +602,8 @@ let error_unresolvable env comp evd =
     else (found, accu)
    in
   let (_, ev) = Evd.fold_undefined fold evd (true, None) in
-  Typeclasses_errors.unsatisfiable_constraints
-    (Evarutil.nf_env_evar evd env) evd ev comp
+    Pretype_errors.unsatisfiable_constraints
+      (Evarutil.nf_env_evar evd env) evd ev comp
 
 (** Check if an evar is concerned by the current resolution attempt,
     (and in particular is in the current component), and also update
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 5d4a7509a..efcde3d1b 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -21,6 +21,7 @@ open Tacticals
 open Tacmach
 open Tactics
 open Clenv
+open Pretype_errors
 open Typeclasses
 open Typeclasses_errors
 open Classes
@@ -1449,10 +1450,11 @@ let cl_rewrite_clause_tac ?abs strat clause gl =
       let res = cl_rewrite_clause_aux ?abs strat (pf_env gl) [] sigma concl is_hyp in
 	treat res
     with
-    | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
+    | Pretype_errors.PretypeError (env, sigma, 
+				   (Pretype_errors.UnsatisfiableConstraints _ as e)) ->
 	Refiner.tclFAIL 0
 	  (str"Unable to satisfy the rewriting constraints."
-	   ++ fnl () ++ Himsg.explain_typeclass_error env e)
+	   ++ fnl () ++ Himsg.explain_pretype_error env sigma e)
   in tac gl
 
 
@@ -1535,9 +1537,9 @@ let cl_rewrite_clause_newtac ?abs strat clause =
         cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp
       in treat (res, is_hyp)
     with
-    | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
+    | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) ->
       raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
-                ++ fnl () ++ Himsg.explain_typeclass_error env e))
+			     ++ fnl () ++ Himsg.explain_pretype_error env evd e))
   end
 
 let newtactic_init_setoid () =
@@ -1905,13 +1907,12 @@ let unification_rewrite l2r c1 c2 cl car rel but env =
        ~flags:{ rewrite_unif_flags with Unification.resolve_evars = true } env
         cl.evd ((if l2r then c1 else c2),but)
     with
-    | ex when Pretype_errors.precatchable_exception ex || 
-      Typeclasses_errors.unsatisfiable_exception ex ->
-	  (* ~flags:(true,true) to make Ring work (since it really
-             exploits conversion) *)
-	  Unification.w_unify_to_subterm 
-	  ~flags:{ rewrite2_unif_flags with Unification.resolve_evars = true }
-	    env cl.evd ((if l2r then c1 else c2),but)
+    | ex when Pretype_errors.precatchable_exception ex ->
+	(* ~flags:(true,true) to make Ring work (since it really
+           exploits conversion) *)
+      Unification.w_unify_to_subterm 
+        ~flags:{ rewrite2_unif_flags with Unification.resolve_evars = true }
+        env cl.evd ((if l2r then c1 else c2),but)
   in
   let cl' = {cl with evd = evd'} in
   let cl' = Clenvtac.clenv_pose_dependent_evars true cl' in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index ae8e1f532..e3a303aed 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -660,6 +660,57 @@ let explain_cannot_unify_occurrences env sigma nested (cl2,pos2,t2) (cl1,pos1,t1
   pr_lconstr_env env t1 ++ strbrk " at position " ++ 
   pr_position (cl1,pos1) ++ ppreason ++ str "."
 
+let pr_constraints printenv env evd evars cstrs =
+  let (ev, evi) = Evar.Map.choose evars in
+    if Evar.Map.for_all (fun ev' evi' ->
+      eq_named_context_val evi.evar_hyps evi'.evar_hyps) evars
+    then
+      let l = Evar.Map.bindings evars in
+      let pe =
+        if printenv then
+          pr_ne_context_of (str "In environment:") (mt ())
+            (reset_with_named_context evi.evar_hyps env) ++ fnl ()
+        else mt ()
+      in
+      let evs =
+        prlist_with_sep (fun () -> fnl ())
+        (fun (ev, evi) -> str(string_of_existential ev) ++
+            str " : " ++ pr_lconstr evi.evar_concl) l
+      in
+      pe ++ evs ++ fnl() ++ h 0 (pr_evar_constraints cstrs)
+    else
+      let filter evk _ = Evar.Map.mem evk evars in
+      pr_evar_map_filter ~with_univs:false filter evd
+
+let explain_unsatisfiable_constraints env evd constr comp =
+  let (_, constraints) = Evd.extract_all_conv_pbs evd in
+  let undef = Evd.undefined_map (Evarutil.nf_evar_map_undefined evd) in
+  (** Only keep evars that are subject to resolution and members of the given
+     component. *)
+  let is_kept evk evi = match comp with
+  | None -> Typeclasses.is_resolvable evi
+  | Some comp -> Typeclasses.is_resolvable evi && Evar.Set.mem evk comp
+  in
+  let undef = 
+    let m = Evar.Map.filter is_kept undef in
+      if Evar.Map.is_empty m then undef
+      else m
+  in
+  match constr with
+  | None ->
+    str "Unable to satisfy the following constraints:" ++ fnl () ++
+    pr_constraints true env evd undef constraints
+  | Some (ev, k) ->
+    let cstr =
+      let remaining = Evar.Map.remove ev undef in
+      if not (Evar.Map.is_empty remaining) then
+        str "With the following constraints:" ++ fnl () ++
+          pr_constraints false env evd remaining constraints
+      else mt ()
+    in
+    let info = Evar.Map.find ev undef in
+    explain_typeclass_resolution env info k ++ fnl () ++ cstr
+
 let explain_pretype_error env sigma err =
   let env = Evarutil.env_nf_betaiotaevar sigma env in
   let env = make_all_name_different env in
@@ -693,7 +744,7 @@ let explain_pretype_error env sigma err =
   | NonLinearUnification (m,c) -> explain_non_linear_unification env m c
   | TypingError t -> explain_type_error env sigma t
   | CannotUnifyOccurrences (b,c1,c2,e) -> explain_cannot_unify_occurrences env sigma b c1 c2 e
-
+  | UnsatisfiableConstraints (c,comp) -> explain_unsatisfiable_constraints env sigma c comp
 (* Module errors *)
 
 open Modops
@@ -850,62 +901,6 @@ let pr_constr_exprs exprs =
 	 (fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr d ++ pps)
          exprs (mt ()))
 
-let explain_no_instance env (_,id) l =
-  str "No instance found for class " ++ Nameops.pr_id id ++ spc () ++
-  str "applied to arguments" ++ spc () ++
-    pr_sequence (pr_lconstr_env env) l
-
-let pr_constraints printenv env evd evars cstrs =
-  let (ev, evi) = Evar.Map.choose evars in
-    if Evar.Map.for_all (fun ev' evi' ->
-      eq_named_context_val evi.evar_hyps evi'.evar_hyps) evars
-    then
-      let l = Evar.Map.bindings evars in
-      let pe =
-        if printenv then
-          pr_ne_context_of (str "In environment:") (mt ())
-            (reset_with_named_context evi.evar_hyps env) ++ fnl ()
-        else mt ()
-      in
-      let evs =
-        prlist_with_sep (fun () -> fnl ())
-        (fun (ev, evi) -> str(string_of_existential ev) ++
-            str " : " ++ pr_lconstr evi.evar_concl) l
-      in
-      pe ++ evs ++ fnl() ++ h 0 (pr_evar_constraints cstrs)
-    else
-      let filter evk _ = Evar.Map.mem evk evars in
-      pr_evar_map_filter ~with_univs:false filter evd
-
-let explain_unsatisfiable_constraints env evd constr comp =
-  let (_, constraints) = Evd.extract_all_conv_pbs evd in
-  let undef = Evd.undefined_map (Evarutil.nf_evar_map_undefined evd) in
-  (** Only keep evars that are subject to resolution and members of the given
-     component. *)
-  let is_kept evk evi = match comp with
-  | None -> Typeclasses.is_resolvable evi
-  | Some comp -> Typeclasses.is_resolvable evi && Evar.Set.mem evk comp
-  in
-  let undef = 
-    let m = Evar.Map.filter is_kept undef in
-      if Evar.Map.is_empty m then undef
-      else m
-  in
-  match constr with
-  | None ->
-    str "Unable to satisfy the following constraints:" ++ fnl () ++
-    pr_constraints true env evd undef constraints
-  | Some (ev, k) ->
-    let cstr =
-      let remaining = Evar.Map.remove ev undef in
-      if not (Evar.Map.is_empty remaining) then
-        str "With the following constraints:" ++ fnl () ++
-          pr_constraints false env evd remaining constraints
-      else mt ()
-    in
-    let info = Evar.Map.find ev undef in
-    explain_typeclass_resolution env info k ++ fnl () ++ cstr
-
 let explain_mismatched_contexts env c i j =
   str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
     hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env j) ++
@@ -915,9 +910,6 @@ let explain_mismatched_contexts env c i j =
 let explain_typeclass_error env = function
   | NotAClass c -> explain_not_a_class env c
   | UnboundMethod (cid, id) -> explain_unbound_method env cid id
-  | NoInstance (id, l) -> explain_no_instance env id l
-  | UnsatisfiableConstraints (evd, c, comp) ->
-      explain_unsatisfiable_constraints env evd c comp
   | MismatchedContextInstance (c,i,j) -> explain_mismatched_contexts env c i j
 
 (* Refiner errors *)