MetaCannotDependOn.agda:13,22-24 Cannot instantiate the metavariable _9 to solution Vec n Nat 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 xs has type Vec n Nat