1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/bugs/4624.v b/test-suite/bugs/4624.v
new file mode 100644
index 00000000..a737afcd
--- /dev/null
+++ b/test-suite/bugs/4624.v
@@ -0,0 +1,7 @@
+Record foo := mkfoo { type : Type }.
+
+Canonical Structure fooA (T : Type) := mkfoo (T -> T).
+
+Definition id (t : foo) (x : type t) := x.
+
+Definition bar := id _ ((fun x : nat => x) : _).
+\ No newline at end of file