Adding an instance breaks `Mathlib.Tactic.Ring.Basic`

Stream: mathlib4

[Christopher Hoskin]

In https://github.com/leanprover-community/mathlib4/pull/12617 I'm trying to add an instance:

-- see Note [lower instance priority]
instance (priority := 100) CommSemiring.toNonUnitalNonAssocCommSemiring [CommSemiring α] :
    NonUnitalNonAssocCommSemiring α :=
  { inferInstanceAs (CommMonoid α), inferInstanceAs (CommSemiring α) with }

This then breaks Mathlib.Tactic.Ring.Basic:

[658/4453] Building Mathlib.Tactic.Ring.Basic
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/build/lib:/home/lean/.elan/toolchains/leanprover--lean4---v4.8.0-rc1/lib/lean:/home/lean/.elan/toolchains/leanprover--lean4---v4.8.0-rc1/lib:././.lake/build/lib /home/lean/.elan/toolchains/leanprover--lean4---v4.8.0-rc1/bin/lean -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit=false ././././Mathlib/Tactic/Ring/Basic.lean -R ./././. -o ././.lake/build/lib/Mathlib/Tactic/Ring/Basic.olean -i ././.lake/build/lib/Mathlib/Tactic/Ring/Basic.ilean -c ././.lake/build/ir/Mathlib/Tactic/Ring/Basic.c --json
error: ././././Mathlib/Tactic/Ring/Basic.lean:584:25-584:27: application type mismatch
  sub_pf «$pc» «$pd»
argument
  «$pd»
has type
  @HAdd.hAdd «$α» «$α» «$α»
      (@instHAdd «$α»
        (@Distrib.toAdd «$α»
          (@NonUnitalNonAssocSemiring.toDistrib «$α» NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring)))
      «$a» «$_c» =
    «$d» : Prop
but is expected to have type
  @HAdd.hAdd «$α» «$α» «$α»
      (@instHAdd «$α»
        (@Distrib.toAdd «$α»
          (@NonUnitalNonAssocSemiring.toDistrib «$α» NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring)))
      «$a» «$_c» =
    ?m.108578 : Prop
error: Lean exited with code 1

I've not looked into meta programming in Mathlib yet, so I'm not sure how to proceed?

Or is my instance wrong in some way?

Thanks,

Christopher

[Eric Wieser]

I would guess a well-placed assertInstancesCommute in the meta code will fix this

[Eric Wieser]

Ok, I fixed that issue in #12617 (it relates to issues with dependent types and Qq, as quoted terms that are equal by definition are not equal in Qq) but now we have a worse one relating to CoeFun not firing on linear maps