From fea6fef4c63ad27fdb93119c811729a9efaf6fb9 Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@ens-paris-saclay.fr>
Date: Mon, 4 Mar 2024 19:00:54 +0100
Subject: [PATCH] feat: add `autoPromoteIndices` option

---
 src/Lean/Elab/Inductive.lean |  9 ++++++++-
 tests/lean/run/3458_1.lean   | 27 +++++++++++++++++++++++++++
 2 files changed, 35 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/3458_1.lean

diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index a78e39c54a39..b9d9242c9850 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -25,6 +25,11 @@ open Meta
 builtin_initialize
   registerTraceClass `Elab.inductive
 
+register_builtin_option inductive.autoPromoteIndices : Bool := {
+    defValue := true
+    descr    := "Promote indices to parameters in inductive types whenever possible."
+  }
+
 def checkValidInductiveModifier [Monad m] [MonadError m] (modifiers : Modifiers) : m Unit := do
   if modifiers.isNoncomputable then
     throwError "invalid use of 'noncomputable' in inductive declaration"
@@ -714,10 +719,12 @@ private def isDomainDefEq (arrowType : Expr) (type : Expr) : MetaM Bool := do
   Convert fixed indices to parameters.
 -/
 private partial def fixedIndicesToParams (numParams : Nat) (indTypes : Array InductiveType) (indFVars : Array Expr) : MetaM Nat := do
+  if !inductive.autoPromoteIndices.get (← getOptions) then
+    return numParams
   let masks ← indTypes.mapM (computeFixedIndexBitMask numParams · indFVars)
+  trace[Elab.inductive] "masks: {masks}"
   if masks.all fun mask => !mask.contains true then
     return numParams
-  trace[Elab.inductive] "masks: {masks}"
   -- We process just a non-fixed prefix of the indices for now. Reason: we don't want to change the order.
   -- TODO: extend it in the future. For example, it should be reasonable to change
   -- the order of indices generated by the auto implicit feature.
diff --git a/tests/lean/run/3458_1.lean b/tests/lean/run/3458_1.lean
new file mode 100644
index 000000000000..774848cb0d8c
--- /dev/null
+++ b/tests/lean/run/3458_1.lean
@@ -0,0 +1,27 @@
+/- Ensure that turning off `autoPromoteIndices` stops indices
+   from being promoted to parameters in inductive types.
+   Because free variables aren't allowed in parameters of nested appearances,
+   it is sometimes desirable for fixed indices to not be promoted to parameters.
+   See `IInterp`.
+   -/
+
+set_option autoImplicit false
+universe u v w
+
+structure ISignature (I : Type u) : Type (max u v + 1) where
+  symbols : I → Type v
+  indices : {i : I} → symbols i → List I
+
+inductive All {I : Type u} (P : I → Type v) : List I → Type (max u v) where
+  | nil : All P []
+  | cons {x xs}: P x → All P xs → All P (x :: xs)
+
+set_option inductive.autoPromoteIndices false
+
+inductive IInterp {I} (ζ : ISignature.{u,v} I) (P : I → Type w) : I → Type (max u v w) where
+  | mk :{i : I} → (s : ζ.symbols i) → All P (ζ.indices s) → IInterp ζ P i
+
+notation:max "I⟦ " ζ " ⟧" => IInterp ζ
+
+inductive Iμ {I : Type u} (ζ : ISignature.{u,v} I) : I → Type (max u v) where
+  | mk : (i : I) → I⟦ ζ ⟧ (Iμ ζ) i → Iμ ζ i