From 5165c79b671f0ae5cd300993561b66425d9abbb7 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 15 Jul 2023 17:05:05 -0700
Subject: [PATCH] [ fix ] Ensure local defs with no claim are local

---
 src/TTImp/TTImp.idr                 |  1 +
 tests/Main.idr                      |  2 +-
 tests/idris2/basic070/Issue2592.idr |  4 ++++
 tests/idris2/basic070/Issue2593.idr |  6 ++++++
 tests/idris2/basic070/Issue2782.idr |  9 +++++++++
 tests/idris2/basic070/Issue3016.idr |  9 +++++++++
 tests/idris2/basic070/expected      | 14 ++++++++++++++
 tests/idris2/basic070/run           |  6 ++++++
 8 files changed, 50 insertions(+), 1 deletion(-)
 create mode 100644 tests/idris2/basic070/Issue2592.idr
 create mode 100644 tests/idris2/basic070/Issue2593.idr
 create mode 100644 tests/idris2/basic070/Issue2782.idr
 create mode 100644 tests/idris2/basic070/Issue3016.idr
 create mode 100644 tests/idris2/basic070/expected
 create mode 100755 tests/idris2/basic070/run

diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr
index 6e50dab449..bd57502729 100644
--- a/src/TTImp/TTImp.idr
+++ b/src/TTImp/TTImp.idr
@@ -790,6 +790,7 @@ definedInBlock ns decls =
 
     defName : Namespace -> ImpDecl -> List Name
     defName ns (IClaim _ _ _ _ ty) = [expandNS ns (getName ty)]
+    defName ns (IDef _ nm _) = [expandNS ns nm]
     defName ns (IData _ _ _ (MkImpData _ n _ _ cons))
         = expandNS ns n :: map (expandNS ns) (map getName cons)
     defName ns (IData _ _ _ (MkImpLater _ n _)) = [expandNS ns n]
diff --git a/tests/Main.idr b/tests/Main.idr
index 9888cafcc5..ae109ea3cc 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -42,7 +42,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
        "basic051", "basic052", "basic053", "basic054", "basic055",
        "basic056", "basic057", "basic058", "basic059", "basic060",
        "basic061", "basic062", "basic063", "basic064", "basic065",
-       "basic066", "basic067", "basic068", "basic069",
+       "basic066", "basic067", "basic068", "basic069", "basic070",
        "idiom001",
        "dotted001",
        "rewrite001",
diff --git a/tests/idris2/basic070/Issue2592.idr b/tests/idris2/basic070/Issue2592.idr
new file mode 100644
index 0000000000..2e07c2b91f
--- /dev/null
+++ b/tests/idris2/basic070/Issue2592.idr
@@ -0,0 +1,4 @@
+bar = 3
+ where wat = 2
+baz = 3
+ where wat = 2
diff --git a/tests/idris2/basic070/Issue2593.idr b/tests/idris2/basic070/Issue2593.idr
new file mode 100644
index 0000000000..93d3a14de7
--- /dev/null
+++ b/tests/idris2/basic070/Issue2593.idr
@@ -0,0 +1,6 @@
+two: Nat
+two = 2
+
+bar: a -> a
+bar x = x where
+ wat = two
diff --git a/tests/idris2/basic070/Issue2782.idr b/tests/idris2/basic070/Issue2782.idr
new file mode 100644
index 0000000000..9271e72011
--- /dev/null
+++ b/tests/idris2/basic070/Issue2782.idr
@@ -0,0 +1,9 @@
+foo : Integer
+foo =
+  let z : Int
+      z = 1
+      y = 1
+  in y
+
+fee : Integer
+fee = y
diff --git a/tests/idris2/basic070/Issue3016.idr b/tests/idris2/basic070/Issue3016.idr
new file mode 100644
index 0000000000..1907ba3781
--- /dev/null
+++ b/tests/idris2/basic070/Issue3016.idr
@@ -0,0 +1,9 @@
+import Data.String
+
+test str = len
+  where
+    xs = words str
+    len = length xs
+
+parameters (n : Nat) (strs : List String)
+  len = List.length strs
diff --git a/tests/idris2/basic070/expected b/tests/idris2/basic070/expected
new file mode 100644
index 0000000000..90af640b73
--- /dev/null
+++ b/tests/idris2/basic070/expected
@@ -0,0 +1,14 @@
+1/1: Building Issue3016 (Issue3016.idr)
+1/1: Building Issue2782 (Issue2782.idr)
+Error: While processing right hand side of fee. Undefined name y. 
+
+Issue2782:9:7--9:8
+ 5 |       y = 1
+ 6 |   in y
+ 7 | 
+ 8 | fee : Integer
+ 9 | fee = y
+           ^
+
+1/1: Building Issue2592 (Issue2592.idr)
+1/1: Building Issue2593 (Issue2593.idr)
diff --git a/tests/idris2/basic070/run b/tests/idris2/basic070/run
new file mode 100755
index 0000000000..59c5abe156
--- /dev/null
+++ b/tests/idris2/basic070/run
@@ -0,0 +1,6 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check Issue3016.idr
+$1 --no-color --console-width 0 --no-banner --check Issue2782.idr
+$1 --no-color --console-width 0 --no-banner --check Issue2592.idr
+$1 --no-color --console-width 0 --no-banner --check Issue2593.idr