From 552f27f8131e86d5ca816417f5011b1814234f50 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Fri, 2 Sep 2022 10:49:19 +0100
Subject: [PATCH] [ fix #2640 ] Do not shadow function name during case split

---
 src/TTImp/Interactive/CaseSplit.idr         | 3 ++-
 tests/Main.idr                              | 2 +-
 tests/idris2/interactive044/SplitShadow.idr | 5 +++++
 tests/idris2/interactive044/expected        | 4 ++++
 tests/idris2/interactive044/input           | 3 +++
 tests/idris2/interactive044/run             | 8 ++++++++
 6 files changed, 23 insertions(+), 2 deletions(-)
 create mode 100644 tests/idris2/interactive044/SplitShadow.idr
 create mode 100644 tests/idris2/interactive044/expected
 create mode 100644 tests/idris2/interactive044/input
 create mode 100755 tests/idris2/interactive044/run

diff --git a/src/TTImp/Interactive/CaseSplit.idr b/src/TTImp/Interactive/CaseSplit.idr
index fdac038af..8861b6a66 100644
--- a/src/TTImp/Interactive/CaseSplit.idr
+++ b/src/TTImp/Interactive/CaseSplit.idr
@@ -119,7 +119,8 @@ findAllVars (Bind _ x (Let _ _ _ _) sc)
     = x :: findAllVars sc
 findAllVars (Bind _ x (PLet _ _ _ _) sc)
     = x :: findAllVars sc
-findAllVars _ = []
+-- #2640 also grab the name of the function being defined
+findAllVars t = toList (dropNS <$> getDefining t)
 
 export
 explicitlyBound : Defs -> NF [] -> Core (List Name)
diff --git a/tests/Main.idr b/tests/Main.idr
index b50138db1..ae991002b 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -101,7 +101,7 @@ idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing
        "interactive029", "interactive030", "interactive031", "interactive032",
        "interactive033", "interactive034", "interactive035", "interactive036",
        "interactive037", "interactive038", "interactive039", "interactive040",
-       "interactive041", "interactive042", "interactive043"]
+       "interactive041", "interactive042", "interactive043", "interactive044"]
 
 idrisTestsInterface : TestPool
 idrisTestsInterface = MkTestPool "Interface" [] Nothing
diff --git a/tests/idris2/interactive044/SplitShadow.idr b/tests/idris2/interactive044/SplitShadow.idr
new file mode 100644
index 000000000..bfa36fe98
--- /dev/null
+++ b/tests/idris2/interactive044/SplitShadow.idr
@@ -0,0 +1,5 @@
+data Chaos : Type where
+  Emerald : (colour : Nat) -> Chaos
+
+colour : Chaos -> ()
+colour c = ?colour_rhs_5
diff --git a/tests/idris2/interactive044/expected b/tests/idris2/interactive044/expected
new file mode 100644
index 000000000..60a990901
--- /dev/null
+++ b/tests/idris2/interactive044/expected
@@ -0,0 +1,4 @@
+1/1: Building SplitShadowGen (SplitShadowGen.idr)
+Main> colour (Emerald k) = ?colour_rhs_6
+Main> Loaded file SplitShadowGen.idr
+Main> Bye for now!
diff --git a/tests/idris2/interactive044/input b/tests/idris2/interactive044/input
new file mode 100644
index 000000000..2c8bb3c5e
--- /dev/null
+++ b/tests/idris2/interactive044/input
@@ -0,0 +1,3 @@
+:cs 5 7 c
+:r
+:q
diff --git a/tests/idris2/interactive044/run b/tests/idris2/interactive044/run
new file mode 100755
index 000000000..23952cc04
--- /dev/null
+++ b/tests/idris2/interactive044/run
@@ -0,0 +1,8 @@
+rm -rf build
+rm -f SplitShadowGen.idr
+
+cp SplitShadow.idr SplitShadowGen.idr
+
+$1 --no-color --console-width 0 --no-banner SplitShadowGen.idr < input
+
+rm SplitShadowGen.idr