Type error on dfinsupp add

Stream: general

[Eric Wieser]

How can I write this theorem statement in a way that will be accepted by the elaborator?

import data.dfinsupp
import data.finsupp.basic

variables {ι : Type*} {M : Type*}

/-- Interpret a homogenous `dfinsupp` as a `finsupp`. -/
def dfinsupp.to_finsupp [decidable_eq ι] [has_zero M] [Π m : M, decidable (m ≠ 0)]
  (f : Π₀ i : ι, M) : ι →₀ M :=
⟨f.support, f, λ i, by simp only [dfinsupp.mem_support_iff]⟩

/-- addition works fine -/
def my_add [add_zero_class M] (f g : Π₀ i : ι, M) : Π₀ i : ι, M := f + g

#lint -- all the arguments above were necessary

-- yet lean can't resolve this addition
@[simp] lemma to_finsupp_add [decidable_eq ι] [add_zero_class M] [Π m : M, decidable (m ≠ 0)]
  (f g : Π₀ i : ι, M) :
  dfinsupp.to_finsupp (f + g) = (f.to_finsupp + g.to_finsupp : ι →₀ M) :=
sorry -- `finsupp.coe_fn_injective rfl` would solve this if the statement were accepted

[Eric Wieser]

The word lemma gives me the error:

type mismatch at application
  f.to_finsupp
term
  f
has type
  Π₀ (i : ι), M : Type (max u_1 u_2)
but is expected to have type
  Π₀ (i : ?m_1), ?m_2 : Type (max ? ?)
Additional information:
Untitled-2: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch at application
    f.to_finsupp
  term
    f
  has type
    Π₀ (i : ι), M : Type (max u_1 u_2)
  but is expected to have type
    Π₀ (i : ?m_1), ?m_2 : Type (max ? ?)

and the + give me four errors, all roughly

type mismatch at application
  has_add.add f
term
  f
has type
  Π₀ (i : ι), M : Type (max u_1 u_2)
but is expected to have type
  Π₀ (i : ?m_1), ?m_2 : Type (max ? ?)

[Eric Wieser]

If I add underscores everywhere then it works:

@[simp] lemma to_finsupp_add [add_zero_class M] [Π m : M, decidable (m ≠ 0)] (f g : Π₀ i : ι, M) :
  @dfinsupp.to_finsupp _ M _ _ _ (f + g) =
    (@dfinsupp.to_finsupp _ M _ _ _ f + @dfinsupp.to_finsupp _ M _ _ _ g : ι →₀ M) :=
finsupp.coe_fn_injective $ dfinsupp.coe_add _ _

What's going on here? Why can't it infer M from the types of f and g?

[Eric Wieser]

It also seems there are different elaboration rules for dot notation - this works, but changing any of the to_finsupp calls to use dot notation fails:

@[simp] lemma to_finsupp_add [add_zero_class M] [Π m : M, decidable (m ≠ 0)] (f g : Π₀ i : ι, M) :
  (dfinsupp.to_finsupp (f + g) : ι →₀ M) =
    (dfinsupp.to_finsupp f + dfinsupp.to_finsupp g) :=
finsupp.coe_fn_injective $ dfinsupp.coe_add _ _