TC solver introduces eta-expansions and fails

[Tragicus]

I found an instance where the typeclass solver fails at the very end of a run by trying to match some term with its eta-expansion.
The issue can be reproduced using the cstc branch of math-comp, which contains the relevant nix configuration. The failing line is l.2870 of ssralg.v (without the cast).