unification weaker in lean4

Stream: mathlib4

[Eric Rodriguez]

time and time again, when I've ported, unification has felt far weaker that in lean3, making many things like congr_arg _ needing to be replaced with congrArg (· * r). I guess some part of this is to do with the heterogeneous operations by default, but I fear this is gonna hurt more and more the deeper into porting we go :(

[Heather Macbeth]

@Eric Rodriguez I agree with the "general impression", but do you have time to make a mwe? I think we should be reporting these things in the hope of getting specific changes to the algorithm. The devs have done this before.

[Eric Rodriguez]

here's one simple one, no imports needed:

example (a b c : Nat) : a = b → a * c = b * c := congrArg _ --fails, works with (· * c)

[Jireh Loreaux]

Is the issue that we need to fix the unification algorithm, or is it that we need to provide Lean with unification hints now? I was under the impression that the latter is something it might be helpful to start doing again, even though we banned it in mathlib 3.

[Eric Rodriguez]

what's a unification hint?

[Mario Carneiro]

I've never come across a situation where a unification hint looks like the best most robust solution, compared to things like changing the unification algorithm itself

[Mario Carneiro]

This seems like a MWE example of unification hints:

unif_hint foo (x : Nat) where x ≟ 5 ⊢ 2 * x ≟ 10

def Even (n : Nat) := ∃ x, n = 2 * x

theorem even_double : Even (2 * x) := ⟨_, rfl⟩

example : Even 10 := even_double

except it doesn't work

[Eric Wieser]

What if you flip the equality?

[Mario Carneiro]

no dice

[Kevin Buzzard]

@Eric Rodriguez are you going to open a Lean 4 issue explaining the regression? This worked fine in Lean 3.

[Eric Rodriguez]

lean4#2051

[Jireh Loreaux]

I have another issue where unification is annoyingly failing, unfortunately, I have no idea how to minimize as it is deep in GroupTheory.Coset. If you want to have a look, check out this commit: https://github.com/leanprover-community/mathlib4/pull/1874/commits/2c3b43f2c621dfc5cdebe8d78d5ce93aede31d26

I added a section test where you can see the problem.

[Jireh Loreaux]

The workaround is just to add the type ascription, but it's very annoying, and as the types get harder to state it only gets more annoying. I'm going to keep working on this file, and I'll delete that section test, so if you want to see it make sure to check out that specific commit.

[Jireh Loreaux]

@Mario Carneiro :up:

[Yury G. Kudryashov]

I need to specify implicit args here and there in topology.constructions.