Merge PR #8737: Correctly report non-projection fields in records

3 files changed, 83 insertions, 4 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6b22261a15..c03a5fee90 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -120,6 +120,9 @@ type internalization_error =
   | UnboundFixName of bool * Id.t
   | NonLinearPattern of Id.t
   | BadPatternsNumber of int * int
+  | NotAProjection of qualid
+  | NotAProjectionOf of qualid * qualid
+  | ProjectionsOfDifferentRecords of qualid * qualid
 
 exception InternalizationError of internalization_error Loc.located
 
@@ -145,6 +148,16 @@ let explain_bad_patterns_number n1 n2 =
   str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++
   str " but found " ++ int n2
 
+let explain_field_not_a_projection field_id =
+  pr_qualid field_id ++ str ": Not a projection"
+
+let explain_field_not_a_projection_of field_id inductive_id =
+  pr_qualid field_id ++ str ": Not a projection of inductive " ++ pr_qualid inductive_id
+
+let explain_projections_of_diff_records inductive1_id inductive2_id =
+  str "This record contains fields of both " ++ pr_qualid inductive1_id ++
+  str " and " ++ pr_qualid inductive2_id
+
 let explain_internalization_error e =
   let pp = match e with
   | VariableCapture (id,id') -> explain_variable_capture id id'
@@ -153,6 +166,11 @@ let explain_internalization_error e =
   | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id
   | NonLinearPattern id -> explain_non_linear_pattern id
   | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
+  | NotAProjection field_id -> explain_field_not_a_projection field_id
+  | NotAProjectionOf (field_id, inductive_id) ->
+    explain_field_not_a_projection_of field_id inductive_id
+  | ProjectionsOfDifferentRecords (inductive1_id, inductive2_id) ->
+    explain_projections_of_diff_records inductive1_id inductive2_id
   in pp ++ str "."
 
 let error_bad_inductive_type ?loc =
@@ -1281,6 +1299,10 @@ let check_duplicate loc fields =
     user_err ?loc (str "This record defines several times the field " ++
       pr_qualid r ++ str ".")
 
+let inductive_of_record loc record =
+  let inductive = IndRef (inductive_of_constructor record.Recordops.s_CONST) in
+  Nametab.shortest_qualid_of_global ?loc Id.Set.empty inductive
+
 (** [sort_fields ~complete loc fields completer] expects a list
     [fields] of field assignments [f = e1; g = e2; ...], where [f, g]
     are fields of a record and [e1] are "values" (either terms, when
@@ -1303,8 +1325,7 @@ let sort_fields ~complete loc fields completer =
             let gr = global_reference_of_reference first_field_ref in
             (gr, Recordops.find_projection gr)
           with Not_found ->
-            user_err ?loc ~hdr:"intern"
-                         (pr_qualid first_field_ref ++ str": Not a projection")
+            raise (InternalizationError(loc, NotAProjection first_field_ref))
         in
         (* the number of parameters *)
         let nparams = record.Recordops.s_EXPECTEDPARAM in
@@ -1363,12 +1384,18 @@ let sort_fields ~complete loc fields completer =
                with Not_found ->
                  user_err ?loc ~hdr:"intern"
                                (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in
+               let this_field_record = try Recordops.find_projection field_glob_ref
+                 with Not_found ->
+                   let inductive_ref = inductive_of_record loc record in
+                   raise (InternalizationError(loc, NotAProjectionOf (field_ref, inductive_ref)))
+               in
                let remaining_projs, (field_index, _) =
                  let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in
                  try CList.extract_first the_proj remaining_projs
                  with Not_found ->
-                   user_err ?loc 
-                     (str "This record contains fields of different records.")
+                   let ind1 = inductive_of_record loc record in
+                   let ind2 = inductive_of_record loc this_field_record in
+                   raise (InternalizationError(loc, ProjectionsOfDifferentRecords (ind1, ind2)))
                in
                index_fields fields remaining_projs ((field_index, field_value) :: acc)
             | [] ->
diff --git a/test-suite/output/RecordFieldErrors.out b/test-suite/output/RecordFieldErrors.out
new file mode 100644
index 0000000000..5b67f632c9
--- /dev/null
+++ b/test-suite/output/RecordFieldErrors.out
@@ -0,0 +1,14 @@
+The command has indeed failed with message:
+unit: Not a projection.
+The command has indeed failed with message:
+unit: Not a projection.
+The command has indeed failed with message:
+This record contains fields of both t and t'.
+The command has indeed failed with message:
+unit: Not a projection.
+The command has indeed failed with message:
+This record defines several times the field foo.
+The command has indeed failed with message:
+This record defines several times the field unit.
+The command has indeed failed with message:
+unit: Not a projection of inductive t.
diff --git a/test-suite/output/RecordFieldErrors.v b/test-suite/output/RecordFieldErrors.v
new file mode 100644
index 0000000000..27aa07822b
--- /dev/null
+++ b/test-suite/output/RecordFieldErrors.v
@@ -0,0 +1,38 @@
+(** Check that various errors in record fields are reported with the correct
+underlying issue. *)
+
+Record t :=
+  { foo: unit }.
+
+Record t' :=
+  { bar: unit }.
+
+Fail Check {| unit := tt |}.
+(* unit: Not a projection. *)
+
+Fail Check {| unit := tt;
+              foo := tt |}.
+(* unit: Not a projection. *)
+
+Fail Check {| foo := tt;
+              bar := tt |}.
+(* This record contains fields of both t and t'. *)
+
+Fail Check {| unit := tt;
+              unit := tt |}.
+(* unit: Not a projection. *)
+
+Fail Check {| foo := tt;
+              foo := tt |}.
+(* This record defines several times the field foo. *)
+
+Fail Check {| foo := tt;
+              unit := tt;
+              unit := tt |}.
+(* This is slightly wrong (would prefer "unit: Not a projection."), but it's
+acceptable and seems an unlikely mistake. *)
+(* This record defines several times the field unit. *)
+
+Fail Check {| foo := tt;
+              unit := tt |}.
+(* unit: Not a projection of inductive t. *)