[bug?] Mismatch between pattern-matching and manifest `record` field requiring `unsafe` irrelevant projection?

[jamesmckinna]

[bug?] Mismatch between pattern-matching and manifest `record` field requiring `unsafe` irrelevant projection?

[andreasabel]

Default irrelevance in Agda is "nested", that means, entering an irrelevant position only promotes irrelevant hypotheses in the current context to relevant ones, but does not allow you to use new irrelevant that enter the context.
E.g., this is rejected:

record Squash (A : Set) : Set where
  constructor squash
  field .squashed : A

postulate
  irrelevant : (A : Set) → .A → Set

foo : Set → Set
foo A = irrelevant (Squash A → A) (λ (squash x) → x)

Variable x is declared irrelevant, so it cannot be used here

You can get this with --irrelevant-projections, which in effect makes irrelevant "flat":

foo : Set → Set
foo A = irrelevant (Squash A → A) (λ s → squashed s)

Having said that, Agda does seem inconsequential in that

1. it internally converts top into failing-top through the record-pattern translation, but
2. rejects failing-top when written by the user.

Evidence for fact 1 is that the following snipped is accepted by Agda:

postulate
  A : Set
  a : A
  s : Squash A

T : Squash A → Set
T (squash _) = A

test : T s
test = a

Agda reduces T s to A by virtue of its internal representation of T that translated away the match against squash.

However, adding a check that failing-top is ok would maybe a bit cumbersome. We would have to check that the projection could be eliminated by doing a match on the lhs instead, not involving no-eta-equality records.

[jamesmckinna]

Ha! Interesting... many thanks for the feedback, and for the hint that in the presence of eta, failing-top should be OK... but sadly (for me in certain other settings), not for me/users themselves to define.

As for using --irrelevant-projections, that's not going to fly for stdlib modules I/we might otherwise STRONGLY wish to mark as --safe... oh well.