Inference faiing, but not inside a λ

Stream: general

[Anne Baanen]

I just encountered this weird failure of typeclass inference:

import data.finsupp.basic

noncomputable example {η R : Type*} [semiring R] {ιs : η → Type*} : Π i, add_comm_monoid (ιs i →₀ R) := infer_instance -- fails
noncomputable example {η R : Type*} [semiring R] {ιs : η → Type*} : Π i, add_comm_monoid (ιs i →₀ R) := λ i, infer_instance -- works

Any idea why the first one fails and how to make it work again?

[Anne Baanen]

Looking at trace.class_instances, the first thing it does is @finsupp.add_comm_monoid (?x_1 i) (?x_2 i) (?x_3 i) failed is_def_eq, but that should "obviously" be defeq.

[Anne Baanen]

Aha, the expected type of the instance contains mul_zero_class.to_has_zero and finsupp.add_comm_monoid uses add_zero_class.to_has_zero.

[Anne Baanen]

And indeed, after local attribute [-instance] mul_zero_class.to_has_zero the first infer_instance works again.

[Anne Baanen]

So I guess the question is: why is semiring.to_monoid_with_zero.to_mul_zero_class.to_has_zero not defeq to semiring.to_add_comm_monoid.to_add_monoid.to_add_zero_class.to_has_zero, unless you add the λ?

[Eric Wieser]

I've seen this before, but never worked out what was going on