Coercion instance problems with matrix exponential

Stream: mathlib4

[David Loeffler]

As part of PR #29648, I'm adding some lemmas about the topology of GL(n) and SL(n) over a topological ring. The reviewer for the PR (@Anatole Dedecker ) suggested these could live in Mathlib.Topology.Instances.Matrix, but this has brought on a strange coercion instance problem.

The problem is that the lemmas need some imports from Matrix.GeneralLinearGroup.Defs. Adding this import to Topology.Instances.Matrix means it is also transitively imported in the downstream file Analysis.Normed.Algebra.MatrixExponential, and the latter file will not compile with this import: we get an error

failed to synthesize
  CoeT (Matrix m m 𝔸) x (Matrix m m 𝔸)ˣ
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

I have no idea what this means. The problem seems to come from the following instance in GeneralLinearGroup/Defs.lean:

instance instCoeFun : CoeFun (GL n R) fun _ => n → n → R where
  coe A := (A : Matrix n n R)

Is this instance somehow bad? Or is it MatrixExponential that's doing something strange? I'd be grateful if someone could help me out here.

Tagging @Eric Wieser as the author of the matrix exponential files.

[Jovan Gerbscheid]

Can you share a #mwe that gives the deterministic timeout?

[David Loeffler]

import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
import Mathlib.LinearAlgebra.GeneralLinearGroup
import Mathlib.Algebra.Ring.Subring.Units
--import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

variable {𝕂 m 𝔸 : Type*}
  [Fintype m] [DecidableEq m] [Ring 𝔸] (U : (Matrix m m 𝔸)ˣ) (A : Matrix m m 𝔸)

#check U * A

This works, but it fails if you un-comment the last import line. (The other imports are precisely the files imported by GeneralLinearGroup.Defs, so the problem is this file specifically.)

[Jovan Gerbscheid]

Unification is trying really hard to fill in a metavariable of type CommRing 𝔸, but it only knows Ring 𝔸. This is an instance of the problem I describe and fix at #lean4 > Exponential blowup in unification with metavariables

In your example there are two instances that trigger this exponential slowdown: Matrix.SpecialLinearGroup.hasCoeToGeneralLinearGroup and Matrix.GeneralLinearGroup.instCoeFun. Turning them off locally solves the problem:

attribute [-instance] Matrix.SpecialLinearGroup.hasCoeToGeneralLinearGroup Matrix.GeneralLinearGroup.instCoeFun

[David Loeffler]

Ah, I see! So it is on a hopeless quest to prove that an arbitrary ring is commutative.

[David Loeffler]

The instance Matrix.GeneralLinearGroup.instCoeFun can actually be generalized to any ring (even semiring) without change. But hasCoeToGeneralLinearGroup is only meaningful over a commutative ring.

[Jovan Gerbscheid]

I would guess that docs#Matrix.GeneralLinearGroup is intentionally taking a CommRing assumption, equivalently to the special linear group.

[Matthew Ballard]

Using SMul instead of Mul in your check makes it much happier.

[Matthew Ballard]

Separately, there are lots of abbrevs around there.

[Sébastien Gouëzel]

@Jovan Gerbscheid, could you recap your RFCs / PRs to core improving the situation with typeclass inference? Hopefully at some point someone from the FRO will notice :-)
On my side I am still very sad with lean4#9077 which IMHO is a major bug but core is not really interested in fixing.

Maybe issues which are major on the mathlib side, but not so much from core point of view, is something where the Mathlib Iniative could help by providing some interface with the FRO? @Johan Commelin

[David Loeffler]

I can get it to work by

• generalizing Matrix.GeneralLinearGroup.instCoeFun to allow Semiring in place of CommRing
• locally disabling hasCoeToGeneralLinearGroup at the relevant places.

@Jovan Gerbscheid could you elaborate on why you think the CommRing assumption for GLn was intentional? Is it a Bad Thing to generalize it where possible? Certainly general linear groups over non-commutative rings are a thing that gets studied in some fields.

@Matthew Ballard unfortunately the original declaration had U * A * U⁻¹, so using SMul doesn't help. Are abbrevs a problem? Should GL become a def rather than an abbrev (which would come at a cost of a very considerable amount of extra boilerplate to copy over instances from Units)?

[Jovan Gerbscheid]

David Loeffler said:

Certainly general linear groups over non-commutative rings are a thing that gets studied in some fields.

In that case, feel free to generalize it in a separate PR.

[Matthew Ballard]

Sébastien Gouëzel said:

Jovan Gerbscheid, could you recap your RFCs / PRs to core improving the situation with typeclass inference? Hopefully at some point someone from the FRO will notice :-)
On my side I am still very sad with lean4#9077 which IMHO is a major bug but core is not really interested in fixing.

