Agda-2.3.2.2: test/fail/StronglyRigidOccurrence.err
StronglyRigidOccurrence.agda:13,8-12 Refuse to construct infinite term by instantiating _9 to suc _9 when checking that the expression refl has type _9 ≡ suc _9
StronglyRigidOccurrence.agda:13,8-12 Refuse to construct infinite term by instantiating _9 to suc _9 when checking that the expression refl has type _9 ≡ suc _9