@@ -522,10 +522,11 @@ mkMultiPaths ist path cg
522522 = concat (map extend cg)
523523 where extend (nextf, args)
524524 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
525− | otherwise
525+ | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
526526 = case lookupCtxt Nothing nextf (idris_callgraph ist) of
527527 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
528528 _ -> [ reverse ((nextf, args) : path) ]
529+ | otherwise = [ reverse ((nextf, args) : path) ]
529530
530531-- do (nextf, args) <- cg
531532-- if ((nextf, args) `elem` path)
@@ -571,7 +572,7 @@ checkMP ist i mp = if i > 0
571572 Total []
572573 else Partial (Mutual (map (fst . fst) path ++ [f]))
573574 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
574− let argspos = zip nextargs [0..] in
575+ let argspos = collapseNothing (zip nextargs [0..]) in
575576 collapse' Unchecked $
576577 do (a, pos) <- argspos
577578 case a of
@@ -595,10 +596,17 @@ checkMP ist i mp = if i > 0
595596 _ -> trace ("Shouldn't happen " ++ show e) $
596597 return (Partial Itself)
597598 else return Unchecked
598− | [Total _] <- lookupTotal f (tt_ctxt ist) = Unchecked
599+ | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
599600 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
600601 | otherwise = Unchecked
601602
603+collapseNothing ((Nothing, _) : xs)
604+ = filter (\ (x, _) -> case x of
605+ Nothing -> False
606+ _ -> True) xs
607+collapseNothing (x : xs) = x : collapseNothing xs
608+collapseNothing [] = []
609+
602610noPartial (Partial p : xs) = Partial p
603611noPartial (_ : xs) = noPartial xs
604612noPartial [] = Total []