1
MetaCannotDependOn.agda:13,22-24
2
Cannot instantiate the metavariable _9 to solution Vec n Nat since
3
it contains the variable n which is not in scope of the
4
metavariable or irrelevant in the metavariable but relevant in the
6
when checking that the expression xs has type Vec n Nat