@@ -779,13 +779,24 @@ mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
779779mkMultiPaths ist path [] = [reverse path]
780780mkMultiPaths ist path cg = concatMap extend cg
781781 where extend (nextf, args)
782− | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
782+ | (nextf, args) `inPath` path = [ reverse ((nextf, args) : path) ]
783783 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
784784 = case lookupCtxt nextf (idris_callgraph ist) of
785785 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
786786 _ -> [ reverse ((nextf, args) : path) ]
787787 | otherwise = [ reverse ((nextf, args) : path) ]
788788
789+ inPath :: SCGEntry -> [SCGEntry] -> Bool
790+ inPath f [] = False
791+ inPath f (g : gs) = smallerEq f g || f == g || inPath f gs
792+
793+ smallerEq :: SCGEntry -> SCGEntry -> Bool
794+ smallerEq (f, args) (g, args')
795+ = f == g && not (null (filter smallers args))
796+ && filter smallers args == filter smallers args'
797+ smallers (Just (_, Smaller)) = True
798+ smallers _ = False
799+
789800-- If any route along the multipath leads to infinite descent, we're fine.
790801-- Try a route beginning with every argument.
791802-- If we reach a point we've been to before, but with a smaller value,