From 54562510ed05bacdf7c9c2a41bb104a68aeaa1c0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 29 Feb 2020 13:26:08 +0100
Subject: Be robust in calculating visible ids for non-registered constants.

The previous code was only doing that when either in debug or toplevel mode.
Unfortunately, when dealing with open modules the constants might not have
been registered yet, leading to printing failure. I do not see a reason
why this code should fail when used with globals without a user facing name
when the only goal is to compute a set of identifiers that might clash. Thus,
the above failsafe behaviour is now systematic.

Fixes #8206: Module signature error sometimes prints ??.
---
 engine/namegen.ml              | 16 +++++++++-------
 test-suite/output/bug_8206.out |  5 +++++
 test-suite/output/bug_8206.v   | 11 +++++++++++
 3 files changed, 25 insertions(+), 7 deletions(-)
 create mode 100644 test-suite/output/bug_8206.out
 create mode 100644 test-suite/output/bug_8206.v

diff --git a/engine/namegen.ml b/engine/namegen.ml
index bcc8c34a4d..d2c37fb716 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -259,15 +259,17 @@ let visible_ids sigma (nenv, c) =
     let (gseen, vseen, ids) = !accu in
     let g = global_of_constr c in
     if not (GlobRef.Set_env.mem g gseen) then
-      begin
-      try
       let gseen = GlobRef.Set_env.add g gseen in
-      let short = Nametab.shortest_qualid_of_global Id.Set.empty g in
-      let dir, id = repr_qualid short in
-      let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in
+      let ids = match Nametab.shortest_qualid_of_global Id.Set.empty g with
+      | short ->
+        let dir, id = repr_qualid short in
+        if DirPath.is_empty dir then Id.Set.add id ids else ids
+      | exception Not_found ->
+        (* This may happen if given pathological terms or when manipulating
+           open modules *)
+        ids
+      in
       accu := (gseen, vseen, ids)
-      with Not_found when !Flags.in_debugger || !Flags.in_toplevel -> ()
-      end
   | Rel p ->
     let (gseen, vseen, ids) = !accu in
     if p > n && not (Int.Set.mem p vseen) then
diff --git a/test-suite/output/bug_8206.out b/test-suite/output/bug_8206.out
new file mode 100644
index 0000000000..6015fe32f9
--- /dev/null
+++ b/test-suite/output/bug_8206.out
@@ -0,0 +1,5 @@
+File "stdin", line 11, characters 0-23:
+Error: Signature components for label homework do not match: expected type
+"forall a b : nat, bug_8206.M.add a b = bug_8206.M.add b a" but found type
+"nat -> forall b : nat, bug_8206.M.add 0 b = bug_8206.M.add b 0".
+
diff --git a/test-suite/output/bug_8206.v b/test-suite/output/bug_8206.v
new file mode 100644
index 0000000000..8d4e73dfac
--- /dev/null
+++ b/test-suite/output/bug_8206.v
@@ -0,0 +1,11 @@
+Module Type Sig.
+  Parameter add: nat -> nat -> nat.
+  Axiom homework: forall (a b: nat), add a b = add b a.
+End Sig.
+
+Module Impl.
+  Definition add(a b: nat) := plus a b.
+  Axiom homework: forall (a b: nat), add 0 b = add b 0.
+End Impl.
+
+Module M : Sig := Impl.
-- 
cgit v1.2.3