Error: motive is not type correct

Stream: new members

[Apurva Nakade]

I was playing around with mathlib and got a new error for the first time. I don't even understand what the words mean lol.

Here's a mwe:

import ring_theory.localization

example (b : ℤ) (b' : ℕ)
  (hb : 2 ^ b' = b) :
  submonoid.log ⟨b, b', hb⟩ = b' :=
begin
  have := @submonoid.log_pow_int_eq_self 2 (lt_add_one 1) b',
  unfold submonoid.pow at this,
  rw ← hb,
  -- rewrite tactic failed, motive is not type correct
  -- λ (_a : ℤ), submonoid.log ⟨b, _⟩ = b' = (submonoid.log ⟨_a, _⟩ = b')
end

What does this error mean? What's a motive?

Thanks,