unification bug?

Stream: lean4

[Michael Jam]

Hello! I have this bit of code:

theorem th : ∀ x : Nat, x * 2 = x + x := by
  intro x
  rw [Nat.mul_succ, Nat.mul_one]

def double1 (x : Nat) : {y : Nat // y = x + x} := ⟨x + x, rfl⟩
def double2 (x : Nat) : {y : Nat // y = x + x} := ⟨x * 2, th x⟩

class Double (α : Type u) where
  double [Add α] (x : α) : {y : α // y = x + x}
instance : Double Nat where double x := ⟨x + x, rfl⟩
instance : Double Nat where double x := ⟨x * 2, th x⟩

double1 and double2 are formally verified functions computing the double of some input nat x.
double2 is slightly different in that it uses multiplication, but it has the same specification, so it needs to provide a proof that what it does is good. So far so good.

Now I make a typeclass Double which represents a function double on a type alpha equipped with an addition.
Again that function formally specifies that its output should represent the double of its input.

when I write the first instance its OK, but for the second instance it fails to accept my proof although its exactly the same as in double2
Error message is

application type mismatch
  { val := x * 2, property := th x }
argument
  th x
has type
  x * 2 = x + x : Prop
but is expected to have type
  x * 2 = x + x : Prop

Is this a bug? (Lean (version 4.0.0-nightly-2021-05-10, commit 89373bd64fb5, Release)

[Mario Carneiro]

Not a bug. Your definition says that given any implementation of [Add A] it can construct a value y = x + x, which can only be done by using x + x directly. In particular it is not necessarily the "canonical" instance associated to A

[Mario Carneiro]

fixed:

class Double (α : Type u) [Add α] where
  double (x : α) : {y : α // y = x + x}
instance : Double Nat where double x := ⟨x + x, rfl⟩
instance : Double Nat where double x := ⟨x * 2, th x⟩

[Michael Jam]

ok thank you