Typeclass resolution

Stream: mathlib4

[Joachim Breitner]

Sorry if this is a FAQ, but I couldn’t find it (easily), and the porting wiki does not address it:
It seems that lean4 fails to find instances where lean3 would, because lean4 does no or less unfolding of the definitions in the goal (or something like that, I might be wrong).
What is the suggested fix? Add more instances (which are defined to be def-equal to the other instance)? (Or maybe I am barking up the wrong tree)

[Yury G. Kudryashov]

Any specific examples?

[Yury G. Kudryashov]

(e.g., a link to a PR or an #mwe)

[Kevin Buzzard]

Typeclass inference has changed in several ways between Lean 3 and Lean 4. There is at least one open issue where regressions have been observed. Another has just been closed an hour ago, but it will take a while to filter up to mathlib. If you can point me to an explicit example I can try to figure out whether it's covered by existing issues on the Lean 4 repo.

[Joachim Breitner]

I am not 100% sure this is the problem, but in map_neg in https://github.com/leanprover-community/mathlib4/pull/1979/files#diff-6f14283bfbc75a32a870660bc104a4b628a3645bacef2d02343637199a25f517R1062 I get

failed to synthesize instance
  Neg (M →ₗ[R] M₂)

but there is

/-- The negation of a linear map is linear. -/
instance : Neg (M →ₛₗ[σ₁₂] N₂) :=

in LinearMap.lean and that is the instance that was used in lean3

[Joachim Breitner]

Similarly, in https://github.com/leanprover-community/mathlib4/pull/1765/files I added

instance decidableSubsetFinset [DecidableEq α] {s t : Finset α} : Decidable (s ⊆ t) :=
  decidableDforallFinset

to Mathlib/Data/Finset/Basic.lean for (presumably) the same reason. There, it seems lean3 unfolded ⊆ and found an instance using the underlying definition.

[Joachim Breitner]

(the new behavior is probably cleaner, the question is more about what's the right way to adapt)

[Gabriel Ebner]

(deleted)

[Kevin Buzzard]

The first one looks familiar. If you try this:

set_option trace.Meta.synthInstance true
set_option trace.Meta.isDefEq true
#synth Neg (M →ₗ[R] M₂)
#exit

and unfold the traces (click on the triangles) you can see [] ❌ R →+* R =?= R →+* R at some point. If you now switch on pp.all as well you can see that the actual goal is

  [] ❌ @RingHom.{?u.854759, ?u.854759} R R
                  (@Semiring.toNonAssocSemiring.{?u.854759} R (@Ring.toSemiring.{?u.854759} R inst✝⁴))
                  (@Semiring.toNonAssocSemiring.{?u.854759} R
                    (@Ring.toSemiring.{?u.854759} R
                      inst✝⁴)) =?= @RingHom.{?u.854759, ?u.854759} R R
                  (@NonAssocRing.toNonAssocSemiring.{?u.854759} R (@Ring.toNonAssocRing.{?u.854759} R inst✝⁴))
                  (@NonAssocRing.toNonAssocSemiring.{?u.854759} R (@Ring.toNonAssocRing.{?u.854759} R inst✝⁴))

and although I need to get back to marking (and in particular can't look at the second one right now) it would not surprise me if these were defeq if eta for structures is on (which it is usually) but not defeq if it's off (and for the version of Lean being used by mathlib it's off at this point). In short, hopefully this issue is fixed in lean4 master https://github.com/leanprover/lean4/pull/2093 and it's just a matter of time before the issue permeates up to mathlib4.

[Eric Wieser]

Is there an open PR already to bump mathlib4's lean4 version, or are we waiting for a lean4 release?

[Ruben Van de Velde]

nightly-2023-02-06 has been out for two hours, so go for it :)

[Kevin Buzzard]

Does it definitely contain the fix?

[Ruben Van de Velde]

It claims to have

15a045e fix: reenable structure eta during tc search

is that the one?

[Johan Commelin]

lgtm

[Johan Commelin]

@Eric Wieser @Ruben Van de Velde is either of you working on this?

[Eric Wieser]

I don't plan to for at least a few hours

[Ruben Van de Velde]

(deleted)

[Joachim Breitner]

JFTR, I checked if with the latest lean4 bump I can remove the instance that I added while porting (https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Typeclass.20resolution/near/326012518), but it still seems to be required. Not sure if that’s a noteworthy difference in instance resolution.

[Johan Commelin]

Thanks for checking!

[Gabriel Ebner]

No changes are expected from 2003. It's only supposed to be faster.