# Counterexample request: ill-scoped metavariable solution

This is a question on metavariable (aka holes) resolution in (dependent) type theories.

In many referential implementations (such as Andras Kovacs' elaboration-zoo), there is one step called 'scope check', which checks if the solution of a metavariable is well-scoped. It is unclear to me how a solution can be ill-scoped. I wonder if there is a counterexample showing an ill-scoped solution to a metavariable?

I think I just came up with one. The following code block is written in a syntax similar to Agda.

test : (a : _) (B : Set) (b : B) -> a ≡ b
test a B b = refl


Assuming ≡ to be the homogeneous equality type and refl to be its constructor, the solution to the underscore is B, which is not defined there yet. Type checking the above code (with open import Agda.Builtin.Equality) will result in the following error message:

Cannot instantiate the metavariable _1 to solution B
since it contains the variable B
which is not in scope of the metavariable
when checking that the expression b has type _1