Problem with DISPLAY pragma for ⊥ in Data.Empty

[jamesmckinna]

Agda issue#7533 and its 'resolution'/explanation via Agda issue#2004 suggests that perhaps we should rethink our approach to how to deal lexically with the ⊥ token (for output as well as input)? Or else (at least!) document that Data.Irrelevant should be approached with caution...

Sadly, syntax declarations are subject to the same, or similar, effects, so attempting to write

syntax Irrelevant Empty = ⊥

is both ill-formed (the 'hole' Empty is never used), and useless (Empty is not correctly interpreted as a already-defined term).

Perhaps a solution is simply to remove the DISPLAY pragma altogether?
UPDATED: NB. this is the only use of the pragma in stdlib!

[MatthewDaggitt]

Hmm, this is very irritating. It's a big usability loss to remove the DISPLAY pragma... I really don't want Irrelevant Empty popping up in people's buffers...

Introduced by @gallais in 367e3d6. Can't exactly revert this either, as it'll break a lot of code.

@gallais any ideas?

Could we use the new abstract feature somehow to prevent reduction?

[gallais]

Could we use the new abstract feature somehow to prevent reduction?

This is what I was going to suggest we should experiment with.

However the following does not typecheck and so it does seem that Agda's emptyness check
refuses to go under abstract types which would make it a dramatically breaking change.

data Empty : Set where

abstract

  ⊥ : Set
  ⊥ = Empty


⊥-elim : ⊥ → ∀ {a} {A : Set a} → A
⊥-elim ()

I've commented on an upstream issue bringing up a similar issue for positivity annotations:
agda/agda#6970 (comment)

[jamesmckinna]

Andreas has reopened my originating issue, so there may be upstream progress at some point agda/agda#7536 ... in the meanwhile, display pragma is a new label on the main Agda issue tracker...

Separately, he hinted that perhaps REWRITE could be used here, but I'm not clear whether or not any such attempt would be subject to the same interpretation of Empty as a (pattern) variable...

[jamesmckinna]

As for pragmatics of the problem, I only encountered it when trying to have Data.Empty and Data.Irrelevant in scope at the same time... a (perhaps) rare scenario? (And leaning in to my customary observation about explicit use of ⊥ and ⊥-elim when these are largely avoidable via other mechanisms...)

[andreasabel]

Prompted by this issue, Agda 2.8 might have more usable DISPLAY pragmas:

• DISPLAY: match on defined names agda#7543

This should fix your problem (albeit not right now).

[MatthewDaggitt]

That's great, thank you! So I guess we mark this issue as blocked upstream and wait for the fix.