add a new superclass, need some new @s

Stream: general

[Scott Morrison]

We've currently got three PRs open where someone has added a new super-class to an existing class, and then in unexpected places they've need to write an extra @ to get a lemma to fire.

These are at

• https://github.com/leanprover-community/mathlib/pull/6786#discussion_r598341749
• https://github.com/leanprover-community/mathlib/pull/6797#discussion_r598307156
• https://github.com/leanprover-community/mathlib/pull/6775#discussion_r598005391

Could we get e.g. @Mario Carneiro, @Gabriel Ebner, or @Rob Lewis to help diagnose?

[Riccardo Brasca]

The same happened to me here https://github.com/leanprover-community/mathlib/pull/6746

[Anne Baanen]

For #6786 it looks like there is a subproblem with a diamond (semiring -> monoid_with_zero -> has_zero and semiring -> non_unital_non_assoc_semiring -> has_zero) that the elaborator needs to do a lot of work on. Somehow it doesn't use the rest of the expression to infer missing metavariables, instead choosing nat as a default value. I think the problem has turned from first-order to higher-order unification, and that higher-order unification makes some unfortunate choices here.

[Kevin Buzzard]

Could there be a cheap fix involving lowering or raising a priority?

[Anne Baanen]

I expect that changing priorities would fix one half of usages and break the other half. It might well be possible that the fixed half is exactly the lemmas that are in mathlib now, and the broken half the ones that are added later.

[Kevin Buzzard]

Unification hints?

[Gabriel Ebner]

I also think that there's a problematic diamond at play here. But the issue is not related to higher-order unification, it is plain old first-order unification:

[Gabriel Ebner]

The first example in that PR requires unifying 0 and 0, which is obviously hard.

[Gabriel Ebner]

It's hard because these two come from the two edges of the diamond. Essentially (skipping a few intermediate type classes):

@has_zero.zero ?m_1 (field.to_has_zero ?m_2) =?= @has_zero.zero ?m_1 (monoid_with_zero.to_has_zero ?m_3)

[Gabriel Ebner]

The problem is that Lean needs to assign ?m_2 : field ?m_1 or ?m_3 : monoid_with_zero ?m_1.
But there is no obvious choice for ?m_2 or ?m_3. Or at least none that Lean could find by unfolding field.to_has_zero.

[Gabriel Ebner]

Kevin Buzzard said:

Unification hints?

@[unify]
def unif_hint {α : Type} [i : monoid_with_zero α] [j : semiring α] : unification_hint :=
{ pattern := non_unital_non_assoc_semiring.to_mul_zero_class α ≟
    @monoid_with_zero.to_mul_zero_class α i,
  constraints := [semiring.to_monoid_with_zero α ≟ i] }

[Gabriel Ebner]

Unfortunately, unification hints are pretty broken in Lean 3. For example, the hint above doesn't work if you replace Type by Type*...

[Eric Wieser]

That probably explains why I've never had any luck doing anything with a unification hint, as Type* is muscle memory at this point.

[Gabriel Ebner]

AFAICT the Lean 4 unification hints have exactly the same bug. I'm trying it out now.

[Gabriel Ebner]

I can't reconstruct this issue in Lean 4. Mostly because Lean 4 will completely refuse to elaborate terms if it can't synthesize all instance arguments. For example, you just can't use cases le_or_gt _ _ in Lean 4.

[Oliver Nash]

Thanks @Gabriel Ebner for the explanation (which I have yet to digest) and especially for adding this commit while I was tied up with other things. You saved me a lot of time :-)

[Riccardo Brasca]

Something interesting happen in one of my PR, see https://github.com/leanprover-community/mathlib/pull/6831#discussion_r599508067

If you don't want to look at the two PR here is what happened: in #6746 I introduced semi_normed_group, and several lemmas stopped working. The solution was almost always to use some extra @. The PR got bigger and bigger, so I decided to split it, and in #6831 I generalized Lipschitz maps for pseudo_emetric_space (this was part of the other PR). Now, some of the problems appeared also in this PR (this is already interesting, since I thought they come from the new class semi_normed_group, while they come from Lipschitz maps). Even more interesting, a new problem appeared (of the same nature), the one in the above comment. Now, I know that it will disappear when everything is generalized to semi_normed_group, so I now think that also the other ones will go away if everything is stated in the correct generality.