From 8aa003bdfca4cdb67ab0ac89ff8d85c545cf0525 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Thu, 12 Jun 2025 14:52:02 -0700 Subject: [PATCH] fix: move structProjCases pass before extendJoinPointContext (#8752) This PR fixes an issue where the `extendJoinPointContext` pass can lift join points containing projections to the top level, as siblings of `cases` constructs matching on other projections of the same base value. This prevents the `structProjCases` pass from projecting both at once, extending the lifetime of the parent value and breaking linearity at runtime. This would theoretically be possible to fix in `structProjCases`, but it would require some better infrastructure for handling join points. It's also likely that the IR passes dealing with reference counting would have similar bugs that pessimize the code. For this reason, the simplest thing is to just perform the `structProjCases` pass earlier, which prevents `extendJoinPointContext` from lifting these join points. --- src/Lean/Compiler/LCNF/Passes.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean index 57b6e5ef0f..1a4fdd722e 100644 --- a/src/Lean/Compiler/LCNF/Passes.lean +++ b/src/Lean/Compiler/LCNF/Passes.lean @@ -68,6 +68,7 @@ def builtinPassManager : PassManager := { toMono, simp (occurrence := 3) (phase := .mono), reduceJpArity (phase := .mono), + structProjCases, extendJoinPointContext (phase := .mono) (occurrence := 0), floatLetIn (phase := .mono) (occurrence := 1), reduceArity, @@ -78,7 +79,6 @@ def builtinPassManager : PassManager := { lambdaLifting, extendJoinPointContext (phase := .mono) (occurrence := 1), simp (occurrence := 5) (phase := .mono), - structProjCases, cse (occurrence := 2) (phase := .mono), saveMono, -- End of mono phase extractClosed