8000 Match display forms in the right context by plt-amy · Pull Request #7480 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Match display forms in the right context #7480

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
Merged
merged 2 commits into from
Sep 10, 2024
Merged

Match display forms in the right context #7480

merged 2 commits into from
Sep 10, 2024

Conversation

plt-amy
Copy link
Member
@plt-amy plt-amy commented Sep 9, 2024 •
edited
Loading

Surprisingly, in

module _ (f : Nat → Foo) where
  module _ n where open Foo (f n) renaming (f to g) public
  _ = {! g 10  !}

the normal form of g 10 prints as Foo.f (f 10) rather than g 10. Display form matching is trying to compare (I've lined up the pattern and the actual eliminations)

name        : wip.test110.Foo.f
displayForms: [Display 1 [@1 @0] (wip.test110._._._.f @1 @0)]
arguments   :            [@0 10]

which fails, since 0 ≠ 1. The display form has correctly been generalised over n, as per #958. However, the pattern and the RHS exist in different contexts --- the RHS exists in a context with one variable less than the display form (which binds the pattern variable @0). So we really should be lifting the term to the context of the patterns before trying to do matching, and making sure that the matching doesn't depend on the pattern variables later.

@plt-amy plt-amy added type: bug Issues and pull requests about actual bugs ux: display Issues relating to how terms are printed for display labels Sep 9, 2024
@plt-amy plt-amy changed the title Match display forms in the right scope Match display forms in the right context Sep 9, 2024
andreasabel
andreasabel reviewed Sep 9, 2024
View reviewed changes
@andreasabel andreasabel added this to the 2.8.0 milestone Sep 10, 2024
andreasabel
andreasabel approved these changes Sep 10, 2024
View reviewed changes
Copy link
Member
@andreasabel andreasabel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@plt-amy plt-amy merged commit 9e0d5a5 into master Sep 10, 2024
28 checks passed
@plt-amy plt-amy deleted the aliao/lift-display-form branch September 10, 2024 10:13
@andreasabel andreasabel modified the milestones: 2.8.0, 2.7.0.1 Sep 11, 2024
andreasabel pushed a commit that referenced this pull request Sep 11, 2024
@plt-amy @andreasabel
Match display forms in the right context (#7480)
6d4fc7d
andreasabel pushed a commit that referenced this pull request Sep 11, 2024
@plt-amy @andreasabel
Match display forms in the right context (#7480)
794f5c9
fredins pushed a commit to fredins/agda that referenced this pull request Nov 24, 2024
@plt-amy @fredins
Match display forms in the right context (agda#7480)
0a0f60e
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@andreasabel andreasabel andreasabel approved these changes

@UlfNorell UlfNorell Awaiting requested review from UlfNorell

Assignees
No one assigned
Labels
type: bug Issues and pull requests about actual bugs ux: display Issues relating to how terms are printed for display
Projects
None yet
Milestone
2.7.0.1
Development

Successfully merging this pull request may close these issues.
2 participants
@plt-amy @andreasabel
0