Treat nested names the same as elsewhere

idris-lang · Sep 11, 2023 · 64bc185 · 64bc185
1 parent 6f3cde8
commit 64bc185
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr
@@ -460,9 +460,10 @@ checkCase rig elabinfo nest env fc opts scr scrty_in alts exp
         = case getFn x of
                IVar _ n =>
                   do defs <- get Ctxt
-                     [(n', (_, ty))] <- do nested <- maybe (pure []) (\n => lookupTyName n (gamma defs))
-                                                      (join $ Builtin.fst <$> List.lookup n nest.names)
-                                           (nested ++) <$> lookupTyName n (gamma defs)
+                     let n' = case lookup n (names nest) of
+                                Just (Just n', _) => n'
+                                _ => n
+                     [(_, (_, ty))] <- lookupTyName n' (gamma defs)
                          | _ => guessScrType xs
                      Just (tyn, tyty) <- getRetTy defs !(nf defs [] ty)
                          | _ => guessScrType xs