test-suite/bugs/4624.v


1
2
3
4
5
6
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) : _).