<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

```


---

