coe_fn and class instances

Stream: general

[Yury G. Kudryashov]

I tried to redefine free_group.to_group as a bundled monoid_hom, and failed. It turns out that to_group f has type @monoid_hom.{u v} (free_group.{u} α) β (@group.to_monoid.{u} (free_group.{u} α) (@free_group.group.{u} α)) (@group.to_monoid.{v} β ?m_1), and Lean doesn't try to fill in ?m_1 before doing the coe_fn search. Any chance to have this fixed in 3.x? I have no idea if it is a hard or an easy task.

[Yury G. Kudryashov]

I mean, a proper fix would make Lean realize that this is monoid_hom _ _, so we already know how to coerce it to a function but I guess it might be easier to fix the order of instance resolution thus fixing a bug in some cases.

[Reid Barton]

This issue comes up in many contexts, frequently with equiv. For example, in the type of adjunction.hom_equiv:

hom_equiv : Π (X Y), (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)

We would much prefer X and Y to be implicit parameters, since they are nearly always obvious from context. But then the type (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y) is not yet fully known and so it will not be usable as a function because the coercion will not fire. You always have to specify X and Y explicitly (explicitly enough that they can be inferred without considering the context at the use site of hom_equiv).

[Reid Barton]

Fixing this would mean allowing instance search to run (or, perhaps, allowing it to succeed) when there are still metavariables in the goal of the instance search (here coe_to_fun (monoid_hom ?m_1 ?m_2) or similar). I would say it is unclear how difficult this would be to change, and also unclear what other problems it might introduce.

[Yury G. Kudryashov]

In my example it is more like coe_to_fun (@monoid_hom α β _inst_1 ?m1)

[Yury G. Kudryashov]

I mean that both α and β are already known.

[Yury G. Kudryashov]

It would be strange to make monoid β (or group β in my example) an explicit parameter.

[Reid Barton]

I guess it is a bit different because you expect the monoid beta argument also to be supplied by instance search, right?

[Yury G. Kudryashov]

Right.

[Reid Barton]

Seems like a delicate situation

[Yury G. Kudryashov]

BTW, is there any reason not to go the Python way? I mean, if we want to treat f as a function, try f.to_fun first; if it falls, try coe_fn for compatibility.

[Yury G. Kudryashov]

The first option will work in (almost?) all mathlib use cases

[Yury G. Kudryashov]

This particular case (not-yet-elaborated class instance makes coe_fn fail) makes it hard to use bundled homs in free_group.to_group, quotient_group.lift and AFAIR mv_polynomial.map hits the same problem.

[Yury G. Kudryashov]

BTW, is it going to work in Lean 4?

[Reid Barton]

Supposedly

[Yury G. Kudryashov]

How hard would be to make a workaround for Lean3?

[Sebastien Gouezel]

Just to mention that this is the reason why, in the manifold files, I use f.to_funand f.inv_fun for local homeos or local equivs: I first tried with coercions, and Lean got confused all the time.

[Patrick Massot]

This is a well-known issue. Coercions to functions just don't work in Lean 3.

[Patrick Massot]

We can only hope they will work in Lean 4.

[Kevin Buzzard]

A student of mine is writing a group cohomology repo using bundled homs and coercions to functions. We're just at this stage basically, we need to make a decision about whether to coerce or not. I thought that coercions worked quite well at this basic level (we're doing morphisms of G-modules). Now you're making me wonder whether we should switch but I don't think Anca had too many problems when she did H^0 and H^1 and also used bundled G-module homs

[Reid Barton]

I wouldn't necessarily be too eager to switch away from coercions, particularly if you don't intend to PR the result to mathlib. It's hard to predict whether you will encounter these inference issues.

[Reid Barton]

And it's not really that hard to switch later anyways, so not much is riding on the choice

[Sebastian Ullrich]

Reid Barton said:

Supposedly

Indeed

[Yury G. Kudryashov]

Since @Gabriel Ebner fixed one bug with coe_fn, let me try to revive this thread. Is it hard to make coe_fn work when some arguments are missing, i.e., try to unfold has_coe_to_fun.F and see if it actually uses the missing arguments? If this is hard, what about looking up missing [class_instance _] arguments?