Issue2640.agda:20,20-23
Cannot instantiate the metavariable _21 to solution n since it
contains the variable n which is not in scope of the metavariable
or irrelevant in the metavariable but relevant in the solution
when checking that the expression c _ has type D n
