@@ -152,7 +152,7 @@ mkLDecl n (CaseOp ci _ _ _ pats cd)
152 return (declArgs [] (case_inlinable ci) n e)
152 return (declArgs [] (case_inlinable ci) n e)
154mkLDecl n (TyDecl (DCon tag arity) _) =
154mkLDecl 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
157mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
157mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
158mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
158mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
@@ -474,9 +474,11 @@ instance ToIR SC where
474-- return $ LDefaultCase
474-- return $ LDefaultCase
475-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
475-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
477− mkIRAlt _ (ConCase n t args rhs)
477+ mkIRAlt _ (ConCase n t args sc) = do
478− = do rhs' <- ir rhs
478+ sc' <- ir sc
479+ used <- maybe [] (map fst . usedpos) . lookupCtxtExact n . idris_callgraph <$> getIState
479− return $ LConCase (-1) n args rhs'
480+ return $ LConCase (-1) n [a | (i,a) <- zip [0..] args, i `elem` used] sc'
480 mkIRAlt _ (ConstCase x rhs)
482 mkIRAlt _ (ConstCase x rhs)
481 | matchable x
483 | matchable x
482 = do rhs' <- ir rhs
484 = do rhs' <- ir rhs