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