Zulip Chat Archive

Stream: general

Topic: Inference faiing, but not inside a λ


Anne Baanen (Apr 07 2021 at 09:56):

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 (Apr 07 2021 at 10:01):

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 (Apr 07 2021 at 10:04):

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 (Apr 07 2021 at 10:05):

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

Anne Baanen (Apr 07 2021 at 10:08):

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 (Apr 07 2021 at 11:17):

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


Last updated: Dec 20 2023 at 11:08 UTC