Skip to content
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

fix: make sure monad lift coercion elaborator has no side effects #6024

Merged
merged 3 commits into from
Nov 13, 2024
Merged

fix: make sure monad lift coercion elaborator has no side effects #6024

merged 3 commits into from
Nov 13, 2024

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Nov 10, 2024 •
edited
Loading

This PR fixes a bug where the monad lift coercion elaborator would partially unify expressions even if they were not monads. This could be taken advantage of to propagate information that could help elaboration make progress, for example the first change worked because the monad lift coercion elaborator was unifying @Eq _ _ with @Eq (Nat × Nat) p:

example (p : Nat × Nat) : p = p := by
  change _ = ⟨_, _⟩ -- used to work (yielding `p = (p.fst, p.snd)`), now it doesn't
  change ⟨_, _⟩ = _ -- never worked

As such, this is a breaking change; you may need to adjust expressions to include additional implicit arguments.

@kmill kmill added the changelog-language Language features, tactics, and metaprograms label Nov 10, 2024
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 10, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 10, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6024
fb40def
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 10, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6024
ca56307
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 10, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 11, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6024
bc98496
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 11, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6024
2361f93
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 11, 2024
@kim-em
fix first round of failures for leanprover/lean4#6024
783e37d
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 11, 2024
@kim-em
fix most of 2nd round of failures for leanprover/lean4#6024
afadc60
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Nov 11, 2024
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 12, 2024
@kim-em
fix first round of failures for leanprover/lean4#6024
e9b4260
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 12, 2024
@kim-em
fix most of 2nd round of failures for leanprover/lean4#6024
b7979a5
@kim-em kim-em mentioned this pull request Nov 12, 2024
Closed
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 12, 2024
@kim-em @kmill
chore: backports of adaptations for leanprover/lean4#6024 (#18896)
5ffcbfd 
leanprover/lean4#6024 fixes a serious elaboration bug which, perversely, was quite helpful.

Kyle is investigating replacing the bug with something intentional, but we definitively need to fix the bug in the meantime.

This is the backport of changes from lean-pr-testing-6024 which do not have conflicts with `master`. There are a few more changes that we'll need to handle separately later.

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@kmill kmill added this pull request to the merge queue Nov 12, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Nov 13, 2024
kmill added 2 commits November 12, 2024 19:54
@kmill
fix: make sure monad lift coercion elaborator has no side effects
329c160 
This PR fixes a bug where the monad lift coercion elaborator would partially unify expressions even if they were not monads. Breaking change: examples such as `change _ = .some true` no longer work. They accidentally worked because this elaborator left an accidental type hint on `Eq`.
@kmill
fix tests
53e20fe
@kmill kmill force-pushed the fix_coercemonadlift branch from 2b0f9bb to 53e20fe Compare November 13, 2024 04:02
@kmill kmill enabled auto-merge November 13, 2024 04:02
@kmill kmill added this pull request to the merge queue Nov 13, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1315266dd3faeaf28d1263668cb88f2f3f5e530c --onto 5e01e628b2ef90d8881a5ba10340032eeeabc5d4. (2024-11-13 04:21:42)

@kmill kmill removed this pull request from the merge queue due to a manual request Nov 13, 2024
@kmill kmill added this pull request to the merge queue Nov 13, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Nov 13, 2024
@kmill kmill requested a review from kim-em as a code owner November 13, 2024 06:40
@kmill kmill enabled auto-merge November 13, 2024 06:40
@kmill kmill added this pull request to the merge queue Nov 13, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to no response for status checks Nov 13, 2024
@kmill kmill added this pull request to the merge queue Nov 13, 2024
@kmill kmill removed this pull request from the merge queue due to a manual request Nov 13, 2024
@kmill kmill added this pull request to the merge queue Nov 13, 2024
Merged via the queue into leanprover:master with commit 28cf146 Nov 13, 2024
14 checks passed
@kim-em kim-em mentioned this pull request Nov 17, 2024
Closed
TobiasLeichtfried pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 21, 2024
@kim-em @kmill @TobiasLeichtfried
chore: backports of adaptations for leanprover/lean4#6024 (#18896)
7aa6a93 
leanprover/lean4#6024 fixes a serious elaboration bug which, perversely, was quite helpful.

Kyle is investigating replacing the bug with something intentional, but we definitively need to fix the bug in the meantime.

This is the backport of changes from lean-pr-testing-6024 which do not have conflicts with `master`. There are a few more changes that we'll need to handle separately later.

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@kmill kmill mentioned this pull request Dec 19, 2024
Closed
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@kmill @leanprover-community-bot