@@ -514,6 +514,7 @@ irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])
515-- Hence, we check whether the variables are used at all
515-- Hence, we check whether the variables are used at all
516-- and erase the casesplit if they are not.
516-- and erase the casesplit if they are not.
517irSC vs (Case n [alt]) = do
518irSC vs (Case n [alt]) = do
518 replacement <- case alt of
519 replacement <- case alt of
519 ConCase cn a ns sc -> do
520 ConCase cn a ns sc -> do
@@ -542,7 +543,31 @@ irSC vs (Case n [alt]) = do
542 subexpr (LConstCase _ e) = e
543 subexpr (LConstCase _ e) = e
543 subexpr (LDefaultCase e) = e
544 subexpr (LDefaultCase e) = e
546+-- When we have a non-singleton case-tree of the form
552+-- and C is detaggable (= the only constructor of the family),
553+-- something has gone wrong.
555+-- Especially, if C is newtype-optimisable, we will miss this newtype
556+-- transformation and the resulting code will probably segfault.
558+-- Therefore we first have to check that all alts here are non-trivial.
560+irSC vs sc@(Case n alts) = do
561+ goneWrong <- or <$> mapM isDetaggable alts
563+ $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
545−irSC vs (Case n alts) = LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
566+ LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
568+ isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
569+ isDetaggable _ = return False
546irSC vs ImpossibleCase = return LNothing
571irSC vs ImpossibleCase = return LNothing
548irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
573irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt