Can `unification_hint` help with casting?

Stream: general

[Eric Wieser]

If I have a (a : alternating_map R M N ι) and want to cast it to a multilinear_map, I seem to have no choice but to spell out (a : multilinear_map R (λ i : ι, M) N) which is a mouthful. Is there any way I can train the unifier to let me put underscores in there? Ideally I could write(a : multilinear_map _ _ _) and lean would work it out.

[Kevin Buzzard]

The problem I guess is that in theory there could be a coercion to some other multilinear map too

[Kevin Buzzard]

so is this what unification hints do?

[Eric Wieser]

In part this is me trying to answer the question "what do unification hints do"

[Kevin Buzzard]

I heard very early on in Lean 4 development that they weren't planning on having them so I never took them seriously. Now it turns out that they are there in Lean 4 too so perhaps it's time I figured out what they are.

[Eric Wieser]

I went back through the zulip history and found:

• The tests in lean 3, which are completely contrived and seem mostly to be "these are a backdoor for irreducible", which probably is a useful trick to know
• The lean-omin notes on them
• That Lean Together 2019 workshop that I dropped the link to

[Bryan Gin-ge Chen]

If you figure them out (and they seem useful), please write something up for the community webpage!

[Johan Commelin]

@Kenny Lau see Eric's post for some pointers about unification hints. :up:

[Cyril Cohen]

There is actually a research paper about them: https://www.cs.unibo.it/~sacerdot/PAPERS/tphol09.pdf

[Eric Wieser]

Some more motivation for the original question - can unification hints make this legal?

import data.equiv.ring

-- fails without filling the underscores. Can we teach lean to guess?
example {M N : Type*} [semiring M] [semiring N] (f : M ≃+* N) := (↑f : _ →+* _)