Another type class search issue

Stream: lean4

[Frédéric Dupuis]

I just ran across another type class search issue while porting LinearAlgebra/Isomorphisms in !4#2364. Basically, when defining a linear equiv f : M ≃[R] M, we are actually defining a semilinear equiv which (simplified) looks like:

def SemilinearEquiv (R S : Type _) [Semiring R] [Semiring S] (σ : R →+* S) {σ' : S →+* R}
    [RingHomInvPair σ σ'] := R → S

Of course, in the case of a plain linear equiv, σ is RingHom.id R, and σ' is supposed to be inferred as an outparam. However, now we have the following problem:

import Mathlib.Algebra.Ring.CompTypeclasses

def SemilinearEquiv (R S : Type _) [Semiring R] [Semiring S] (σ : R →+* S) {σ' : S →+* R}
    [RingHomInvPair σ σ'] := R → S

variable {R : Type _}

set_option trace.Meta.synthInstance true
-- This works just fine:
def g [Semiring R] : SemilinearEquiv R R (RingHom.id R) := id

-- Whereas this fails:
def f [Ring R] : SemilinearEquiv R R (RingHom.id R) := id

The error I see in the trace is:

[Meta.synthInstance] ❌ RingHomInvPair (RingHom.id R) ?m.450 ▼
  [] new goal RingHomInvPair (RingHom.id R) _tc.0 ▶
  [] ❌ apply @RingHomInvPair.ids to RingHomInvPair (RingHom.id R) ?m.483 ▼
    [tryResolve] ❌ RingHomInvPair (RingHom.id R) ?m.483 ≟ RingHomInvPair (RingHom.id ?m.486) (RingHom.id ?m.486)

So basically, it refuses to try to find the semiring in the ring. Any thoughts?

[Eric Wieser]

This is lean4#2074 again

[Eric Wieser]

Pretty much all of LinearAlgebra is impacted by this

[Frédéric Dupuis]

I thought this had been fixed...?

[Eric Wieser]

A fix was attempted but it was never merged into Lean4 master

[Jireh Loreaux]

Or rather I think it was merged and then reverted because it caused too many issues without lean4#2003, which is now merged.

[Eric Wieser]

Sorry, what I should have said was "there was never a commit to mathlib master that bumped lean4 to the version that included that change"

[Eric Wieser]

I think there were more problems than just it not working well without lean4#2003, but I don't remember what they were.