simp produces a term that doesn't typecheck when used with WellFounded.fix

[eric-wieser]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

simp sometimes generates a proof that doesn't typecheck

Steps to Reproduce

prelude -- optional
import Init.WF
import Init.WFTactics
import Init.Data.Nat.Basic
namespace Nat

protected def modCore (y : Nat) : Nat → Nat → Nat
  | Nat.zero, x => x
  | Nat.succ fuel, x => if 0 < y ∧ y ≤ x then Nat.modCore y fuel (x - y) else x

protected def mod' (x y : @& Nat) : Nat :=
Nat.modCore y x x

@[simp] theorem zero_mod' (b : Nat) : Nat.mod' 0 b = 0 := rfl

end Nat

namespace Nat

private def gcdF' (x : Nat) : (∀ x₁, x₁ < x → Nat → Nat) → Nat → Nat :=
  match x with
  | 0      => fun _ y => y
  | succ x => fun f y => f (Nat.mod' y (succ x)) sorry (succ x)

noncomputable def gcd' (a b : Nat) : Nat :=
  WellFounded.fix (measure id).wf gcdF' a b

@[simp] theorem gcd'_zero_left (y : Nat) : gcd' 0 y = y :=
  rfl

theorem gcd'_succ (x y : Nat) : gcd' (succ x) y = gcd' (Nat.mod' y (succ x)) (succ x) :=
  rfl   -- replace with `id rfl` and everything is ok

--              VVVVVVVVVVVVVVV error here
@[simp] theorem gcd'_zero_right (n : Nat) : gcd' n 0 = n := by
  cases n <;> simp [gcd'_succ]

end Nat

Expected behavior: simp should either succeed, or give a tactic failure

Actual behavior: simp succeeds, but the kernel rejects the proof with

application type mismatch
  @Eq.ndrec Nat (succ n✝) (fun n => gcd' n 0 = n) (of_eq_true (eq_self (succ n✝)))
argument has type
  succ n✝ = succ n✝
but function has type
  (fun n => gcd' n 0 = n) (succ n✝) → ∀ {b : Nat}, succ n✝ = b → (fun n => gcd' n 0 = n) b

Reproduces how often: 100%

Versions

$ ~/.elan/bin/lean --version
Lean (version 4.0.0-nightly-2023-01-08, commit 74b3d101e967, Release)

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.