@@ -569,8 +569,8 @@ checkMP ist i mp = if i > 0
569 x -> error (show x)
569 x -> error (show x)
570 | [TyDecl (TCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)
570 | [TyDecl (TCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)
571 = Total []
571 = Total []
572− tryPath desc path (e@(f, []) : es) arg
572+ tryPath desc path (e@(f, args) : es) arg
573− | e `elem` es = Partial (Mutual [f])
573+ | e `elem` es && allNothing args = Partial (Mutual [f])
574 tryPath desc path (e@(f, nextargs) : es) arg
574 tryPath desc path (e@(f, nextargs) : es) arg
575 | Just d <- lookup e path
575 | Just d <- lookup e path
576 = if desc > 0
576 = if desc > 0
@@ -587,7 +587,7 @@ checkMP ist i mp = if i > 0
587 -- rest definitely terminates without
587 -- rest definitely terminates without
588 -- any cycles with route so far,
588 -- any cycles with route so far,
589 -- then we might yet be total
589 -- then we might yet be total
590− case collapse (map (tryPath (-10000) ((e, desc):path) es)
590+ case collapse (map (tryPath (-10000) ((e, 0):path) es)
591 [0..length nextargs - 1]) of
591 [0..length nextargs - 1]) of
592 Total _ -> return Unchecked
592 Total _ -> return Unchecked
593 x -> return x
593 x -> return x
@@ -607,6 +607,8 @@ checkMP ist i mp = if i > 0
607 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
607 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
608 | otherwise = Unchecked
608 | otherwise = Unchecked
610+allNothing xs = null (collapseNothing (zip xs [0..]))
610collapseNothing ((Nothing, _) : xs)
612collapseNothing ((Nothing, _) : xs)
611 = filter (\ (x, _) -> case x of
613 = filter (\ (x, _) -> case x of
612 Nothing -> False
614 Nothing -> False