From 231291ee6b62815222b652c21cd17328b76aa00a Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Mon, 4 Sep 2023 20:10:06 -0700
Subject: [PATCH] [ fix ] consider nest when guessing scrutinee

---
 src/TTImp/Elab/Case.idr            |  4 +++-
 tests/Main.idr                     |  2 +-
 tests/idris2/case002/WhereData.idr | 11 +++++++++++
 tests/idris2/case002/expected      |  1 +
 tests/idris2/case002/run           |  3 +++
 5 files changed, 19 insertions(+), 2 deletions(-)
 create mode 100644 tests/idris2/case002/WhereData.idr
 create mode 100644 tests/idris2/case002/expected
 create mode 100755 tests/idris2/case002/run

diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr
index ba5e03f348..66502caf5f 100644
--- a/src/TTImp/Elab/Case.idr
+++ b/src/TTImp/Elab/Case.idr
@@ -460,7 +460,9 @@ checkCase rig elabinfo nest env fc opts scr scrty_in alts exp
         = case getFn x of
                IVar _ n =>
                   do defs <- get Ctxt
-                     [(n', (_, ty))] <- lookupTyName n (gamma defs)
+                     [(n', (_, ty))] <- do nested <- maybe (pure []) (\n => lookupTyName n (gamma defs))
+                                                      (join $ Builtin.fst <$> List.lookup n nest.names)
+                                           (nested ++) <$> lookupTyName n (gamma defs)
                          | _ => guessScrType xs
                      Just (tyn, tyty) <- getRetTy defs !(nf defs [] ty)
                          | _ => guessScrType xs
diff --git a/tests/Main.idr b/tests/Main.idr
index e30b721df2..d107963e48 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -47,7 +47,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
        "idiom001",
        "literals001",
        "dotted001",
-       "case001",
+       "case001", "case002",
        "rewrite001",
        "interpolation001", "interpolation002", "interpolation003",
        "interpolation004"]
diff --git a/tests/idris2/case002/WhereData.idr b/tests/idris2/case002/WhereData.idr
new file mode 100644
index 0000000000..a00d5444e8
--- /dev/null
+++ b/tests/idris2/case002/WhereData.idr
@@ -0,0 +1,11 @@
+module Main
+
+foo : Int -> Int
+foo x = case isLT of
+            Yes => x*2
+            No => x*4
+   where
+      data MyLT = Yes | No
+
+      isLT : MyLT
+      isLT = if x < 20 then Yes else No
diff --git a/tests/idris2/case002/expected b/tests/idris2/case002/expected
new file mode 100644
index 0000000000..28f2441181
--- /dev/null
+++ b/tests/idris2/case002/expected
@@ -0,0 +1 @@
+1/1: Building WhereData (WhereData.idr)
diff --git a/tests/idris2/case002/run b/tests/idris2/case002/run
new file mode 100755
index 0000000000..43b46c6ae5
--- /dev/null
+++ b/tests/idris2/case002/run
@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check WhereData.idr