[ fix ] consider nest when guessing scrutinee

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

tests/Main.idr

@@ -47,7 +47,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
        "idiom001",
        "literals001",
        "dotted001",
-       "case001",
+       "case001", "case002",
        "rewrite001",
        "interpolation001", "interpolation002", "interpolation003",
        "interpolation004"]

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

tests/idris2/case002/expected

@@ -0,0 +1 @@
+1/1: Building WhereData (WhereData.idr)

tests/idris2/case002/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check WhereData.idr