!4#3552 (LinearAlgebra.Matrix.ToLin)

Stream: mathlib4

[Scott Morrison]

I have !4#3552 (LinearAlgebra.Matrix.ToLin) working.

I found the before we started using etaExperiment, people were often hacking around the issue by adding (or subtracting!) various instances as needed. These instances were then accumulating, and leading to typeclass search timeouts.

Thus I've done a lot of cleanup: removing hacks adding or removing instances, and more uniformly just using etaExperiment.

To ease review, I've separated out those changes as !4#3668.

[Scott Morrison]

ToLin is on the critical path, so it would be great if these could be speedily reviewed. :-)

[Eric Wieser]

I was suspicious that adding those instance hacks might make the problem worse, thanks for confirming that suspicion!

[Scott Morrison]

It turns out !4#3668 was more complicated than I at first thought (I fixed ToLin, but broke other files that CI picked up). Hopefully ready for review again soon (TM).

[Scott Morrison]

Fortunately the instance hacks are all well signposted with porting notes, so easy to track down and exterminate. :-)

[Scott Morrison]

Okay, the etaExperiment cleanup branch !4#3668 is finally compiling again.