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