Agda-2.3.2.2: test/fail/IrrelevantMatchRefl.err
IrrelevantMatchRefl.agda:59,11-15 D != D → D of type Set when checking that the expression refl has type K∞ ≡ abs (λ y → K∞)
IrrelevantMatchRefl.agda:59,11-15 D != D → D of type Set when checking that the expression refl has type K∞ ≡ abs (λ y → K∞)