Test file for #4624, fixed by Matthieu's bfce815bd1.

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 0000000000..a737afcdab
--- /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