fix: support Eq.recOn in the new compiler (#8602)

This PR adds support to the new compiler for `Eq.recOn` (which is
supported by the old compiler but missing a test).

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -704,7 +704,7 @@ where
         visitQuotLift e
       else if declName == ``Quot.mk then
         visitCtor 3 e
-      else if declName == ``Eq.casesOn || declName == ``Eq.rec || declName == ``Eq.ndrec then
+      else if declName == ``Eq.casesOn || declName == ``Eq.rec || declName == ``Eq.recOn || declName == ``Eq.ndrec then
         visitEqRec e
       else if declName == ``HEq.casesOn || declName == ``HEq.rec || declName == ``HEq.ndrec then
         visitHEqRec e

tests/lean/run/eqRecursors.lean

@@ -0,0 +1,4 @@
+def castRec {α : Type u} {m n : Nat} (h : m = n) (v : Vector α m) : Vector α n := Eq.rec v h
+def castNdrec {α : Type u} {m n : Nat} (h : m = n) (v : Vector α m) : Vector α n := Eq.ndrec v h
+def castRecOn {α : Type u} {m n : Nat} (h : m = n) (v : Vector α m) : Vector α n := Eq.recOn h v
+def castCasesOn {α : Type u} {m n : Nat} (h : m = n) (v : Vector α m) : Vector α n := Eq.casesOn h v