Typeclass inference can't fill in parameters

Stream: general

[Eric Wieser]

What's going on here?

import linear_algebra.basic
import data.dfinsupp

variables {ι : Type*} {R : Type*} (S : Type*) {M : ι → Type*} {N : Type*}

variables [decidable_eq ι]
variables [semiring R] [Π i, add_comm_monoid (M i)] [Π i, semimodule R (M i)]
variables [add_comm_monoid N] [semimodule R N]

def ok : add_comm_monoid (Π₀ i, M i →ₗ[R] N) :=
  @dfinsupp.add_comm_monoid ι (λ i, M i →ₗ[R] N) _
def fail1 : add_comm_monoid (Π₀ i, M i →ₗ[R] N) :=
  @dfinsupp.add_comm_monoid ι _
def fail2 : add_comm_monoid (Π₀ i, M i →ₗ[R] N) :=
  dfinsupp.add_comm_monoid
def fail2 : add_comm_monoid (Π₀ i, M i →ₗ[R] N) :=
  by apply_instance

[Eric Wieser]

docs#dfinsupp.add_comm_monoid isn't found without way too much help

[Eric Wieser]

This reveals some of the pain:

def ok_but_scary : add_comm_monoid (Π₀ i, M i →ₗ[R] N) :=
begin
  convert dfinsupp.add_comm_monoid,
  swap,
  apply_instance,
  refl,
end

[Eric Wieser]

Possibly related to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/class.20instance.20resolution.20failure/near/225688941, since both use typeclasses with quantifiers

[Eric Wieser]

I found a workaround for this in #6185, but it's a monster