Zulip Chat Archive

Stream: lean4

Topic: Another type class search issue


Frédéric Dupuis (Feb 19 2023 at 01:03):

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 (Feb 19 2023 at 12:07):

This is lean4#2074 again

Eric Wieser (Feb 19 2023 at 12:07):

Pretty much all of LinearAlgebra is impacted by this

Frédéric Dupuis (Feb 19 2023 at 14:25):

I thought this had been fixed...?

Eric Wieser (Feb 19 2023 at 14:29):

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

Jireh Loreaux (Feb 19 2023 at 15:40):

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 (Feb 19 2023 at 15:41):

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 (Feb 19 2023 at 15:42):

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


Last updated: Dec 20 2023 at 11:08 UTC