Issue875.agda:8,7-8
Cannot instantiate the metavariable _5 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 f has type P x
