LinearAlgebra.Determinant !4#3694

Stream: mathlib4

[Scott Morrison]

LinearAlgebra.Determinant !4#3694 is experiencing a strange interaction between the simpNF linter and etaExperiment:

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
-- Mathlib.LinearAlgebra.Determinant
#check LinearEquiv.det_symm.{u_2, u_1} /- LINTER FAILED:
simplify fails on left-hand side:
application type mismatch
  @LinearEquiv R R Ring.toSemiring Ring.toSemiring (RingHom.id R)
argument
  RingHom.id R
has type
  @RingHom R R NonAssocRing.toNonAssocSemiring NonAssocRing.toNonAssocSemiring : Type u_1
but is expected to have type
  @RingHom R R Semiring.toNonAssocSemiring Semiring.toNonAssocSemiring : Type u_1 -/

Does anyone have an idea what we should be doing here? Do we need to turn on etaExperiment during linting?!

[Jeremy Tan]

Scott Morrison said:
Do we need to turn on etaExperiment during linting?!

Yes, there should be a way to tell the linter that eta should be used for a particular simp lemma

[Eric Wieser]

Is the linter re-elaborating the syntax somehow? The error message is very strange.

[Scott Morrison]

Okay, we've ended up merged this with a @[nolint] to dodge this issue. :-(

[Jeremy Tan]

I am both surprised and concerned that you didn't investigate this further, even if you deem nolint simpNF good enough for now

[Eric Wieser]

The idea in "good enough for now" is that it removes the urgency to investigate the issue!

[Scott Morrison]

No, it's not re-elaborating anything. It's simp itself (run by the linter, with etaExperiment turned off) that is constructing a term that doesn't typecheck without etaExperiment.

[Scott Morrison]

I'm not really sure what more there is to investigate here.

[Scott Morrison]

There are many more failures of this kind at https://github.com/leanprover-community/mathlib4/actions/runs/4864919793/jobs/8674551592?pr=3651

[Jeremy Tan]

Which is why I said, it would be desirable to have a simp option to use etaExperiment when type-checking the constructed term