diff --git a/src/Lean/Compiler/LCNF/JoinPoints.lean b/src/Lean/Compiler/LCNF/JoinPoints.lean index 604b30602e..fed4d8db7d 100644 --- a/src/Lean/Compiler/LCNF/JoinPoints.lean +++ b/src/Lean/Compiler/LCNF/JoinPoints.lean @@ -534,7 +534,7 @@ def Decl.extendJoinPointContext (decl : Decl) : CompilerM Decl := do JoinPointContextExtender.extend decl def extendJoinPointContext : Pass := - .mkPerDeclaration `extendJoinPointContext Decl.extendJoinPointContext .base + .mkPerDeclaration `extendJoinPointContext Decl.extendJoinPointContext .mono builtin_initialize registerTraceClass `Compiler.extendJoinPointContext (inherited := true) diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean index 7347dfa3c4..92b964b4d9 100644 --- a/src/Lean/Compiler/LCNF/Passes.lean +++ b/src/Lean/Compiler/LCNF/Passes.lean @@ -55,6 +55,10 @@ def builtinPassManager : PassManager := { cse, saveBase, -- End of base phase toMono, + simp (occurrence := 3) (phase := .mono), + reduceJpArity (phase := .mono), + extendJoinPointContext, + simp (occurrence := 4) (phase := .mono), -- TODO: lambda lifting, reduce function arity saveMono -- End of mono phase ] diff --git a/src/Lean/Compiler/LCNF/ReduceJpArity.lean b/src/Lean/Compiler/LCNF/ReduceJpArity.lean index 1d1f06a4fa..5687267b66 100644 --- a/src/Lean/Compiler/LCNF/ReduceJpArity.lean +++ b/src/Lean/Compiler/LCNF/ReduceJpArity.lean @@ -70,8 +70,8 @@ def Decl.reduceJpArity (decl : Decl) : CompilerM Decl := do let value ← reduce decl.value |>.run {} return { decl with value } -def reduceJpArity : Pass := - .mkPerDeclaration `reduceJpArity Decl.reduceJpArity .base +def reduceJpArity (phase := Phase.base) : Pass := + .mkPerDeclaration `reduceJpArity Decl.reduceJpArity phase builtin_initialize registerTraceClass `Compiler.reduceJpArity (inherited := true) diff --git a/src/Lean/Compiler/LCNF/Simp.lean b/src/Lean/Compiler/LCNF/Simp.lean index 7361938464..038d372f4a 100644 --- a/src/Lean/Compiler/LCNF/Simp.lean +++ b/src/Lean/Compiler/LCNF/Simp.lean @@ -56,8 +56,8 @@ where else return decl -def simp (config : Config := {}) (occurrence : Nat := 0) : Pass := - .mkPerDeclaration `simp (Decl.simp · config) .base (occurrence := occurrence) +def simp (config : Config := {}) (occurrence : Nat := 0) (phase := Phase.base) : Pass := + .mkPerDeclaration `simp (Decl.simp · config) phase (occurrence := occurrence) builtin_initialize registerTraceClass `Compiler.simp (inherited := true) diff --git a/tests/lean/run/1686.lean b/tests/lean/run/1686.lean new file mode 100644 index 0000000000..57750fdecb --- /dev/null +++ b/tests/lean/run/1686.lean @@ -0,0 +1,7 @@ +import Lean +open Lean Meta + +def substIssue (hLocalDecl : LocalDecl) : MetaM Unit := do + let error {α} _ : MetaM α := throwError "{hLocalDecl.type}" + let some (_, lhs, rhs) ← matchEq? hLocalDecl.type | error () + error ()