Merge PR #7941: Extend QuestionMark to produce a better error message in case of missing record field

17 files changed, 152 insertions, 23 deletions

diff --git a/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh b/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh
new file mode 100644
index 000000000..56c0dc343
--- /dev/null
+++ b/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "7941" ] || [ "$CI_BRANCH" = "jun-27-missing-record-field-error-message-quickfix" ]; then
+    Equations_CI_BRANCH=overlay-question-mark-extended-for-missing-record-field
+    Equations_CI_GITURL=https://github.com/bollu/Coq-Equations
+fi
diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml
index 12e2fda8e..ea1e57254 100644
--- a/engine/evar_kinds.ml
+++ b/engine/evar_kinds.ml
@@ -21,12 +21,27 @@ type matching_var_kind = FirstOrderPatVar of Id.t | SecondOrderPatVar of Id.t
 
 type subevar_kind = Domain | Codomain | Body
 
+(* maybe this should be a Projection.t *)
+type record_field = { fieldname : Constant.t; recordname : Names.inductive }
+
+type question_mark = {
+     qm_obligation: obligation_definition_status;
+     qm_name: Name.t;
+     qm_record_field: record_field option;
+}
+
+let default_question_mark = {
+  qm_obligation=Define true;
+  qm_name=Anonymous;
+  qm_record_field=None;
+}
+
 type t =
   | ImplicitArg of GlobRef.t * (int * Id.t option)
      * bool (** Force inference *)
   | BinderType of Name.t
   | NamedHole of Id.t (* coming from some ?[id] syntax *)
-  | QuestionMark of obligation_definition_status * Name.t
+  | QuestionMark of question_mark
   | CasesType of bool (* true = a subterm of the type *)
   | InternalHole
   | TomatchTypeParameter of inductive * int
diff --git a/engine/evar_kinds.mli b/engine/evar_kinds.mli
new file mode 100644
index 000000000..4facdb200
--- /dev/null
+++ b/engine/evar_kinds.mli
@@ -0,0 +1,51 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+(** The kinds of existential variable *)
+
+(** Should the obligation be defined (opaque or transparent (default)) or
+    defined transparent and expanded in the term? *)
+
+type obligation_definition_status = Define of bool | Expand
+
+type matching_var_kind = FirstOrderPatVar of Id.t | SecondOrderPatVar of Id.t
+
+type subevar_kind = Domain | Codomain | Body
+
+(* maybe this should be a Projection.t *)
+(* Represents missing record field *)
+type record_field = { fieldname : Constant.t; recordname : Names.inductive }
+
+type question_mark = {
+     qm_obligation: obligation_definition_status;
+     qm_name: Name.t;
+     (* Tracks if the evar represents a missing record field *)
+     qm_record_field: record_field option;
+}
+
+(* Default value of question_mark which is used most often *)
+val default_question_mark : question_mark
+
+type t =
+  | ImplicitArg of GlobRef.t * (int * Id.t option)
+     * bool (** Force inference *)
+  | BinderType of Name.t
+  | NamedHole of Id.t (* coming from some ?[id] syntax *)
+  | QuestionMark of question_mark
+  | CasesType of bool (* true = a subterm of the type *)
+  | InternalHole
+  | TomatchTypeParameter of inductive * int
+  | GoalEvar
+  | ImpossibleCase
+  | MatchingVar of matching_var_kind
+  | VarInstance of Id.t
+  | SubEvar of subevar_kind option * Evar.t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index b4afb6415..12d31e5f4 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -754,7 +754,7 @@ let mark_in_evm ~goal evd content =
                - GoalEvar (morally not dependent)
                - VarInstance (morally dependent of some name).
                This is a heuristic for naming these evars. *)
-            | loc, (Evar_kinds.QuestionMark (_,Names.Name id) |
+  | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} |
                     Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
             | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
             | loc,_ -> loc,Evar_kinds.GoalEvar }
diff --git a/engine/termops.ml b/engine/termops.ml
index 2b179c43b..e4c8ae66b 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -114,7 +114,7 @@ let pr_evar_suggested_name evk sigma =
   | None -> match evi.evar_source with
   | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
   | _,Evar_kinds.VarInstance id -> id
-  | _,Evar_kinds.QuestionMark (_,Name id) -> id
+  | _,Evar_kinds.QuestionMark {Evar_kinds.qm_name = Name id} -> id
   | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
   | _ ->
       let env = reset_with_named_context evi.evar_hyps (Global.env()) in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9a4f2177f..cb50245d5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -566,7 +566,7 @@ let term_of_name = function
   | Name id -> DAst.make (GVar id)
   | Anonymous ->
        let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
-       DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), IntroAnonymous, None))
+    DAst.make (GHole (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=st }, IntroAnonymous, None))
 
 let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function
  | Anonymous -> (renaming,env), None, Anonymous
