Tentative, hacky fix for shadowing issue

Qpf/Macro/Data/Ind.lean

@@ -95,60 +95,73 @@ def seq [Coe α (TSyntax kx)] (f : α → TSyntax kx → m (TSyntax kx)) : List
 
 open Lean.Parser.Term in
 def generate_body (values : Array (Name × List RecursionForm)) : m $ TSyntax `Lean.Parser.Term.matchAlts := do
-  let deeper: (TSyntaxArray `Lean.Parser.Term.matchAlt) ← values.mapM fun ⟨name, form⟩ => do
+  let deeper: (TSyntaxArray `Lean.Parser.Term.matchAlt) ← values.mapM fun ⟨outerCase, form⟩ => do
     let rec_count := form.count .recursive
     let names ← listToEqLenNames form
+    -- TODO: this is not a good way to deal with names
+    --       but, for some unknowable reason, this fixes a shadowing
+    --       issue
+
+    let names : Array Ident := ⟨
+      names.toList.enum.map fun ⟨i, _⟩ =>
+        mkIdent <| Name.str (.anonymous) s!"_PRIVATE_ y {i}"
+    --                                      ^^^^^^^^^^^^^^^
+    -- HACK: notice how the variable name contains a space.
+    -- This is deliberate, to reduce the possibility of name collisions,
+    -- given that these names are unhygienic
+    ⟩
+    -- The following would be better, with fresh names,
+    -- but for some reason this causes the variable `p` to be renamed to something new, which will then give errors when we use `p` later on
+    -- let names : Array Ident ← names.mapM fun _ => do
+    --   mkFreshIdent .missing
+
     let recs := names.zip (form.toArray)
           |>.filter (·.snd == .recursive)
           |>.map Prod.fst
 
     let witnesses ← toEqLenNames recs
 
     let body : Term ← if 0 = rec_count
-      then `($(mkIdent name) $names*)
+      then `($(mkIdent outerCase) $names*)
       else
-        let name := mkIdent name
-
         let p := mkIdent `p
         let w := mkIdent `w
 
-        let cases ← values.mapM fun ⟨case, _⟩ =>
-          let case := mkIdent case
-          if case != name then
-            `(tactic| case $case:ident => contradiction)
+        let cases ← values.mapM fun ⟨innerCase, _⟩ => do
+          let innerCaseTag := mkIdent innerCase
+          if innerCase != outerCase then
+            `(tactic| case $innerCaseTag:ident => contradiction)
           else do
-            let split: Syntax.TSepArray `tactic "" := .ofElems $ ← names.mapM fun n =>
+            let split : Array (TSyntax `tactic) ← names.mapM fun n =>
               `(tactic|rcases $n:ident with ⟨_, $n:ident⟩)
-
             let injections ← listToEqLenNames form
 
-            `(tactic|case $name:ident $[$names:ident]* => {
-              extract_goal;
-              $split*
-
-              stop
-              injection $p with $injections*
-              subst $injections:ident*
-
-              exact $(← wrapIfNotSingle recs)
-            })
+            `(tactic|
+              case $innerCaseTag:ident $[$names:ident]* => (
+                $split:tactic*
+                injection $p:ident with $injections*
+                subst $injections:ident*
+                exact $(← wrapIfNotSingle recs)
+            ))
 
         trace[QPF] s!"count : {cases.size} {values.size}"
 
         let proofs ← wrapIfNotSingle witnesses
         let ty ← seq (fun a b => `($a ∧ $b)) (← recs.mapM fun x => `($motive $x)).toList
+        let outerCase := mkIdent outerCase
         `(have $proofs:term : $ty := by
             simp [$(mkIdent ``MvFunctor.LiftP):ident, $(mkIdent ``MvFunctor.map):ident] at $ih:ident
 
-            rcases $ih:ident with ⟨$w, $p⟩
+            rcases $ih:ident with ⟨$w:ident, $p:ident⟩
+            -- extract_goal;
 
             /- sorry -/
             cases $w:ident
-            $cases:tactic;*
-          $name $names* $witnesses*)
+            $cases:tactic*
+          $outerCase:ident $names* $witnesses*)
 
     `(matchAltExpr|
-      | .$(mkIdent name) $names*, $ih => $body
+      | .$(mkIdent outerCase) $names*, $ih => $body
     )
   let x ← `(matchAltExprs| $deeper:matchAlt* )
   pure ⟨x.raw⟩

Test/ListInduction.lean

@@ -0,0 +1,24 @@
+import Qpf.Macro.Data
+
+/-!
+## Test for induction principle generation
+-/
+
+namespace Test
+
+data QpfList α
+  | nil
+  | cons : α → QpfList α → QpfList α
+
+/-- info: 'Test.QpfList.ind' depends on axioms: [Quot.sound, propext] -/
+#guard_msgs in #print axioms QpfList.ind
+
+-- The following test might be a bit brittle.
+-- Feel free to remove if it gives too many false positives
+/--
+info: Test.QpfList.ind {α : Type} {motive : QpfList α → Prop} (nil : motive QpfList.nil)
+  (cons : ∀ (x : α) (x_1 : QpfList α), motive x_1 → motive (QpfList.cons x x_1)) (val✝ : QpfList α) : motive val✝
+-/
+#guard_msgs in #check QpfList.ind
+
+end Test