Module instance for dfinsupp

Stream: general

[Riccardo Brasca]

I don't understand why the second one fails, and all the other work... are we missing an instance?

import linear_algebra.direct_sum.finsupp

variables {R : Type*} [ring R]
variables {S : Type*} [semiring S]

open_locale direct_sum

--works
example {ι : Type*} (M : ι → Type*) [Π (i : ι), add_comm_monoid (M i)]
  [Π (i : ι), module S (M i)] : module S (Π₀ i, M i) := infer_instance

--doesn't work
example {ι : Type*} (M : ι → Type*) [Π (i : ι), add_comm_group (M i)]
  [Π (i : ι), module R (M i)] : module R (Π₀ i, M i) := infer_instance

--works! (monoids as modules over a ring)
example {ι : Type*} (M : ι → Type*) [Π (i : ι), add_comm_monoid (M i)]
  [Π (i : ι), module R (M i)] : module R (Π₀ i, M i) := infer_instance

--works!! (note that direct sum an dfinsupp are defeq)
example {ι : Type*} (M : ι → Type*) [Π (i : ι), add_comm_group (M i)]
  [Π (i : ι), module R (M i)] : module R (⨁ i, M i) := infer_instance

[Anne Baanen]

I have encountered similar bugs before, where the Pi type made inference fail.

[Yaël Dillies]

That's why we have both the dependent and independent versions, right?

[Anne Baanen]

See e.g.:

• https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclass.20resolution.20under.20binders/near/245176934
• https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/decidable_pred.20instance.20not.20found.20by.20typeclass.20search/near/219962294
• leanprover/lean4#509

[Riccardo Brasca]

I am not really complaining, what I really want is the last one, that works. But it should be literally the same as the second one...

[Kevin Buzzard]

Does it work in lean 4?

[Eric Wieser]

The reason is that we have a duplicate instance somewhere that specifically covers the failing case

[Eric Wieser]

Can you print the instance that's actually found?

[Eric Wieser]

I would guess we have both docs#direct_sum.module and docs#direct_sum.module'

[Riccardo Brasca]

example {ι : Type*} (M : ι → Type*) [Π (i : ι), add_comm_group (M i)]
  [Π (i : ι), module R (M i)] : module R (⨁ i, M i) := direct_sum.module

works

[Riccardo Brasca]

You can even replace direct_sum.module by dfinsupp.module and it still works (keeping the direct sum).

[Riccardo Brasca]

But

example {ι : Type*} (M : ι → Type*) [Π (i : ι), add_comm_group (M i)]
  [Π (i : ι), module R (M i)] : module R (Π₀ i, M i) := dfinsupp.module

doesn't work.

[Riccardo Brasca]

type mismatch, term
  @dfinsupp.module.{?l_1 ?l_2 ?l_3} ?m_4 ?m_5 ?m_6 ?m_7 ?m_8 ?m_9
has type
  @module.{?l_1 (max ?l_2 ?l_3)} ?m_4
    (@dfinsupp.{?l_2 ?l_3} ?m_5 (λ (i : ?m_5), ?m_6 i)
       (λ (i : ?m_5),
          @add_zero_class.to_has_zero.{?l_3} (?m_6 i)
            (@add_monoid.to_add_zero_class.{?l_3} (?m_6 i) (@add_comm_monoid.to_add_monoid.{?l_3} (?m_6 i) (?m_7 i)))))
    ?m_8
    (@dfinsupp.add_comm_monoid.{?l_2 ?l_3} ?m_5 (λ (i : ?m_5), ?m_6 i) (λ (i : ?m_5), ?m_7 i)) : Type (max
        ?l_1
        ?l_2
        ?l_3)
but is expected to have type
  @module.{u_1 (max ?l_1 ?l_2)} R
    (@dfinsupp.{?l_1 ?l_2} ι (λ (i : ι), M i)
       (λ (i : ι),
          @add_zero_class.to_has_zero.{?l_2} (M i)
            (@add_monoid.to_add_zero_class.{?l_2} (M i)
               (@sub_neg_monoid.to_add_monoid.{?l_2} (M i)
                  (@add_group.to_sub_neg_monoid.{?l_2} (M i)
                     (@add_comm_group.to_add_group.{?l_2} (M i) (_inst_3 i)))))))
    (@ring.to_semiring.{u_1} R _inst_1)
    (@add_comm_group.to_add_comm_monoid.{(max ?l_1 ?l_2)}
       (@dfinsupp.{?l_1 ?l_2} ι (λ (i : ι), M i)
          (λ (i : ι),
             @add_zero_class.to_has_zero.{?l_2} (M i)
               (@add_monoid.to_add_zero_class.{?l_2} (M i)
                  (@sub_neg_monoid.to_add_monoid.{?l_2} (M i)
                     (@add_group.to_sub_neg_monoid.{?l_2} (M i)
                        (@add_comm_group.to_add_group.{?l_2} (M i) (_inst_3 i)))))))
       (@dfinsupp.add_comm_group.{?l_1 ?l_2} ι (λ (i : ι), M i) (λ (i : ι), _inst_3 i))) : Type (max u_1 ?l_1 ?l_2)

[Eric Wieser]

Is your example really finding direct_sum.module for the add_comm_group case? Can you confirm with show_term?

[Eric Wieser]

Oh, looking at your last message; this is because unification can find the add_comm_monoid structure as an argument to direct_sum, but dfinsupp only takes has_zero so can't offer unification help.