Issue659.err

Issue659.agda:41,11-15
((r₁ : (ℓ : Level) → R ℓ) {a : Level} {A : Set a} → A → A) !=<
(P _k_32 _A_34) because this would result in an invalid use of Setω
when checking that the expression M.id has type P _k_32 _A_34