test-suite/bugs/closed/5368.v


1
2
3
4
5
6

Set Universe Polymorphism.

Record cantype := {T:Type; op:T -> unit}.
Canonical Structure test (P:Type) := {| T := P -> Type; op := fun _ => tt|}.

Check (op _ ((fun (_:unit) => Set):_)).