Matrix multiplication notation failed

Stream: mathlib4

[nemo]

I was trying to write something about matrices when I encounted the following error, where lean seems to have failed to parse the matrix multiplication notation under certain circumstances.

It is an unexpected bug or did I use the wrong way to write it?

import Mathlib
example [RCLike 𝕜] [Fintype m] [Fintype n] (A : Matrix m n 𝕜) (B : Matrix n n 𝕜) :
  A * B = A := by
  /-
  failed to synthesize
  CoeT (Matrix n n 𝕜) x (Matrix m n 𝕜)
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached
Note: Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.
Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
  -/
  sorry

example [RCLike 𝕜] [Fintype m] [Fintype n] (A : Matrix m n 𝕜) (B : Matrix n n 𝕜) :
  Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul A B = A := by
  /-
  Works well when I write the mul explicitly
  -/

example [RCLike 𝕜] [Fintype m] (A : Matrix m m 𝕜) (B : Matrix m m 𝕜) :
  A * B = A := by
  /-
  Also works if the matrix is square
  -/
  sorry
  sorry

[Notification Bot]

This topic was moved here from #lean4 > Matrix multiplication notation failed by Yury G. Kudryashov.

[Notification Bot]

This topic was moved here from #new members > Matrix multiplication notation failed by Yury G. Kudryashov.

[Yury G. Kudryashov]

Sorry for moving twice. First I thought that you've made a typo, then I realized that I've misread your message. I guess, when the parser sees that the type of the first multiplier is the same as the type of the product, it tries to elaborate the second multiplier as the same type.

[Yury G. Kudryashov]

CC: @Eric Wieser

[Yury G. Kudryashov]

As a temporary workaround, you can use HMul.hMul A B. I know that it looks bad.

[Robin Arnez]

This looks like we have some terrible coercion instances, specifically:

import Mathlib

attribute [-instance] IsometryClass.instCoeOutIsometryEquiv
attribute [-instance] ContinuousMonoidHom.instCoeOutOfMonoidHomClassOfContinuousMapClass
attribute [-instance] ContinuousAddMonoidHom.instCoeOutOfAddMonoidHomClassOfContinuousMapClass
attribute [-instance] HomeomorphClass.instCoeOutHomeomorph
attribute [-instance] StarRingEquivClass.instCoeHead
attribute [-instance] CoalgEquivClass.instCoeToCoalgEquiv
attribute [-instance] PositiveLinearMapClass.instCoeToLinearMap
attribute [-instance] SemilinearEquivClass.instCoeToSemilinearEquiv
attribute [-instance] SemilinearMapClass.instCoeToSemilinearMap
attribute [-instance] BialgHomClass.instCoeToBialgHom
attribute [-instance] LinearMapClass.instCoeToLinearMap
attribute [-instance] NonUnitalStarRingHomClass.instCoeHeadNonUnitalStarRingHom
attribute [-instance] StarAlgEquivClass.instCoeHead
attribute [-instance] CompletelyPositiveMapClass.instCoeToCompletelyPositiveMap
attribute [-instance] CoalgHomClass.instCoeToCoalgHom
attribute [-instance] SignType.instCoeTail

example [RCLike 𝕜] [Fintype m] [Fintype n] (A : Matrix m n 𝕜) (B : Matrix n n 𝕜) :
    A * B = A := by
  sorry

works

[Kenny Lau]

wow, thanks for taking the time to diagnose all that!

[Robin Arnez]

Wait, actually

import Mathlib

attribute [-instance] SignType.instCoeTail

example [RCLike 𝕜] [Fintype m] [Fintype n] (A : Matrix m n 𝕜) (B : Matrix n n 𝕜) :
    A * B = A := by
  sorry

is enough?

[Robin Arnez]

Still I don't like all of these other ones firing for all coercions

[Robin Arnez]

Alright I'm officially confused;

import Mathlib

set_option trace.Meta.synthInstance true
variable [RCLike 𝕜] [Fintype m] [Fintype n] in
#synth CoeTail SignType (Matrix m n 𝕜)

is the problem but it takes less steps to resolve Zero (Matrix m n 𝕜), One (Matrix m n 𝕜) and Neg (Matrix m n 𝕜) combined?

[Aaron Liu]

Yury G. Kudryashov said:

I guess, when the parser sees that the type of the first multiplier is the same as the type of the product, it tries to elaborate the second multiplier as the same type.

I don't think the typeclass takes into account the type of the product at all, since it's an outParam.

[Yury G. Kudryashov]

Should we use docs#CoeHTCT ? I know that it's discouraged in the docstring.

[Yury G. Kudryashov]

Or should the coercion from SignType be a CoeHead?

[Aaron Liu]

Why is docs#SignType.cast even a coercion

[Aaron Liu]

is it even used that much

[Aaron Liu]

not like Nat.cast which is everywhere

[Yury G. Kudryashov]

I think it's convenient to have it as a coercion, but CoeHead may be better so that it applies only for coercions from SignType.

[Robin Arnez]

The right thing to do is CoeDep I believe

[Robin Arnez]

I don't think you can do CoeHead because there's no way to know what to coerce to with that

[Robin Arnez]

Alright, I opened #31168

[Eric Wieser]

It would be great to note in the docstring for CoeDep that it is useful in nondependent cases

[Yury G. Kudryashov]

BTW, why do we have a separate CoeDep, not just extra instances of CoeT?

[Aaron Liu]

they seems to serve different function

[Aaron Liu]

CoeDep is for dependent coercions specifically and CoeT is for all the coercions

[Aaron Liu]

that's my guess

[Yury G. Kudryashov]

They have the same signature. CoeT has instances coming from non-dependent coercions + an instance from CoeDep. I don't understand why not just use specific CoeT instances instead of having an extra class.

[Robin Arnez]

Alright I see there is a bit of a problem; we have a coercion diamond between docs#SemilinearMapClass.instCoeToSemilinearMap and docs#LinearEquiv.instCoeLinearMap

[Robin Arnez]

I see that there is also a theorem about this: docs#LinearEquiv.toLinearMap_eq_coe. Which of these is supposed to be the normal form then?

[Yury G. Kudryashov]

AFAIR, @Yaël Dillies mentioned that *Class.instCoe* instances are going to be removed, not sure about the details.

[Anne Baanen]

Yury G. Kudryashov said:

BTW, why do we have a separate CoeDep, not just extra instances of CoeT?

CoeT is an implementation detail that users should not implement directly. It's unlikely that this will get a large redesign in the nearby future, but I can certainly imagine that CoeT will be replaced someday.

(Similarly, we should really have dealt already with all the CoeTC instances still defined in Mathlib...)