Tentatively more informative report of failure when inferring

pattern-matching predicate.

13 files changed, 70 insertions, 51 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a0654220e..0fbd3cff9 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1514,7 +1514,7 @@ let internalize globalenv env allow_patvar lvar c =
 		   GCases(Loc.ghost,Term.RegularStyle,(* Some (GSort (Loc.ghost,GType None)) *)None, (* "return Type" *)
 			  List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars, (* "match v1,..,vn" *)
 			  [Loc.ghost,[],thepats, (* "|p1,..,pn" *)
-			   Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType,Misctypes.IntroAnonymous,None)) rtnpo; (* "=> P" is there were a P "=> _" else *)
+			   Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None)) rtnpo; (* "=> P" is there were a P "=> _" else *)
 			   Loc.ghost,[],List.make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *)
 			   GHole(Loc.ghost,Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None) (* "=> _" *)]))
 	in
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index f77fc5a6a..aae6e95aa 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -21,11 +21,11 @@ type t =
      * bool (** Force inference *)
   | BinderType of Name.t
   | QuestionMark of obligation_definition_status
-  | CasesType
+  | CasesType of bool (* true = a subterm of the type *)
   | InternalHole
   | TomatchTypeParameter of inductive * int
   | GoalEvar
   | ImpossibleCase
   | MatchingVar of bool * Id.t
   | VarInstance of Id.t
-  | SubEvar of t
+  | SubEvar of Constr.existential_key
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index eeb367a43..cd3c6276a 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 cb5673c2e..0e1ecda5c 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 0fcff3d49..19a325df9 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 8e8bbf367..abb895e62 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 c9435b54c..0fe16f0ed 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 99b5a51f9..9b5b79284 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 5882d8b9c..122240621 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 f5aea567f..dfe018c33 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;
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 9256e10d6..bb7a3f2e3 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -477,17 +477,16 @@ module New = struct
       Evd.fold_undefined (fun evk evi acc ->
         if is_undefined_up_to_restriction sigma evk && not (Evd.mem origsigma evk)
         then
-          evi::acc
+          (evk,evi)::acc
         else
           acc)
         extsigma []
     in
     match rest with
     | [] -> ()
-    | evi :: _ ->
-      let (loc,k) = evi.Evd.evar_source in
-      let evi = Evarutil.nf_evar_info sigma evi in
-      Pretype_errors.error_unsolvable_implicit loc env sigma evi k None
+    | (evk,evi) :: _ ->
+      let (loc,_) = evi.Evd.evar_source in
+      Pretype_errors.error_unsolvable_implicit loc env sigma evk None
 
   let tclWITHHOLES accept_unresolved_holes tac sigma x =
     tclEVARMAP >>= fun sigma_initial ->
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 3c52a6a31..d16029400 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -501,34 +501,47 @@ let pr_trailing_ne_context_of env sigma =
   then str "."
   else (str " in environment:"++ fnl () ++ pr_context_unlimited env sigma)
 
-let rec explain_evar_kind env = function
-  | Evar_kinds.QuestionMark _ -> strbrk "this placeholder"
-  | Evar_kinds.CasesType ->
+let rec explain_evar_kind env sigma evk ty = function
+  | Evar_kinds.QuestionMark _ ->
+      strbrk "this placeholder of type " ++ ty
+  | Evar_kinds.CasesType false ->
       strbrk "the type of this pattern-matching problem"
+  | Evar_kinds.CasesType true ->
+      strbrk "a subterm of type " ++ ty ++
+      strbrk " in the type of this pattern-matching problem"
   | Evar_kinds.BinderType (Name id) ->
       strbrk "the type of " ++ Nameops.pr_id id
   | Evar_kinds.BinderType Anonymous ->
       strbrk "the type of this anonymous binder"
   | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
       let id = Option.get ido in
