More detailed error messages for Canonical Structure, #6398

5 files changed, 35 insertions, 8 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 9ff9a75b3..ab1f3cd32 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -298,29 +298,40 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 
 (*s High-level declaration of a canonical structure *)
 
-let error_not_structure ref =
+let error_not_structure ref description =
   user_err ~hdr:"object_declare"
-    (Id.print (basename_of_global ref) ++ str" is not a structure object.")
+    (str"Could not declare a canonical structure " ++
+       (Id.print (basename_of_global ref) ++ str"." ++ spc() ++
+          str(description)))
 
 let check_and_decompose_canonical_structure ref =
-  let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
+  let sp =
+    match ref with
+      ConstRef sp -> sp
+    |  _ -> error_not_structure ref "Expected an instance of a record or structure."
+  in
   let env = Global.env () in
   let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
   let vc = match Environ.constant_opt_value_in env (sp, u) with
     | Some vc -> vc
-    | None -> error_not_structure ref in
+    | None -> error_not_structure ref "Could not find its value in the global environment." in
   let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in
   let body = EConstr.Unsafe.to_constr body in
   let f,args = match kind body with
     | App (f,args) -> f,args
-    | _ -> error_not_structure ref in
+    | _ ->
+       error_not_structure ref "Expected a record or structure constructor applied to arguments." in
   let indsp = match kind f with
     | Construct ((indsp,1),u) -> indsp
-    | _ -> error_not_structure ref in
-  let s = try lookup_structure indsp with Not_found -> error_not_structure ref in
+    | _ -> error_not_structure ref "Expected an instance of a record or structure." in
+  let s =
+    try lookup_structure indsp
+    with Not_found ->
+      error_not_structure ref
+        ("Could not find the record or structure " ^ (MutInd.to_string (fst indsp))) in
   let ntrue_projs = List.count snd s.s_PROJKIND in
   if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
-    error_not_structure ref;
+    error_not_structure ref "Got too few arguments to the record or structure constructor.";
   (sp,indsp)
 
 let declare_canonical_structure ref =
diff --git a/test-suite/output/ErrorInCanonicalStructures.out b/test-suite/output/ErrorInCanonicalStructures.out
new file mode 100644
index 000000000..73da4f44f
--- /dev/null
+++ b/test-suite/output/ErrorInCanonicalStructures.out
@@ -0,0 +1,5 @@
+File "stdin", line 3, characters 0-24:
+Error:
+Could not declare a canonical structure Foo.
+Expected an instance of a record or structure.
+
diff --git a/test-suite/output/ErrorInCanonicalStructures.v b/test-suite/output/ErrorInCanonicalStructures.v
new file mode 100644
index 000000000..49597df6f
--- /dev/null
+++ b/test-suite/output/ErrorInCanonicalStructures.v
@@ -0,0 +1,3 @@
+Record Foo := MkFoo { field1 : nat; field2 : nat -> nat }.
+
+Canonical Structure Foo.
diff --git a/test-suite/output/ErrorInCanonicalStructures2.out b/test-suite/output/ErrorInCanonicalStructures2.out
new file mode 100644
index 000000000..63a2871b8
--- /dev/null
+++ b/test-suite/output/ErrorInCanonicalStructures2.out
@@ -0,0 +1,5 @@
+File "stdin", line 3, characters 0-24:
+Error:
+Could not declare a canonical structure bar.
+Expected an instance of a record or structure.
+
diff --git a/test-suite/output/ErrorInCanonicalStructures2.v b/test-suite/output/ErrorInCanonicalStructures2.v
new file mode 100644
index 000000000..10ee177aa
--- /dev/null
+++ b/test-suite/output/ErrorInCanonicalStructures2.v
@@ -0,0 +1,3 @@
+Definition bar := 99.
+
+Canonical Structure bar.