8000 `DISPLAY` pragmas should treat any defined name as matchable · Issue #7533 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

DISPLAY pragmas should treat any defined name as matchable #7533

8000
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
jamesmckinna opened this issue Oct 4, 2024 · 5 comments · Fixed by #7536 or #7543
Closed

DISPLAY pragmas should treat any defined name as matchable #7533

jamesmckinna opened this issue Oct 4, 2024 · 5 comments · Fixed by #7536 or #7543
Assignees
@andreasabel
Labels
display pragma Issues with the DISPLAY pragma ux: warnings Issues relating to the reporting of warnings
Milestone
2.8.0

Comments

@jamesmckinna
Copy link
Contributor

Agda version v2.7.0 (also v2.6.4.3, it seems)
stdlib version: master branch

Interactive attempt to check the following MWE causes a weird error, which I don't even know how to localise as to cause (failure in the variable generalisation mechanism? in the DISPLAY pragma?):

module IrrelevantBug where

open import Level
open import Data.Empty using (⊥)
open import Data.Irrelevant
open import Relation.Nullary.Recomputable

private
  variable
    a : Level
    A : Set a

recompute-irrelevant : Recomputable (Irrelevant A)
recompute-irrelevant p = {!p!}

Emacs interaction, instead of printing ?0 : Irrelevant A prints ?0 : ⊥?

