1 2 3 4
(* This used to fail with an anomaly NotASort at some time *) Class A (O: Type): Type := a: O -> Type. Fail Goal forall (x: a tt), @a x = @a x.