From e9c112007b5ece5bdbfec41923ba9aaa52a9f43d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Jan 2022 09:36:06 -0800
Subject: [PATCH] fix: avoid Syntax trees leaks into .olean files

closes #918
---
 src/Lean/Elab/PreDefinition/Basic.lean           | 10 +++++++---
 src/Lean/Elab/PreDefinition/Structural/Main.lean |  8 +++++---
 src/Lean/Elab/PreDefinition/WF/Main.lean         |  1 +
 3 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index e802b54920..d62ca38b42 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -129,16 +129,20 @@ def addNonRec (preDef : PreDefinition) : TermElabM Unit := do
 /--
   Eliminate recursive application annotations containing syntax. These annotations are used by the well-founded recursion module
   to produce better error messages. -/
-def eraseRecAppSyntax (e : Expr) : CoreM Expr :=
+def eraseRecAppSyntaxExpr (e : Expr) : CoreM Expr :=
   Core.transform e (post := fun e => TransformStep.done <| if (getRecAppSyntax? e).isSome then e.mdataExpr! else e)
 
-def addAndCompileUnsafe (preDefs : Array PreDefinition) (safety := DefinitionSafety.unsafe) : TermElabM Unit :=
+def eraseRecAppSyntax (preDef : PreDefinition) : CoreM PreDefinition :=
+  return { preDef with value := (← eraseRecAppSyntaxExpr preDef.value) }
+
+def addAndCompileUnsafe (preDefs : Array PreDefinition) (safety := DefinitionSafety.unsafe) : TermElabM Unit := do
+  let preDefs ← preDefs.mapM fun d => eraseRecAppSyntax d
   withRef preDefs[0].ref do
     let decl := Declaration.mutualDefnDecl <| ← preDefs.toList.mapM fun preDef => return {
         name        := preDef.declName
         levelParams := preDef.levelParams
         type        := preDef.type
-        value       := (← eraseRecAppSyntax preDef.value)
+        value       := preDef.value
         safety      := safety
         hints       := ReducibilityHints.opaque
       }
diff --git a/src/Lean/Elab/PreDefinition/Structural/Main.lean b/src/Lean/Elab/PreDefinition/Structural/Main.lean
index 02c64db037..1ef5fdd13a 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Main.lean
@@ -81,11 +81,13 @@ def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
     throwError "structural recursion does not handle mutually recursive functions"
   else do
     let ((recArgPos, preDefNonRec), state) ← run <| elimRecursion preDefs[0]
+    let preDefNonRec ← eraseRecAppSyntax preDefNonRec
+    let preDef ← eraseRecAppSyntax preDefs[0]
     state.addMatchers.forM liftM
     mapError (addNonRec preDefNonRec) (fun msg => m!"structural recursion failed, produced type incorrect term{indentD msg}")
-    addAndCompilePartialRec preDefs
-    addSmartUnfoldingDef preDefs[0] recArgPos
-    registerEqnsInfo preDefs[0] recArgPos
+    addAndCompilePartialRec #[preDef]
+    addSmartUnfoldingDef preDef recArgPos
+    registerEqnsInfo preDef recArgPos
 
 builtin_initialize
   registerTraceClass `Elab.definition.structural
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index a3b553d01b..5d03771565 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Main.lean
@@ -56,6 +56,7 @@ def wfRecursion (preDefs : Array PreDefinition) (wfStx? : Option Syntax) (decrTa
   let preDefNonRec ← withoutModifyingEnv do
     addAsAxiom unaryPreDef
     mkFix unaryPreDef wfRel decrTactic?
+  let preDefNonRec ← eraseRecAppSyntax preDefNonRec
   trace[Elab.definition.wf] ">> {preDefNonRec.declName}"
   addNonRec preDefNonRec
   addNonRecPreDefs preDefs preDefNonRec