fix: avoid Syntax trees leaks into .olean files

closes #918

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
       }

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

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