fix: noConfusion shape info mistake

This PR fixes noConfusion compilation.

fixes #11610.

Author: nomeata

src/Lean/Meta/Constructions/NoConfusion.lean

@@ -262,9 +262,9 @@ def mkNoConfusionCoreImp (indName : Name) : MetaM Unit := do
     (value       := e)
     (hints       := ReducibilityHints.abbrev)))
   setReducibleAttribute declName
-  let arity := info.numParams + 1 + 3 * (info.numIndices + 1)
-  let lhsPos := info.numParams + 1 + info.numIndices
-  let rhsPos := info.numParams + 1 + info.numIndices + 1 + info.numIndices
+  let arity  := 1 + 3 * (info.numParams + info.numIndices + 1)
+  let lhsPos := 1 + info.numParams + info.numIndices
+  let rhsPos := 1 + 2 * info.numParams + 2 * info.numIndices + 1
   modifyEnv fun env => markNoConfusion env declName (.regular arity lhsPos rhsPos)
   modifyEnv fun env => addProtected env declName
 

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// Please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;

tests/lean/run/issue11610.lean

@@ -0,0 +1,25 @@
+import Lean
+
+variable {α β γ δ : Sort _}
+
+structure Prod' (α : Type u) (β : Type v) where
+  /--
+  Constructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.
+  -/
+  mk ::
+  /-- The first element of a pair. -/
+  fst : α
+  /-- The second element of a pair. -/
+  snd : β
+
+def mk.injArrow' {α : Type _} {β : Type _} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} :
+    Prod'.mk x₁ y₁ = Prod'.mk x₂ y₂ → ∀ ⦃P : Sort _⦄, (x₁ = x₂ → y₁ = y₂ → P) → P :=
+  fun h₁ _ h₂ ↦ Prod'.noConfusion rfl rfl (heq_of_eq h₁)
+    (fun h₃ h₄ ↦ h₂ (eq_of_heq h₃) (eq_of_heq h₄))
+
+-- Also for structures in Init:
+
+def mk.injArrow {α : Type _} {β : Type _} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} :
+    Prod.mk x₁ y₁ = Prod.mk x₂ y₂ → ∀ ⦃P : Sort _⦄, (x₁ = x₂ → y₁ = y₂ → P) → P :=
+  fun h₁ _ h₂ ↦ Prod.noConfusion rfl rfl (heq_of_eq h₁)
+    (fun h₃ h₄ ↦ h₂ (eq_of_heq h₃) (eq_of_heq h₄))