LinearEquiv.finrank_eq : typeclass instance problem is stuck

Stream: mathlib4

[Utensil Song]

For this #mwe

import Mathlib.RingTheory.FiniteType
import Mathlib.Tactic

open FiniteDimensional

example (R: Type uR) (A B: Type uA) [CommRing R] [AddCommGroup A] [AddCommGroup B]
  [Module R A] [Module R B] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :
  (A ≃ₐ[R] B) → finrank R A = finrank R B := by
  intro ha
  have hl := ha.toLinearEquiv
  /-
    typeclass instance problem is stuck, it is often due to metavariables

    Module ?m.2272 ?m.2274
  -/
  -- have hf := LinearEquiv.finrank_eq hl

  /-
    application type mismatch
      LinearEquiv.finrank_eq hl
    argument
      hl
    has type
      @LinearEquiv R R CommSemiring.toSemiring CommSemiring.toSemiring (RingHom.id R) (RingHom.id R)
        (_ : RingHomInvPair (RingHom.id R) (RingHom.id R)) (_ : RingHomInvPair (RingHom.id R) (RingHom.id R)) A B
        NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule
        Algebra.toModule : Type uA
    but is expected to have type
      @LinearEquiv R R Ring.toSemiring Ring.toSemiring (RingHom.id R) (RingHom.id R)
        (_ : RingHomInvPair (RingHom.id R) (RingHom.id R)) (_ : RingHomInvPair (RingHom.id R) (RingHom.id R)) A B
        AddCommGroup.toAddCommMonoid AddCommGroup.toAddCommMonoid inst✝⁵ inst✝⁴ : Type uA
  -/
  have hf' := @LinearEquiv.finrank_eq R A B _ _ _ _ _ hl

I can't see why the types mismatch. Any ideas?

[Eric Rodriguez]

can you try by convert hl to see what the diamond is?

[Eric Wieser]

You put two additive structures on A and B

[Eric Wieser]

[AddCommGroup A] [Semiring A] is bad as it defines + twice; it should be [Ring A]

[Utensil Song]

They come from the process trying to meet the need for both the ≃ₐ and finrank. Changing the statement to

example (R: Type uR) (A B: Type uA) [CommRing R] [Ring A] [Ring B]
  [Module R A] [Module R B] [Algebra R A] [Algebra R B] :
  (A ≃ₐ[R] B) → finrank R A = finrank R B :=

gives me almost identical error.

[Utensil Song]

Eric Rodriguez said:

can you try by convert hl to see what the diamond is?

Thanks, I don't understand where can I put this, tried a few places, none type checks.

[Eric Wieser]

[Module R A] [Algebra R A] is bad for the same reason, the latter implies the former

[Eric Wieser]

With both, you're giving two unrelated scalar multiplication actions

[Utensil Song]

Utensil Song said:

Eric Rodriguez said:

can you try by convert hl to see what the diamond is?

Thanks, I don't understand where can I put this, tried a few places, none type checks.

If I write convert LinearEquiv.finrank_eq, Lean hangs forever.

[Utensil Song]

Eric Wieser said:

[Module R A] [Algebra R A] is bad for the same reason, the latter implies the former

Thanks! That's probably the cause. Before merging into Ring, Algebra complains can't synth Module, and adding Module to address the complaint caused the stuck.

[Utensil Song]

It now becomes the one-liner it should be:

example (R: Type uR) (A B: Type uA) [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] :
  (A ≃ₐ[R] B) → finrank R A = finrank R B := fun ha => LinearEquiv.finrank_eq ha.toLinearEquiv

[Utensil Song]

And this was the motive:

import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
import Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
import Mathlib.RingTheory.FiniteType
import Mathlib.Tactic

open FiniteDimensional

local notation "Clℂ" => CliffordAlgebra CliffordAlgebraComplex.Q

example : finrank ℝ Clℂ = finrank ℝ ℂ := LinearEquiv.finrank_eq CliffordAlgebraComplex.equiv.toLinearEquiv