typeclass inference of `add_comm_monoid` vs `add_comm_group`

Stream: general

[Eric Wieser]

Anne Baanen said:

There should be no issues making arguments to functions more general, since any consumers must declare these arguments themselves (unless they share a variables statement with your definition.)

This seems to fall apart once the requirements are pi-instances - see this small PR for an example

[Anne Baanen]

As far as I can tell, you can replace the first typeclass argument (λ i, by apply_instance) in your example with infer_instance in the third argument and it will still work.

[Anne Baanen]

The error comes from diamond inheritance in comm_group -> {comm_monoid, group} -> monoid, and the unifier is not smart enough to unify the comm_monoid.to_monoid (comm_group.to_monoid ?) that it expects with the instance group.to_monoid (comm_group.to_group __inst_3) that it has inferred.

[Eric Wieser]

Can priority be used to avoid needing the unifier?

[Anne Baanen]

Possibly. I'm not an expert in dealing with typeclass diamonds, though.

[Anne Baanen]

The priority was tweaked in the opposite direction in #2848:

I have tweaked a few instance priorities to make sure that things don't go too bad: there are often additional steps in typeclass inference, going from ring to semiring and from add_comm_group to add_comm_monoid, so I have increased their priority (putting it strictly between 100 and 1000), and adjusted some other priorities to get more canonical instance paths, fixing some preexisting weirdnesses (notably in multilinear maps).

[Anne Baanen]

This is breaking my head. If we add a line to direct_sum:

local attribute [instance, priority 1] add_comm_group.to_add_group

def direct_sum : Type* := Π₀ i, β i

then the following works in direct_sum_module:

instance : semimodule R (direct_sum ι M) := @dfinsupp.to_semimodule _ M _ _ _ _

or:

instance : semimodule R (direct_sum ι M) := @dfinsupp.to_semimodule _ _ _ _ infer_instance _

But any other variations give a type error.

[Eric Wieser]

I don't have an understanding as to why, but relaxing a few more constraints seems to have set the linked PR on a possibly successful build... Guess I'll wait and see.

[Eric Wieser]

Yep, got it working #3490 is now passing. There's some really ugly _ introductions that had to happen to make it work.

[Oliver Nash]

I'm having trouble inferring an add_comm_group class on a direct sum of submodules. Here's a MWE:

import linear_algebra.direct_sum_module

open_locale direct_sum

variables (ι R M : Type*) [ring R] [add_comm_group M] [module R M] (I : ι → submodule R M)

 -- succeeds
def foo : add_comm_monoid (⨁ i, I i) := infer_instance

 -- fails
def bar : add_comm_group (⨁ i, I i) := infer_instance

 -- fails, error seems to make sense; `coe_sort` doesn't have a pi rule I guess
def baz : add_comm_group (⨁ i, I i) := direct_sum.add_comm_group I

-- succeeds
def qux : add_comm_group (⨁ i, I i) := direct_sum.add_comm_group (λ i, ↥(I i))

[Oliver Nash]

My problem is essentially the failure of bar and I'm wondering what is the right solution. One solution would be to register qux as an instance but I'd guess this is fixing a symptom rather than a root cause.

[Oliver Nash]

Any advice from experts would be most gratefully received!

[Eric Wieser]

This is a known problem, and I think the workaround is to just add an almost duplicate instance like I've tried in #8221

[Eric Wieser]

@Kevin Buzzard made a minimal repro for lean4 and they fixed it there, but I'm kinda suspicious the fix only fixes a small subset of this type of problem given the description of how the fix works.

[Eric Wieser]

Unfortunately I can't tell if #8221 is actively a bad idea, or if we just have too many proofs on the borderline of timing out

[Oliver Nash]

Interesting thanks. I guess I'll just add the instance I need in a similar spirit to #8221 and move on with my life.

[Oliver Nash]

I'll also link to this conversation https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclass.20resolution.20under.20binders for the sake of anyone coming here in the future.

[Kevin Buzzard]

I think it would be a really interesting and important project to try and manually make these typeclasses in Lean 4, to see what the devs think. There's no reason we can't start experimenting with the new typeclass inference now -- and it's what Leo wants us to do. I've already made a bunch of the algebra hierarchy in mathlib4 and there are UK undergraduates (both current and former) already actively writing mathlib 4 code.

[Kevin Buzzard]

It's no secret that Leo sometimes has a difficult relationship with mathematicians, but he has spent the last few of his life working furiously on what he hopes is his masterpiece and he would really like us to do small experiments with it. This sounds like a perfect small experiment to me.

[Kevin Buzzard]

I should also say that there's a schemes branch where I'm extremely slowly manually porting the definition of a scheme to lean 4. Let's make schemes in Lean again! It's one of my hobbies! Feel free to help anyone

[Kevin Buzzard]

@Cyril Cohen are you interested in any of these projects?

[Kevin Buzzard]

@Chris Hughes ?

[Kevin Buzzard]

This sounds like both good fun and cutting edge type theory

[Oliver Nash]

I'm in favour of this. I have no idea how hard / easy it would be to make these typeclass in Lean 4 but I'd be up for trying towards the end of next week if someone else doesn't beat me to it.