Zulip Chat Archive

Stream: general

Topic: typeclass inference of `add_comm_monoid` vs `add_comm_group`


view this post on Zulip Eric Wieser (Jul 21 2020 at 10:34):

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

view this post on Zulip Anne Baanen (Jul 21 2020 at 11:01):

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.

view this post on Zulip Anne Baanen (Jul 21 2020 at 11:05):

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.

view this post on Zulip Eric Wieser (Jul 21 2020 at 11:06):

Can priority be used to avoid needing the unifier?

view this post on Zulip Anne Baanen (Jul 21 2020 at 11:09):

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

view this post on Zulip Anne Baanen (Jul 21 2020 at 11:19):

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).

view this post on Zulip Anne Baanen (Jul 21 2020 at 11:34):

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.

view this post on Zulip Eric Wieser (Jul 21 2020 at 13:03):

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.

view this post on Zulip Eric Wieser (Jul 21 2020 at 14:02):

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


Last updated: May 09 2021 at 18:17 UTC