Tentatively more informative report of failure when inferring

pattern-matching predicate.

8 files changed, 31 insertions, 24 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index eeb367a43d..cd3c6276a0 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1586,8 +1586,11 @@ let rec list_assoc_in_triple x = function
  * similarly for each ti.
 *)
 
-let abstract_tycon loc env evdref subst _tycon extenv t =
-  let t = nf_betaiota !evdref t in (* it helps in some cases to remove K-redex *)
+let abstract_tycon loc env evdref subst tycon extenv t =
+  let t = nf_betaiota !evdref t in (* it helps in some cases to remove K-redex*)
+  let src = match kind_of_term t with
+    | Evar (evk,_) -> (loc,Evar_kinds.SubEvar evk)
+    | _ -> (loc,Evar_kinds.CasesType true) in
   let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv subst t in
   (* We traverse the type T of the original problem Xi looking for subterms
      that match the non-constructor part of the constraints (this part
@@ -1596,8 +1599,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
      convertible subterms of the substitution *)
   let rec aux (k,env,subst as x) t =
     let t = whd_evar !evdref t in match kind_of_term t with
-    | Rel n when pi2 (lookup_rel n env) != None ->
-        map_constr_with_full_binders push_binder aux x t
+    | Rel n when pi2 (lookup_rel n env) != None -> t
     | Evar ev ->
         let ty = get_type_of env !evdref t in
 	let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in
@@ -1606,7 +1608,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
 	    (fun i _ ->
               try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
               1 (rel_context env) in
-        let ev' = e_new_evar env evdref ~src:(loc, Evar_kinds.CasesType) ty in
+        let ev' = e_new_evar env evdref ~src ty in
         begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with
         | Success evd -> evdref := evd
         | UnifFailure _ -> assert false
@@ -1637,9 +1639,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
 	  (named_context extenv) in
       let filter = Filter.make (rel_filter @ named_filter) in
       let candidates = u :: List.map mkRel vl in
-      let ev =
-	e_new_evar extenv evdref ~src:(loc, Evar_kinds.CasesType)
-	  ~filter ~candidates ty in
+      let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in
       lift k ev
   in
   aux (0,extenv,subst0) t0
@@ -1913,7 +1913,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
 	| Some t -> sigma,t
 	| None -> 
 	  let sigma, (t, _) = 
-	    new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType) in
+	    new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in
 	    sigma, t
 	in
         (* First strategy: we build an "inversion" predicate *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index cb5673c2ea..0e1ecda5cf 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -552,7 +552,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let env1,rel_sign = env_rel_context_chop k env in
   let sign1 = evar_hyps evi1 in
   let filter1 = evar_filter evi1 in
-  let src = let (loc,k) = evi1.evar_source in (loc,Evar_kinds.SubEvar k) in
+  let src = subterm_source evk1 evi1.evar_source in
   let ids1 = List.map pi1 (named_context_of_val sign1) in
   let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in
   let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 0fcff3d492..19a325df94 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -650,9 +650,7 @@ let check_evars env initial_sigma sigma c =
             let (loc,k) = evar_source evk sigma in
 	      match k with
 	      | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
-	      | _ ->
-		  let evi = nf_evar_info sigma (Evd.find_undefined sigma evk) in
-		    error_unsolvable_implicit loc env sigma evi k None)
+	      | _ -> error_unsolvable_implicit loc env sigma evk None)
       | _ -> iter_constr proc_rec c
   in proc_rec c
 
@@ -834,3 +832,9 @@ let lift_tycon n = Option.map (lift n)
 let pr_tycon env = function
     None -> str "None"
   | Some t -> Termops.print_constr_env env t
+
+let subterm_source evk (loc,k) =
+  let evk = match k with
+    | Evar_kinds.SubEvar (evk) -> evk
+    | _ -> evk in
+  (loc,Evar_kinds.SubEvar evk)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 8e8bbf3679..abb895e62e 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -233,3 +233,6 @@ val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
 val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
 val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
+
+val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
+  Evar_kinds.t Loc.located
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c9435b54c9..0fe16f0edd 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1601,7 +1601,9 @@ let pr_decl ((id,b,_),ok) =
 
 let rec pr_evar_source = function
   | Evar_kinds.QuestionMark _ -> str "underscore"
-  | Evar_kinds.CasesType -> str "pattern-matching return predicate"
+  | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
+  | Evar_kinds.CasesType true ->
+      str "subterm of pattern-matching return predicate"
   | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id
   | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder"
   | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
@@ -1615,7 +1617,8 @@ let rec pr_evar_source = function
   | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
   | Evar_kinds.MatchingVar _ -> str "matching variable"
   | Evar_kinds.VarInstance id -> str "instance of " ++ pr_id id
-  | Evar_kinds.SubEvar k -> str "subterm of " ++ pr_evar_source k
+  | Evar_kinds.SubEvar evk ->
+      str "subterm of " ++ str (string_of_existential evk)
 
 let pr_evar_info evi =
   let phyps =
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 99b5a51f93..9b5b79284b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -36,8 +36,7 @@ type pretype_error =
   | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
   (* Tactic unification *)
   | UnifOccurCheck of existential_key * constr
-  | UnsolvableImplicit of Evd.evar_info * Evar_kinds.t *
-      Evd.unsolvability_explanation option
+  | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option
   | CannotUnify of constr * constr * unification_error option
   | CannotUnifyLocal of constr * constr * constr
   | CannotUnifyBindingType of constr * constr
@@ -107,9 +106,9 @@ let error_not_a_type_loc loc env sigma j =
 let error_occur_check env sigma ev c =
   raise (PretypeError (env, sigma, UnifOccurCheck (ev,c)))
 
-let error_unsolvable_implicit loc env sigma evi e explain =
+let error_unsolvable_implicit loc env sigma evk explain =
   Loc.raise loc
-    (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain)))
+    (PretypeError (env, sigma, UnsolvableImplicit (evk, explain)))
 
 let error_cannot_unify_loc loc env sigma ?reason (m,n) =
   Loc.raise loc (PretypeError (env, sigma,CannotUnify (m,n,reason)))
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 5882d8b9c2..1222406217 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -37,8 +37,7 @@ type pretype_error =
   | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
   (** Tactic Unification *)
   | UnifOccurCheck of existential_key * constr
-  | UnsolvableImplicit of Evd.evar_info * Evar_kinds.t *
-      Evd.unsolvability_explanation option
+  | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option
   | CannotUnify of constr * constr * unification_error option
   | CannotUnifyLocal of constr * constr * constr
   | CannotUnifyBindingType of constr * constr
@@ -100,7 +99,7 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
 val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
 
 val error_unsolvable_implicit :
-  Loc.t -> env -> Evd.evar_map -> Evd.evar_info -> Evar_kinds.t ->
+  Loc.t -> env -> Evd.evar_map -> existential_key ->
       Evd.unsolvability_explanation option -> 'b
 
 val error_cannot_unify_loc : Loc.t -> env -> Evd.evar_map ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f5aea567f4..dfe018c33b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -190,8 +190,7 @@ let check_extra_evars_are_solved env current_sigma pending =
 	match k with
 	| Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
 	| _ ->
-	    let evi = nf_evar_info current_sigma (Evd.find_undefined current_sigma evk) in
-	    error_unsolvable_implicit loc env current_sigma evi k None) pending
+	    error_unsolvable_implicit loc env current_sigma evk None) pending
 
 let check_evars_are_solved env current_sigma pending =
   check_typeclasses_instances_are_solved env current_sigma pending;