[Agda] "Not in Scope" definitional equalities

[Jesper Cockx]

Hi Sergey,

A part of the context of the form `X = X₁ : Set (ℓ ⊔ ℓ′)  (not in scope)`
can mean two things:

1. either there is a variable named `X` in scope, but it is shadowed by
another variable `X` so Agda decided to rename it to `X₁`
2. or the variable `X` is an implicit argument and Agda decided to
pro-actively rename it to `X₁` to avoid a name conflict with another
(implicit or explicit) variable

In case 1., you need to find out which other variable is also named `X` and
rename one of them. In case 2., you need to bind the implicit argument
explicitly, e.g. by writing `{X = X}` in the left-hand side of the clause.

-- Jesper

ps: To the Agda devs: maybe in the first case Agda should display
`(shadowed)` instead of `(not in scope)` so it is easier to distinguish
between the two cases?


On Mon, Mar 23, 2020 at 2:26 AM Sergey Goncharov <sergey.goncharov at fau.de>
wrote:

> Hi All,
>
> I have the following problem: in course of a proof, as a part of the
> running context, I have:
>
> X = X₁ : Set (ℓ ⊔ ℓ′)  (not in scope)
>
> and when I try to resolve a hole in this context I get
>
> X !=< X₁ of type Set (ℓ ⊔ ℓ′)
> when checking that the expression ... has type ...
>
> It is hard to provide more details, because the complete example is
> large, and as usual everything depends on everything else. But maybe
> someone could help me with a general understanding how these "not in
> scope" definitional equalities can be avoided, and why they are not
> effective anyway?
>
> Thanks,
> Sergey
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200323/5d478a4e/attachment.html>