@@ -151,16 +151,14 @@ mkLDecl n (CaseOp ci _ _ _ pats cd)
151151 do e <- ir (args, sc)
152152 return (declArgs [] (case_inlinable ci) n e)
153153
154−mkLDecl n (TyDecl (DCon t a) _) = do
155− cg <- idris_callgraph <$> getIState
156− return $ LConstructor n t a
157−{-
158− case lookupCtxt n cg of
159− [CGInfo _ _ _ _ [(i, _)]]
160− | -> iLOG $ "USED: " ++ show n ++ ": " ++ show used
161− [CGInfo _ _ _ _ used] -> iLOG $ "USED: " ++ show n ++ ": " ++ show used
162− _ -> return $ LConstructor n t a
163−-}
154+mkLDecl n (TyDecl (DCon tag arity) _) = do
155+ ist <- getIState
156+
157+ let realArity = case lookupCtxt n (idris_callgraph ist) of
158+ [CGInfo _ _ _ _ xs] -> length xs
159+ _ -> arity
160+
161+ return $ LConstructor n tag realArity
164162
165163mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
166164mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run