leanprover
fix: segfault in old compiler due to noConfusion assumptions
This fixes #2901, a bug in the old compiler which causes a segfault. The issue is that when visiting noConfusion applications, it assumes that each constructor case has nfields arguments, e.g. head1 = head2 -> tail1 = tail2 -> P has two arguments because List.cons has 2 fields, but in fact propositional fields are skipped by the noConfusion type generator, so for example Subtype.noConfusionType is:
@[reducible] protected def Subtype.noConfusionType.{u_1, u} : {α : Sort u} →
{p : α → Prop} → Sort u_1 → Subtype p → Subtype p → Sort u_1 :=
fun {α} {p} P v1 v2 ↦
Subtype.casesOn v1 fun val property ↦ Subtype.casesOn v2 fun val_1 property ↦
(val = val_1 → P) → P
where val = val_1 → P only has the one argument even though Subtype.mk has two fields, presumably because it is useless to have an equality of propositions. Unfortunately there isn't any easy cache or getter to use here to get the number of non-propositional fields, so we just calculate it on the spot.
I took the liberty to make the PR title more explicit, it helps at least me when looking at notifications. I hope that doesn't step on anyone's toes.
- ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-11-17' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-11-17 14:17:44)
- 🟡 Mathlib branch lean-pr-testing-2903 build against this PR was cancelled. (2023-11-20 03:50:44) View Log
- ✅ Mathlib branch lean-pr-testing-2903 has successfully built against this PR. (2023-11-20 05:04:55) View Log
- 🟡 Mathlib branch lean-pr-testing-2903 build this PR didn't complete normally. (2024-05-10 01:41:41) View Log
will this go to 4.4 or nightly ?
@nrolland, when this is merged it will land in the nightly releases. It will then be rolled out as part of v4.5.0-rc1 (likely on Dec 21).