@@ -1370,7 +1370,8 @@ let sort_fields ~complete loc fields completer =
                (* the order does not matter as we sort them next,
                   List.rev_* is just for efficiency *)
                let remaining_fields =
-                 let complete_field (idx, _field_ref) = (idx, completer idx) in
+                 let complete_field (idx, field_ref) = (idx,
+                 completer idx field_ref record.Recordops.s_CONST) in
                  List.rev_map complete_field remaining_projs in
                List.rev_append remaining_fields acc
         in
@@ -1524,7 +1525,7 @@ let drop_notations_pattern looked_for genv =
     | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id)
     | CPatRecord l ->
       let sorted_fields =
-	sort_fields ~complete:false loc l (fun _idx -> CAst.make ?loc @@ CPatAtom None) in
+        sort_fields ~complete:false loc l (fun _idx fieldname constructor -> CAst.make ?loc @@ CPatAtom None) in
       begin match sorted_fields with
 	| None -> DAst.make ?loc @@ RCPatAtom None
 	| Some (n, head, pl) ->
@@ -1918,8 +1919,16 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
        let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
        let fields =
 	 sort_fields ~complete:true loc fs
-	             (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)),
-                                                           IntroAnonymous, None))
+                     (fun _idx fieldname constructorname ->
+                         let open Evar_kinds in
+                         let fieldinfo : Evar_kinds.record_field =
+                             {fieldname=fieldname; recordname=inductive_of_constructor constructorname}
+                             in
+                         CAst.make ?loc @@ CHole (Some
+                 (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with
+                     Evar_kinds.qm_obligation=st;
+                     Evar_kinds.qm_record_field=Some fieldinfo
+                }) , IntroAnonymous, None))
        in
        begin
 	  match fields with
@@ -2002,7 +2011,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
            let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
            (match naming with
            | IntroIdentifier id -> Evar_kinds.NamedHole id
-           | _ -> Evar_kinds.QuestionMark (st,Anonymous))
+           | _ -> Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=st; })
         | Some k -> k
         in
         let solve = match solve with
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index f24ab2bdd..dc027c404 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -604,8 +604,11 @@ let subst_var_with_hole occ tid t =
            else
 	     (incr locref;
               DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
-	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),
-                     IntroAnonymous, None)))
+              GHole (Evar_kinds.QuestionMark {
+                  Evar_kinds.qm_obligation=Evar_kinds.Define true;
+                  Evar_kinds.qm_name=Anonymous;
+                  Evar_kinds.qm_record_field=None;
+              }, IntroAnonymous, None)))
         else x
     | _ -> map_glob_constr_left_to_right substrec x in
   let t' = substrec t
@@ -616,13 +619,21 @@ let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
   let rec substrec c = match DAst.get c with
-    | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s) ->
+    | GHole (Evar_kinds.QuestionMark {
+                Evar_kinds.qm_obligation=Evar_kinds.Define true;
+                Evar_kinds.qm_name=Anonymous;
+                Evar_kinds.qm_record_field=None;
+            }, IntroAnonymous, s) ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
 	  (incr locref;
            DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
-           GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s))
+           GHole (Evar_kinds.QuestionMark {
+               Evar_kinds.qm_obligation=Evar_kinds.Define true;
+               Evar_kinds.qm_name=Anonymous;
+               Evar_kinds.qm_record_field=None;
+           },IntroAnonymous,s))
     | _ -> map_glob_constr_left_to_right substrec c
   in
   substrec t
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 2d72b9db6..6a63fb02f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2104,7 +2104,10 @@ let mk_JMeq_refl evdref typ x =
   papp evdref coq_JMeq_refl [| typ; x |]
 
 let hole na = DAst.make @@
-  GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na),
+  GHole (Evar_kinds.QuestionMark {
+      Evar_kinds.qm_obligation= Evar_kinds.Define false;
+      Evar_kinds.qm_name=na;
+      Evar_kinds.qm_record_field=None},
          IntroAnonymous, None)
 
 let constr_of_pat env evdref arsign pat avoid =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 5c4cbefad..7be05ea60 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -98,7 +98,11 @@ let inh_pattern_coerce_to ?loc env pat ind1 ind2 =
 open Program
 
 let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c =
-  let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in
+  let src = Loc.tag ?loc (Evar_kinds.QuestionMark {
+      Evar_kinds.default_question_mark with
+      Evar_kinds.qm_obligation=Evar_kinds.Define opaque;
+      Evar_kinds.qm_name=na;
+  }) in
   let evd, v = Evarutil.new_evar env !evdref ~src c in
   evdref := evd;
   v
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 4dfa789ba..24eb66682 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -562,7 +562,9 @@ let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?lo
   | PatVar (Name id) when not isclosed ->
       GVar id
   | PatVar Anonymous when not isclosed ->
