Consider the following example:
postulate A : Set
data This : A → Set where
this : (x : A) → This x
id-this : ∀ {@0 x} → This x → This x
id-this (this x) = this x
Agda complains:
Variable x is declared erased, so it cannot be used here
when checking that the expression x has type A
Without the @0 in the type signature of id-this, the definition is accepted. Intuitively, it feels wrong that marking something in the type signature (which is anyway erased) with @0 makes Agda consider a constructor argument to be erased.
This reminds me of a general issue with modalities in the LHS unifier that I remember discussing with @anuyts a long time ago, so perhaps he has an opinion on the matter.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4