@@ -152,7 +152,7 @@ mkLDecl n (CaseOp ci _ _ _ pats cd)
152152 return (declArgs [] (case_inlinable ci) n e)
153153
154154mkLDecl n (TyDecl (DCon tag arity) _) =
155− LConstructor n tag . maybe arity (length . usedpos) . lookupCtxtExact n . idris_callgraph <$> getIState
155+ LConstructor n tag . maybe 0 (length . usedpos) . lookupCtxtExact n . idris_callgraph <$> getIState
156156
157157mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
158158mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
@@ -474,9 +474,11 @@ instance ToIR SC where
474474-- return $ LDefaultCase
475475-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
476476-- rhs')
477− mkIRAlt _ (ConCase n t args rhs)
478− = do rhs' <- ir rhs
479− return $ LConCase (-1) n args rhs'
477+ mkIRAlt _ (ConCase n t args sc) = do
478+ sc' <- ir sc
479+ used <- maybe [] (map fst . usedpos) . lookupCtxtExact n . idris_callgraph <$> getIState
480+ return $ LConCase (-1) n [a | (i,a) <- zip [0..] args, i `elem` used] sc'
481+
480482 mkIRAlt _ (ConstCase x rhs)
481483 | matchable x
482484 = do rhs' <- ir rhs