Issue865Big.agda:9,7-11 Cannot eliminate reflexive equation A = A of type Set because K has been disabled. when checking that the pattern refl has type A ≡ A