@@ -569,8 +569,8 @@ checkMP ist i mp = if i > 0
569569 x -> error (show x)
570570 | [TyDecl (TCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)
571571 = Total []
572− tryPath desc path (e@(f, []) : es) arg
573− | e `elem` es = Partial (Mutual [f])
572+ tryPath desc path (e@(f, args) : es) arg
573+ | e `elem` es && allNothing args = Partial (Mutual [f])
574574 tryPath desc path (e@(f, nextargs) : es) arg
575575 | Just d <- lookup e path
576576 = if desc > 0
@@ -587,7 +587,7 @@ checkMP ist i mp = if i > 0
587587 -- rest definitely terminates without
588588 -- any cycles with route so far,
589589 -- 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)
591591 [0..length nextargs - 1]) of
592592 Total _ -> return Unchecked
593593 x -> return x
@@ -607,6 +607,8 @@ checkMP ist i mp = if i > 0
607607 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
608608 | otherwise = Unchecked
609609
610+allNothing xs = null (collapseNothing (zip xs [0..]))
611+
610612collapseNothing ((Nothing, _) : xs)
611613 = filter (\ (x, _) -> case x of
612614 Nothing -> False