Agda-2.3.2.2: test/fail/LevelUnification.err
LevelUnification.agda:13,20-24 a != b of type Level when checking that the pattern refl has type x ≡ y
LevelUnification.agda:13,20-24 a != b of type Level when checking that the pattern refl has type x ≡ y