-      strbrk "the implicit parameter " ++
-      pr_id id ++ spc () ++ str "of" ++
-      spc () ++ Nametab.pr_global_env Id.Set.empty c
-  | Evar_kinds.InternalHole -> strbrk "an internal placeholder"
+      strbrk "the implicit parameter " ++ pr_id id ++ spc () ++ str "of" ++
+      spc () ++ Nametab.pr_global_env Id.Set.empty c ++
+      strbrk " whose type is " ++ ty
+  | Evar_kinds.InternalHole -> strbrk "an internal placeholder of type " ++ ty
   | Evar_kinds.TomatchTypeParameter (tyi,n) ->
       strbrk "the " ++ pr_nth n ++
       strbrk " argument of the inductive type (" ++ pr_inductive env tyi ++
       strbrk ") of this term"
   | Evar_kinds.GoalEvar ->
-      strbrk "an existential variable"
+      strbrk "an existential variable of type " ++ ty
   | Evar_kinds.ImpossibleCase ->
       strbrk "the type of an impossible pattern-matching clause"
   | Evar_kinds.MatchingVar _ ->
       assert false
   | Evar_kinds.VarInstance id ->
-      strbrk "an instance for the variable " ++ pr_id id
-  | Evar_kinds.SubEvar c ->
-      strbrk "a subterm of " ++ explain_evar_kind env c
+      strbrk "an instance of type " ++ ty ++
+      str " for the variable " ++ pr_id id
+  | Evar_kinds.SubEvar evk' ->
+      let evi = Evd.find sigma evk' in
+      let pc = match evi.evar_body with
+      | Evar_defined c -> pr_lconstr_env env sigma (Evarutil.nf_evar sigma c)
+      | Evar_empty -> assert false in
+      let ty' = Evarutil.nf_evar sigma evi.evar_concl in
+      pr_existential_key sigma evk ++ str " of type " ++ ty ++
+      str " in the partial instance " ++ pc ++
+      str " found for " ++ explain_evar_kind env sigma evk'
+      (pr_lconstr_env env sigma ty') (snd evi.evar_source)
 
 let explain_typeclass_resolution env sigma evi k =
   match Typeclasses.class_of_constr evi.evar_concl with
@@ -542,18 +555,19 @@ let explain_typeclass_resolution env sigma evi k =
 let explain_placeholder_kind env sigma c e =
   match e with
   | Some (SeveralInstancesFound n) ->
-      strbrk " (several distinct possible instances found)"
+      strbrk " (several distinct possible type class instances found)"
   | None ->
       match Typeclasses.class_of_constr c with
-      | Some _ -> strbrk " (no instance found)"
+      | Some _ -> strbrk " (no type class instance found)"
       | _ -> mt ()
 
-let explain_unsolvable_implicit env sigma evi k explain =
+let explain_unsolvable_implicit env sigma evk explain =
+  let evi = Evarutil.nf_evar_info sigma (Evd.find_undefined sigma evk) in
   let env = Evd.evar_filtered_env evi in
   let type_of_hole = pr_lconstr_env env sigma evi.evar_concl in
   let pe = pr_trailing_ne_context_of env sigma in
-  strbrk "Cannot infer " ++ explain_evar_kind env k ++
-  strbrk " of type "  ++ type_of_hole ++
+  strbrk "Cannot infer " ++
+  explain_evar_kind env sigma evk type_of_hole (snd evi.evar_source) ++
   explain_placeholder_kind env sigma evi.evar_concl explain ++ pe
 
 let explain_var_not_found env id =
@@ -757,7 +771,7 @@ let explain_pretype_error env sigma err =
     let j = {uj_val = c; uj_type = actty} in
     explain_actual_type env sigma j t (Some e)
   | UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs
-  | UnsolvableImplicit (evi,k,exp) -> explain_unsolvable_implicit env sigma evi k exp
+  | UnsolvableImplicit (evk,exp) -> explain_unsolvable_implicit env sigma evk exp
   | VarNotFound id -> explain_var_not_found env id
   | UnexpectedType (actual,expect) ->
     let env, actual, expect = contract2 env actual expect in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index be5711820..d5073802d 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -39,8 +39,7 @@ let check_evars env evm =
      | Evar_kinds.QuestionMark _
      | Evar_kinds.ImplicitArg (_,_,false) -> ()
      | _ ->
-       Pretype_errors.error_unsolvable_implicit loc env
-         evm (Evarutil.nf_evar_info evm evi) k None)
+       Pretype_errors.error_unsolvable_implicit loc env evm key None)
   (Evd.undefined_map evm)
 
 type oblinfo =