@@ -395,21 +395,44 @@ instance ToIR SC where
395395 alt' <- mkIRAlt tm' alt
396396 return $ LCase tm' [alt']
397397
398+ -- There are two transformations in this case:
399+ --
400+ -- 1. Newtype-case elimination:
401+ -- case {e0} of
402+ -- wrap({e1}) -> P({e1}) ==> P({e0})
403+ --
404+ -- This is important because newtyped constructors are compiled away entirely
405+ -- and we need to do that everywhere.
406+ --
407+ -- 2. Unused-case elimination:
408+ -- case {e0} of
409+ -- C(x,y) -> P[... x,y not used ...] ==> P
410+ --
398411 -- This is important for runtime because sometimes we case on irrelevant data:
399412 --
400− -- case {foo} of
401− -- SingleConstructor x y => ... x, y never used ...
402− --
403− -- In the example above, {foo} will most probably have been erased
404− -- so this vain projection would make the resulting program segfault.
413+ -- In the example above, {e0} will most probably have been erased
414+ -- so this vain projection would make the resulting program segfault
415+ -- because the code generator still emits a PROJECT(...) STG instruction.
405416 --
406417 -- Hence, we check whether the variables are used at all
407418 -- and erase the casesplit if they are not.
408419 ir' (Case n [alt]) = do
409− alt' <- mkIRAlt (LV (Glob n)) alt
410− return $ case namesBoundIn alt' `usedIn` subexpr alt' of
411− [] -> subexpr alt' -- strip the unused top-most case
412− _ -> LCase (LV (Glob n)) [alt']
420+ replacement <- case alt of
421+ ConCase cn a ns sc -> do
422+ detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState
423+ used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState
424+ if detag && length used == 1
425+ then return . Just $ substSC (ns !! head used) n sc
426+ else return Nothing
427+ _ -> return Nothing
428+
429+ case replacement of
430+ Just sc -> ir' sc
431+ _ -> do
432+ alt' <- mkIRAlt (LV (Glob n)) alt
433+ return $ case namesBoundIn alt' `usedIn` subexpr alt' of
434+ [] -> subexpr alt' -- strip the unused top-most case
435+ _ -> LCase (LV (Glob n)) [alt']
413436 where
414437 namesBoundIn :: LAlt -> [Name]
415438 namesBoundIn (LConCase cn i ns sc) = ns
@@ -421,6 +444,22 @@ instance ToIR SC where
421444 subexpr (LConstCase _ e) = e
422445 subexpr (LDefaultCase e) = e
423446
447+ substSC :: Name -> Name -> SC -> SC
448+ substSC n repl (Case n' alts)
449+ | n == n' = Case repl (map (substAlt n repl) alts)
450+ | otherwise = Case n' (map (substAlt n repl) alts)
451+ substSC n repl (STerm t) = STerm $ subst n (P Bound repl Erased) t
452+ substSC n repl sc = error $ "unsupported in substSC: " ++ show sc
453+
454+ substAlt :: Name -> Name -> CaseAlt -> CaseAlt
455+ substAlt n repl (ConCase cn a ns sc) = ConCase cn a ns (substSC n repl sc)
456+ substAlt n repl (FnCase fn ns sc) = FnCase fn ns (substSC n repl sc)
457+ substAlt n repl (ConstCase c sc) = ConstCase c (substSC n repl sc)
458+ substAlt n repl (SucCase n' sc)
459+ | n == n' = SucCase n (substSC n repl sc)
460+ | otherwise = SucCase n' (substSC n repl sc)
461+ substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)
462+
424463 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
425464 return $ LCase (LV (Glob n)) alts'
426465 ir' ImpossibleCase = return LNothing