Instance inference error

Stream: mathlib4

[Gareth Ma]

Error. Why? Bug? Should file?

import Mathlib.Tactic

theorem thm1 {ι : Type*} [SeminormedAddCommGroup ι] : 1 = 0 := sorry

/-
▶ 5:86-5:90: error:
typeclass instance problem is stuck, it is often due to metavariables
  SeminormedAddCommGroup ?m.131
-/
example {ι : Type*} [h : SeminormedAddCommGroup ι] (f : ℕ → ι) : f 1 = f 0 := by rw [thm1]

/- Works -/
example {ι : Type*} [h : SeminormedAddCommGroup ι] (f : ℕ → ι) : f 1 = f 0 := by rw [@thm1 _ h]

[Alex J. Best]

How is Lean supposed to know which iota you want to apply thm1 with by itself?

[Gareth Ma]

What do you mean, there's one iota right

[Alex J. Best]

Well you named them both iota but that doesn't mean Lean will automatically use iota for the argument iota when the theorem is applied (indeed that would be kind of annoying)

[Rémy Degenne]

Your code is the same as this, with different letters for the types:

import Mathlib.Tactic

theorem thm1 {A : Type*} [SeminormedAddCommGroup A] : 1 = 0 := sorry

/-
▶ 5:86-5:90: error:
typeclass instance problem is stuck, it is often due to metavariables
  SeminormedAddCommGroup ?m.131
-/
example {B : Type*} [h : SeminormedAddCommGroup B] (f : ℕ → B) : f 1 = f 0 := by rw [thm1]

/- Works -/
example {C : Type*} [h : SeminormedAddCommGroup C] (f : ℕ → C) : f 1 = f 0 := by rw [@thm1 _ h]

[Gareth Ma]

Ahhh hmm that makes sense, thanks!

[Gareth Ma]

In hindsight it sounds stupid haha

[Alex J. Best]

You are not the first person to ask this, dont worry!