packages feed

Agda-2.3.2.2: test/fail/UnifyWithIrrelevantArgument.err

UnifyWithIrrelevantArgument.agda:11,12-16
Cannot instantiate the metavariable _7 to solution x since it
contains the variable x which is not in scope of the metavariable
or irrelevant in the metavariable but relevant in the solution
when checking that the expression refl has type _7 A _ ≡ x