kernel failed to type check declaration given by rfl

[JasonGross]

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

[digama0]

The theorem isn't actually true by refl, and the kernel is catching it. Here's a slightly simpler example:

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

def int.pow_of_nat (b : ℕ) (e : ℕ) : int.pow_nat b e = int.of_nat (b ^ e) :=
eq.refl _

The reason it's not true by refl is clear when you look at the equations generated:

#print prefix int.pow_nat

int.pow_nat.equations._eqn_1 : ∀ (b : ℕ), int.pow_nat (int.of_nat b) 0 = int.of_nat (b ^ 0)
int.pow_nat.equations._eqn_2 : ∀ (b n : ℕ), int.pow_nat (int.of_nat b) (nat.succ n) = int.of_nat (b ^ nat.succ n)
int.pow_nat.equations._eqn_3 : ∀ (b : ℕ), int.pow_nat -[1+ b] 0 = 1
int.pow_nat.equations._eqn_4 : ∀ (b k : ℕ), int.pow_nat -[1+ b] (k + 1) = -[1+ b] * int.pow_nat -[1+ b] k

As you can see, it generated a spurious case split in the first case, so the theorem you want is actually true by by cases e; refl instead of just rfl.

As for why the elaborator thinks this theorem is okay and leaves it to the kernel to catch (and produce this snarky message), I'm not entirely sure. It doesn't seem like a big problem to me because the error is caught regardless.

[JasonGross]

As for why the elaborator thinks this theorem is okay and leaves it to the kernel to catch (and produce this snarky message), I'm not entirely sure. It doesn't seem like a big problem to me because the error is caught regardless.

I do think either the error message should be changed, or the elaborator should be fixed; it seems poor form to have known tests that produce an error message that says "this is probably a bug" when it is known to not be a bug. (I do see why this theorem isn't proven by rfl, now; thanks for the explanation.) Perhaps this should get a "low priority" tag, or something?

[digama0]

It is a bug in the elaborator, so I will leave this issue open in case anyone wants to investigate further, but it is low priority bug as you say.

[robertylewis]

This error message does sometimes show up in places it shouldn't, for example if you forget to use the meta keyword where it's needed. It's almost surprising to see it used accurately here.

That said, the elaborator is changing in Lean 4 so it's likely the bug will disappear there. I wouldn't expect this to be fixed in Lean 3. It's rare (I've never seen it) and subtle (if you use theorem instead of def as expected, the error goes away).