A question on zulip led me to realize that you can always produce irrelevant projections from a record. For example:
record ⊤ : Set where
record TSquash (A : Set) : Set where
field
.extract : ⊤ -> A
.tflat : ⊤ -> A
tflat x = extract x
open TSquash
.flat : ∀{A} → .A -> A
flat a = tflat (λ where .extract _ → a) _
That passes the latest Agda without --irrelevant-projections.
I think the issue is that tflat is accepted as long as it is eta expanded (but properly rejected if reduced, which was the original zulip question). I don't know what that becomes internally, but it seems strange to accept it unless --irrelevant-projections is on.
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