@@ -514,6 +514,7 @@ irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])
514514--
515515-- Hence, we check whether the variables are used at all
516516-- and erase the casesplit if they are not.
517+--
517518irSC vs (Case n [alt]) = do
518519 replacement <- case alt of
519520 ConCase cn a ns sc -> do
@@ -542,7 +543,31 @@ irSC vs (Case n [alt]) = do
542543 subexpr (LConstCase _ e) = e
543544 subexpr (LDefaultCase e) = e
544545
545−irSC vs (Case n alts) = LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
546+-- When we have a non-singleton case-tree of the form
547+--
548+-- case {e0} of
549+-- C(x) => ...
550+-- ... => ...
551+--
552+-- and C is detaggable (= the only constructor of the family),
553+-- something has gone wrong.
554+--
555+-- Especially, if C is newtype-optimisable, we will miss this newtype
556+-- transformation and the resulting code will probably segfault.
557+--
558+-- Therefore we first have to check that all alts here are non-trivial.
559+--
560+irSC vs sc@(Case n alts) = do
561+ goneWrong <- or <$> mapM isDetaggable alts
562+ when goneWrong
563+ $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
564+
565+ -- everything okay
566+ LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
567+ where
568+ isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
569+ isDetaggable _ = return False
570+
546571irSC vs ImpossibleCase = return LNothing
547572
548573irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt