Agda-2.3.2.2: test/fail/LevelLiterals.err
LevelLiterals.agda:13,19-30 Set (suc zero ⊔ .ℓ) != Set when checking that the expression (A → ⊥) → ⊥ has type Set
LevelLiterals.agda:13,19-30 Set (suc zero ⊔ .ℓ) != Set when checking that the expression (A → ⊥) → ⊥ has type Set