fix: [implemented_by] at functions defined by well-founded recursion

src/Lean/Elab/DeclModifiers.lean

@@ -81,10 +81,14 @@ def Modifiers.isNonrec : Modifiers → Bool
   | { recKind := .nonrec, .. } => true
   | _                          => false
 
-/-- Store `attr` in `modifiers` -/
-def Modifiers.addAttribute (modifiers : Modifiers) (attr : Attribute) : Modifiers :=
+/-- Adds attribute `attr` in `modifiers` -/
+def Modifiers.addAttr (modifiers : Modifiers) (attr : Attribute) : Modifiers :=
   { modifiers with attrs := modifiers.attrs.push attr }
 
+/-- Filters attributes using `p` -/
+def Modifiers.filterAttrs (modifiers : Modifiers) (p : Attribute → Bool) : Modifiers :=
+  { modifiers with attrs := modifiers.attrs.filter p }
+
 instance : ToFormat Modifiers := ⟨fun m =>
   let components : List Format :=
     (match m.docString? with

src/Lean/Elab/Declaration.lean

@@ -184,7 +184,7 @@ def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
   elabInductiveViews #[v]
 
 def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-  let modifiers := modifiers.addAttribute { name := `class }
+  let modifiers := modifiers.addAttr { name := `class }
   let v ← classInductiveSyntaxToView modifiers stx
   elabInductiveViews #[v]
 

src/Lean/Elab/DefView.lean

@@ -135,8 +135,8 @@ open Meta
 def mkDefViewOfAbbrev (modifiers : Modifiers) (stx : Syntax) : DefView :=
   -- leading_parser "abbrev " >> declId >> optDeclSig >> declVal
   let (binders, type) := expandOptDeclSig stx[2]
-  let modifiers       := modifiers.addAttribute { name := `inline }
-  let modifiers       := modifiers.addAttribute { name := `reducible }
+  let modifiers       := modifiers.addAttr { name := `inline }
+  let modifiers       := modifiers.addAttr { name := `reducible }
   { ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.abbrev, modifiers,
     declId := stx[1], binders, type? := type, value := stx[3] }
 
@@ -159,7 +159,7 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
   let prio            ← liftMacroM <| expandOptNamedPrio stx[2]
   let attrStx         ← `(attr| instance $(quote prio):num)
   let (binders, type) := expandDeclSig stx[4]
-  let modifiers       := modifiers.addAttribute { kind := attrKind, name := `instance, stx := attrStx }
+  let modifiers       := modifiers.addAttr { kind := attrKind, name := `instance, stx := attrStx }
   let declId ← match stx[3].getOptional? with
     | some declId =>
       if ← isTracingEnabledFor `Elab.instance.mkInstanceName then

src/Lean/Elab/PreDefinition/Basic.lean

@@ -32,6 +32,9 @@ structure PreDefinition where
   termination : WF.TerminationHints
   deriving Inhabited
 
+def PreDefinition.filterAttrs (preDef : PreDefinition) (p : Attribute → Bool) : PreDefinition :=
+  { preDef with modifiers := preDef.modifiers.filterAttrs p }
+
 def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
   preDefs.mapM fun preDef => do
     pure { preDef with type := (← instantiateMVars preDef.type), value := (← instantiateMVars preDef.value) }

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -129,7 +129,15 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
         eraseRecAppSyntaxExpr value
       /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
       let value ← unfoldDeclsFrom envNew value
-      return { unaryPreDef with value }
+      let unaryPreDef := { unaryPreDef with value }
+      /-
+      We must remove `implemented_by` attributes from the auxiliary application because
+      this attribute is only relevant for code that is compiled. Moreover, the `[implemented_by <decl>]`
+      attribute would check whether the `unaryPreDef` type matches with `<decl>`'s type, and produce
+      and error. See issue #2899
+      -/
+      let unaryPreDef := unaryPreDef.filterAttrs fun attr => attr.name != `implemented_by
+      return unaryPreDef
   trace[Elab.definition.wf] ">> {preDefNonRec.declName} :=\n{preDefNonRec.value}"
   let preDefs ← preDefs.mapM fun d => eraseRecAppSyntax d
   -- Do not complain if the user sets @[semireducible], which usually is a noop,

src/Lean/Elab/Structure.lean

@@ -878,7 +878,7 @@ def structCtor           := leading_parser try (declModifiers >> ident >> " :: "
 def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   checkValidInductiveModifier modifiers
   let isClass   := stx[0].getKind == ``Parser.Command.classTk
-  let modifiers := if isClass then modifiers.addAttribute { name := `class } else modifiers
+  let modifiers := if isClass then modifiers.addAttr { name := `class } else modifiers
   let declId    := stx[1]
   let params    := stx[2].getArgs
   let exts      := stx[3]

tests/lean/run/2899.lean

@@ -0,0 +1,12 @@
+def myfunUnsafe (x : Array α) (i : Fin x.size) : Array α :=
+  sorry
+
+@[implemented_by myfunUnsafe]
+def myfun (x : Array α) (i : Fin x.size) : Array α :=
+  let next := 2*i.1 + 1
+  if h : next < x.size then
+      have : x.size - next < x.size - i.1 := sorry
+      myfun (x.swap i ⟨next,h⟩) ⟨next, (x.size_swap _ _).symm ▸ h⟩
+  else
+    x
+termination_by x.size - i.1