@@ -110,7 +110,7 @@ irMain tm = do i <- ir tm
110mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
110mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
111mkDecls t used
111mkDecls t used
112 = do i <- getIState
112 = 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)
114 decls <- mapM build ds
114 decls <- mapM build ds
115 return decls
115 return decls
@@ -390,6 +390,33 @@ instance ToIR SC where
390 ir' (ProjCase tm alt) = do tm' <- ir tm
390 ir' (ProjCase tm alt) = do tm' <- ir tm
391 alt' <- mkIRAlt tm' alt
391 alt' <- mkIRAlt tm' alt
392 return $ LCase tm' [alt']
392 return $ LCase tm' [alt']
394+ -- This is important for runtime because sometimes we case on irrelevant data:
397+ -- SingleConstructor x y => ... x, y never used ...
399+ -- In the example above, {foo} will most probably have been erased
400+ -- so this vain projection would make the resulting program segfault.
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']
410+ namesBoundIn :: LAlt -> [Name]
411+ namesBoundIn (LConCase cn i ns sc) = ns
412+ namesBoundIn (LConstCase c sc) = []
413+ namesBoundIn (LDefaultCase sc) = []
415+ subexpr :: LAlt -> LExp
416+ subexpr (LConCase _ _ _ e) = e
417+ subexpr (LConstCase _ e) = e
418+ subexpr (LDefaultCase e) = e
393 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
420 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
394 return $ LCase (LV (Glob n)) alts'
421 return $ LCase (LV (Glob n)) alts'
395 ir' ImpossibleCase = return LNothing
422 ir' ImpossibleCase = return LNothing