<p>I think I just came up with one. The following code block is written in a syntax similar to Agda.</p>
<pre><code>test : (a : _) (B : Set) (b : B) -&gt; a ≡ b
test a B b = refl
</code></pre>
<p>Assuming <code>≡</code> to be the homogeneous equality type and <code>refl</code> to be its constructor, the solution to the underscore is <code>B</code>, which is not defined there yet. Type checking the above code (with <code>open import Agda.Builtin.Equality</code>) will result in the following error message:</p>
<pre><code>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
</code></pre>

CC BY-SA 4.0
2021-06-24T05:28:46.180Z
2021-06-24T05:28:46.180Z
ice1000
<p>This is a question on metavariable (aka holes) resolution in (dependent) type theories.</p>
<p>In many referential implementations (such as Andras Kovacs' <a href="https://github.com/AndrasKovacs/elaboration-zoo/blob/d38b695d5177352501463fab2ac6d0929ba4472b/03-holes/Main.hs#L440-L442" rel="nofollow noreferrer">elaboration-zoo</a>), 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?</p>

<dependent-type><type-inference>
Counterexample request: ill-scoped metavariable solution
ice1000
# Counterexample request: ill-scoped metavariable solution

(Asked by: username_0 on 2021-06-24)

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

In many referential implementations (such as Andras Kovacs' [elaboration-zoo](https://github.com/AndrasKovacs/elaboration-zoo/blob/d38b695d5177352501463fab2ac6d0929ba4472b/03-holes/Main.hs#L440-L442)), 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?

**Tags:** dependent-type, type-inference

---

## 1 answers

### Answer by username_0 on 2021-06-24. Score: 3 | Accepted answer

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


---

