kernel failed to type check declaration given by rfl

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.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

def int.pow_nat : ℤ → ℕ → ℤ
| (int.of_nat b) e := int.of_nat (b ^ e)
| (int.neg_succ_of_nat b) 0 := 1
| (int.neg_succ_of_nat b) (k+1) := (int.neg_succ_of_nat b) * int.pow_nat (int.neg_succ_of_nat b) k

instance int_has_pow_nat : has_pow int nat := ⟨int.pow_nat⟩

def int.pow (b : ℤ) : ℤ → ℤ
| (int.of_nat n) := b ^ n
| (int.neg_succ_of_nat n) := 0

instance : has_pow int int := ⟨int.pow⟩

@[simp]
def int.pow_of_nat (b : ℕ) (e : ℕ) : int.pow b e = int.of_nat (b ^ e) := rfl
-- 15:5: kernel failed to type check declaration 'int.pow_of_nat' this is usually due to a buggy tactic or a bug in the builtin elaborator
-- elaborated type:
--   ∀ (b e : ℕ), int.pow ↑b ↑e = int.of_nat (b ^ e)
-- elaborated value:
--   λ (b e : ℕ), rfl
-- nested exception message:
-- type mismatch at definition 'int.pow_of_nat', has type
--   ∀ (b e : ℕ), int.pow ↑b ↑e = int.pow ↑b ↑e
-- but is expected to have type
--   ∀ (b e : ℕ), int.pow ↑b ↑e = int.of_nat (b ^ e)

Expected behavior: either it passes, or I get type mismatch

Actual behavior: I get an error message complaining about a possible bug

Reproduces how often: [What percentage of the time does it reproduce?] 100%

Versions

$ lean --version
Lean (version 3.4.2, commit cbd2b6686ddb, Release)
$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 16.04.6 LTS
Release:        16.04
Codename:       xenial
$ uname -a
Linux jgross-Leopard-WS 4.4.0-161-generic #189-Ubuntu SMP Tue Aug 27 08:10:16 UTC 2019 x86_64 x86_64 x86_64 GNU/Linux

Run the self-contained Lean reproduction with Lean 3.4.2 and inspect the kernel type-checking or builtin elaborator path involved in int.pow_of_nat. Done means the declaration either passes or reports a normal type mismatch instead of claiming a kernel or elaborator bug; add a regression test for the reproduced case.