2
$\begingroup$

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?

$\endgroup$
3
$\begingroup$

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
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.