[Agda] "Not in Scope" definitional equalities

[Sergey Goncharov]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5384 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200323/32989437/attachment.p7s>