@@ -110,7 +110,7 @@ irMain tm = do i <- ir tm
110110mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
111111mkDecls t used
112112 = do i <- getIState
113− let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
113+ let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
114114 decls <- mapM build ds
115115 return decls
116116
@@ -390,6 +390,33 @@ instance ToIR SC where
390390 ir' (ProjCase tm alt) = do tm' <- ir tm
391391 alt' <- mkIRAlt tm' alt
392392 return $ LCase tm' [alt']
393+
394+ -- This is important for runtime because sometimes we case on irrelevant data:
395+ --
396+ -- case {foo} of
397+ -- SingleConstructor x y => ... x, y never used ...
398+ --
399+ -- In the example above, {foo} will most probably have been erased
400+ -- so this vain projection would make the resulting program segfault.
401+ --
402+ -- Hence, we check whether the variables are used at all
403+ -- and erase the casesplit if they are not.
404+ ir' (Case n [alt]) = do
405+ alt' <- mkIRAlt (LV (Glob n)) alt
406+ return $ case namesBoundIn alt' `usedIn` subexpr alt' of
407+ [] -> subexpr alt' -- strip the unused top-most case
408+ _ -> LCase (LV (Glob n)) [alt']
409+ where
410+ namesBoundIn :: LAlt -> [Name]
411+ namesBoundIn (LConCase cn i ns sc) = ns
412+ namesBoundIn (LConstCase c sc) = []
413+ namesBoundIn (LDefaultCase sc) = []
414+
415+ subexpr :: LAlt -> LExp
416+ subexpr (LConCase _ _ _ e) = e
417+ subexpr (LConstCase _ e) = e
418+ subexpr (LDefaultCase e) = e
419+
393420 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
394421 return $ LCase (LV (Glob n)) alts'
395422 ir' ImpossibleCase = return LNothing