-      GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Namegen.IntroAnonymous,None)
+      GHole (Evar_kinds.QuestionMark {
+        Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Define false;
+      },Namegen.IntroAnonymous,None)
   | _ -> raise Not_found
   ) x
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 57c4d363b..122979c1a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -381,8 +381,16 @@ let adjust_evar_source evdref na c =
   | Name id, Evar (evk,args) ->
      let evi = Evd.find !evdref evk in
      begin match evi.evar_source with
-     | loc, Evar_kinds.QuestionMark (b,Anonymous) ->
-        let src = (loc,Evar_kinds.QuestionMark (b,na)) in
+     | loc, Evar_kinds.QuestionMark {
+         Evar_kinds.qm_obligation=b;
+         Evar_kinds.qm_name=Anonymous;
+         Evar_kinds.qm_record_field=recfieldname;
+        } ->
+        let src = (loc,Evar_kinds.QuestionMark {
+            Evar_kinds.qm_obligation=b;
+            Evar_kinds.qm_name=na;
+            Evar_kinds.qm_record_field=recfieldname;
+        }) in
         let (evd, evk') = restrict_evar !evdref evk (evar_filter evi) ~src None in
         evdref := evd;
         mkEvar (evk',args)
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index f9c4bed35..7da059ae3 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -263,7 +263,9 @@ open Evar_kinds
 let mkPattern c = snd (Patternops.pattern_of_glob_constr c)
 let mkGApp f args = DAst.make @@ GApp (f, args)
 let mkGHole = DAst.make @@
-  GHole (QuestionMark (Define false,Anonymous), Namegen.IntroAnonymous, None)
+  GHole (QuestionMark {
+        Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Define false;
+  }, Namegen.IntroAnonymous, None)
 let mkGProd id c1 c2 = DAst.make @@
   GProd (Name (Id.of_string id), Explicit, c1, c2)
 let mkGArrow c1 c2 = DAst.make @@
diff --git a/test-suite/output/RecordMissingField.out b/test-suite/output/RecordMissingField.out
new file mode 100644
index 000000000..7c80a6065
--- /dev/null
+++ b/test-suite/output/RecordMissingField.out
@@ -0,0 +1,4 @@
+File "stdin", line 8, characters 5-22:
+Error: Cannot infer field y2p of record point2d in environment:
+p : point2d
+
diff --git a/test-suite/output/RecordMissingField.v b/test-suite/output/RecordMissingField.v
new file mode 100644
index 000000000..84f1748fa
--- /dev/null
+++ b/test-suite/output/RecordMissingField.v
@@ -0,0 +1,8 @@
+(** Check for error message when missing a record field. Error message
+should contain missing field, and the inferred type of the record **)
+
+Record point2d := mkPoint { x2p: nat; y2p: nat }.
+
+
+Definition increment_x (p: point2d) : point2d :=
+  {| x2p := x2p p + 1; |}.
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index eef7afbfb..102a98f04 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -187,7 +187,9 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let sigma, def =
     let sigma, h_a_term = Evarutil.new_global sigma (delayed_force fix_sub_ref) in
     let sigma, h_e_term = Evarutil.new_evar env sigma
-        ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in
+        ~src:(Loc.tag @@ Evar_kinds.QuestionMark {
+            Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Evar_kinds.Define false;
+        }) wf_proof in
     sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |])
   in
   let sigma, def = Typing.solve_evars env sigma def in
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 534e58f9c..c49ffe267 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -520,11 +520,15 @@ let pr_trailing_ne_context_of env sigma =
   then str "."
   else (str " in environment:"++ pr_context_unlimited env sigma)
 
-let rec explain_evar_kind env sigma evk ty = function
+let rec explain_evar_kind env sigma evk ty =
+    let open Evar_kinds in
+    function
   | Evar_kinds.NamedHole id ->
       strbrk "the existential variable named " ++ Id.print id
-  | Evar_kinds.QuestionMark _ ->
+  | Evar_kinds.QuestionMark {qm_record_field=None} ->
       strbrk "this placeholder of type " ++ ty
+  | Evar_kinds.QuestionMark {qm_record_field=Some {fieldname; recordname}} ->
+          str "field " ++ (Printer.pr_constant env fieldname) ++ str " of record " ++ (Printer.pr_inductive env recordname)
   | Evar_kinds.CasesType false ->
       strbrk "the type of this pattern-matching problem"
   | Evar_kinds.CasesType true ->
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 1f401b4e1..14d764232 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -220,7 +220,7 @@ let eterm_obligations env name evm fs ?status t ty =
 	 in
 	 let loc, k = evar_source id evm in
 	 let status = match k with
-           | Evar_kinds.QuestionMark (o,_) -> o
+           | Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o
            | _ -> match status with
                  | Some o -> o
                  | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))