Zulip Chat Archive

Stream: general

Topic: Typeclass inference can't fill in parameters


Eric Wieser (Feb 11 2021 at 16:37):

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 (Feb 11 2021 at 16:37):

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

Eric Wieser (Feb 11 2021 at 16:42):

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 (Feb 11 2021 at 16:43):

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 (Feb 11 2021 at 17:22):

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


Last updated: Dec 20 2023 at 11:08 UTC