Maybe issues which are major on the mathlib side, but not so much from core point of view, is something where the Mathlib Iniative could help by providing some interface with the FRO? Johan Commelin

I turned off the default transparency for instance implicit arguments on a toolchain at some point but ran out of bandwidth so it could have done nothing. But it was seemingly simple.

[Matthew Ballard]

David Loeffler said:

(which would come at a cost of a very considerable amount of extra boilerplate to copy over instances from Units)?

This is could also be in scope for the Mathlib Initiative.

[Jovan Gerbscheid]

Sébastien Gouëzel said:

@Jovan Gerbscheid, could you recap your RFCs / PRs to core improving the situation with typeclass inference?

Yes, I realized now that my PR was still a draft and I hadn't made an issue, so core isn't to blame for not noticing.

[Jovan Gerbscheid]

Matthew Ballard said:

I turned off the default transparency for instance implicit arguments on a toolchain at some point but ran out of bandwidth so it could have done nothing. But it was seemingly simple.

Yes, to prove that lean#9077 can be solved, we need an experiment of this kind, showing that it fixes the problem, and that mathlib can reasonably adapt to it.

[Matthew Ballard]

I am not sure of the value def. Structure wrappers keep searches and unification more contained. abbrev’s are more convenient for recycling API. def is less characters to type?

[Jovan Gerbscheid]

That's exactly the issue in lean#9077, for many users there is some expectation that def keeps unification contained during type class search, but as it turns out, it does not always do this sufficiently.

[David Loeffler]

This thread has led to some fascinating-sounding discussions that I don't claim to understand, but I'm a little lost now as to how to actually solve my original problem. What should I do to fix the build failure in PR #29648? Is the fix I proposed, namely

I can get it to work by

• generalizing Matrix.GeneralLinearGroup.instCoeFun to allow Semiring in place of CommRing
• locally disabling hasCoeToGeneralLinearGroup at the relevant places.

acceptable?

[Jovan Gerbscheid]

When disabling the instance locally, you could also link to the issue about this slowdown (although I haven't made this issue yet)

[Matthew Ballard]

The local disabling seems to have precedent in the library already. It would be nice to keep track of it as an issue in case someone else comes back to this in the future

[Eric Wieser]

If the instance is bad it should probably be scoped and opened only in the files that need it

[Eric Wieser]

Possibly with the notation for SpecialLinearGroup

[Jovan Gerbscheid]

There is nothing wrong with the instance. The only thing is that it sometimes triggers an exponential slowness in unification that shouldn't be there in the first place

[Eric Wieser]

David Loeffler said:

I can get it to work by

By doing both of these things or either of these things?

[David Loeffler]

Eric Wieser said:

David Loeffler said:

I can get it to work by

By doing both of these things or either of these things?

Both – there's two separate instances that are (independently) troublesome (and the nicer solution that works for the first doesn't work for the second).

[Jovan Gerbscheid]

To be clear, it would also work to disable both instances locally. But one of them can be mathematically generalized, which just so happens to fix the performance problem.

[Jovan Gerbscheid]

Ok, I've now made the issue lean#10414

[David Loeffler]

Jovan Gerbscheid said:

Ok, I've now made the issue lean#10414

Thanks! I've added a note in the PR code referring to this.

[Matthew Ballard]

Matthew Ballard said:

The local disabling seems to have precedent in the library already.

Precisely https://github.com/leanprover-community/mathlib4/blob/d19d8deec21abd7c5e3b7cbb353e995449d5de5c/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean#L38

[Eric Wieser]

That's left from Lean3, where the coercion inserted an unwanted coeFn term

[Eric Wieser]

Now that coercions are inlined the motivation is gone

[David Loeffler]

So is this (GeneralLinearGroup/Defs.lean#L38) just cruft that should be removed, unrelated to the issue we've been discussing here?

[Eric Wieser]

We should at least try to remove it

[Matthew Ballard]

#29722 - let’s see if there are any unexpected problems

[Jovan Gerbscheid]

Quite a few of the attribute [-instance] around mathlib seem to simply be removable...

[David Loeffler]

Looks like the "bench-after-CI" label on #29722 hasn't caught the attention of the benchmark bot

[Lawrence Wu (llllvvuu)]

I hit the same thing in #29478 . I'll adopt the fix here

[Damiano Testa]

I think that, unfortunately, the bench-after-CI label needs to be present before the build workflow starts.

[Bryan Gin-ge Chen]

Damiano Testa said:

I think that, unfortunately, the bench-after-CI label needs to be present before the build workflow starts.

Ah, that was supposed to be fixed in #29392 but I just realized I missed something there.

#29726 should fix this for real.

[Damiano Testa]

I thought that I remember that there had been some fix, but I was not sure. Thanks for chasing it up: let's see how it works!