NB

  • if quantification is explicit, rather than generalisation via the above private variables, then interaction is as expected.
  • similarly, if the import of Data.Empty is excluded, and with it the {-# DISPLAY Irrelevant Empty = ⊥ #-} pragma, then again the example is OK.

Any ideas how to avoid this? Data.Empty has been stable in the stdlib for a while now, so it seems to be only the interaction with the explicit import of Data.Irrelevant/Relation.Nullary.Recomputable (or: irrelevance annotaions?) causing the bug?
@szumixie
Copy link
Member
szumixie commented Oct 4, 2024 •
edited
Loading

if quantification is explicit, rather than generalisation via the above private variables, then interaction is as expected.

I can reproduce the problem without generalized variables.

The DISPLAY pragma only matches on data constructors in the left hand side arguments, not type constructors (see #2004).

So in the pragma {-# DISPLAY Irrelevant Empty = ⊥ #-}, Empty is a new pattern variable, and Irrelevant applied to any argument gets rewritten to ⊥.

Minimized example:

data Empty : Set where

postulate
  F : Set → Set
  X : Set
  A : Set

{-# DISPLAY F Empty = X #-}

_ : F A
_ = {!!} -- ?0 : X

@jamesmckinna
Copy link
Contributor Author
jamesmckinna commented Oct 4, 2024 •
edited
Loading

Oh!? Wow... thanks for the pointer back to #2004 .

Accordingly, I think I'll close this issue now, and re-raise an issue for stdlib as to how to deal with our current (clearly broken!) approach to DISPLAYing ⊥... sigh.

@jamesmckinna jamesmckinna mentioned this issue Oct 4, 2024
Open
@andreasabel andreasabel added display pragma Issues with the DISPLAY pragma status: duplicate Duplicate issue (not in changelog) labels Oct 5, 2024
@andreasabel
Copy link
Member

This is indeed a duplicate of

DISPLAY pragmas are still a prototypical feature and have not matured much since their introduction.
Maybe some REWRITE technology could be transferred to make DISPLAY better behaved.

@andreasabel andreasabel closed this as not planned Won't fix, can't repro, duplicate, stale Oct 5, 2024
@andreasabel
Copy link
Member
andreasabel commented Oct 5, 2024 •
edited
Loading

So in the pragma {-# DISPLAY Irrelevant Empty = ⊥ #-}, Empty is a new pattern variable, and Irrelevant applied to any argument gets rewritten to ⊥.

The least that Agda should do here is to warn about unused pattern variables, i.e., variables bound on the lhs that are not used on the rhs.

Rededicating this issue...

andreasabel added a commit that referenced this issue Oct 6, 2024
@andreasabel
Re #7533: warn when DISPLAY form binds variables unused on the rhs
4f617db
andreasabel referenced this issue Oct 6, 2024
@gallais
[ erase ] as a replacement to TrustMe. (#3300)
b290d0b 
We found out that we could use `erase` defined in terms of `trustMe` to prove UIP
even with the `--without-K` option turned on.

Turning things around and defining a stuck `erase` from which we can derive `trustMe`
should be safer.
@andreasabel andreasabel linked a pull request Oct 6, 2024 that will close this issue
Re #7533: warn when DISPLAY form binds variables unused on the rhs #7536
Merged
@andreasabel
Copy link
Member
andreasabel commented Oct 6, 2024 •
edited
Loading

We seem to have an invalid DISPLAY pragma in our code base ourselves: b290d0b#r147631053

agda/src/data/lib/prim/Agda/Builtin/TrustMe.agda

Line 15 in 1e9725e

{-# DISPLAY primEraseEquality unsafePrimTrustMe = primTrustMe #-}

And the documentation sounds misleading:

agda/doc/user-manual/language/pragmas.lagda.rst

Lines 98 to 100 in 1e9725e

- Left-hand sides of the display form are restricted to variables, constructors, defined
functions or types, and literals. In particular, lambdas are not
allowed in left-hand sides.

@andreasabel andreasabel reopened this Oct 6, 2024
@andreasabel andreasabel changed the title Bug in ... something (DISPLAY pragma)? Warn about defunct DISPLAY pragmas Oct 6, 2024
@andreasabel andreasabel self-assigned this Oct 6, 2024
@andreasabel andreasabel added this to the 2.8.0 milestone Oct 6, 2024
@andreasabel andreasabel added ux: warnings Issues relating to the reporting of warnings and removed status: duplicate Duplicate issue (not in changelog) labels Oct 6, 2024
@andreasabel andreasabel changed the title Warn about defunct DISPLAY pragmas DISPLAY pragmas should treat any defined name as matchable Oct 8, 2024
andreasabel added a commit that referenced this issue Oct 8, 2024
@andreasabel
Re #2004: DISPLAY pragmas can now match on defined names
9e58951 
Closes #7533.
@andreasabel andreasabel mentioned this issue Oct 8, 2024
Merged
andreasabel added a commit that referenced this issue Oct 9, 2024
@andreasabel
Re #2004: DISPLAY pragmas can now match on defined names
799d73b 
Closes #7533.

Squashed into this commit:

- Re #2004: IsBool DisplayLHS instead of Boolean

- Re #2004: get rid of ApplicativeDo
andreasabel added a commit that referenced this issue Oct 11, 2024
@andreasabel
Re #7533: warn when DISPLAY form binds variables unused on the rhs
00e3100
andreasabel added a commit that referenced this issue Oct 11, 2024
@andreasabel
Re #7533: warn when DISPLAY form binds variables unused on the rhs
d0d880f
fredins pushed a commit to fredins/agda that referenced this issue Nov 24, 2024
@andreasabel @fredins
Re agda#2004: DISPLAY pragmas can now match on defined names
6e19b4f 
Closes agda#7533.

Squashed into this commit:

- Re agda#2004: IsBool DisplayLHS instead of Boolean

- Re agda#2004: get rid of ApplicativeDo
fredins pushed a commit to fredins/agda that referenced this issue Nov 24, 2024
@andreasabel @fredins
Re agda#7533: warn when DISPLAY form binds variables unused on the rhs
18b2117
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andreasabel andreasabel

Labels
display pragma Issues with the DISPLAY pragma ux: warnings Issues relating to the reporting of warnings
Projects
None yet
Milestone
2.8.0
3 participants
@andreasabel @jamesmckinna @szumixie
0