@@ -56,15 +56,16 @@ acyclic r cvs = checkCycle (fileFC "root") r [] 0 cvs
56 = Error $ At fc UniverseError
56 = Error $ At fc UniverseError
57 -- FIXME: Make informative
57 -- FIXME: Make informative
58 -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))
58 -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))
59+ -- Issue #1725 on the issue tracker.
60+ -- https://github.com/idris-lang/Idris-dev/issues/1725
59 -- if we reach a cycle but we're at the same universe level, it's
61 -- if we reach a cycle but we're at the same universe level, it's
60 -- fine, because they must all be equal, so stop.
62 -- fine, because they must all be equal, so stop.
61 | inc == 0 && cv `elem` map fst path
63 | inc == 0 && cv `elem` map fst path
62 = return ()
64 = return ()
63− | otherwise
65+ | otherwise
64 = case M.lookup cv r of
66 = case M.lookup cv r of
65 Nothing -> return ()
67 Nothing -> return ()
66 Just cs -> mapM_ (next r ((cv, fc):path) inc) cs
68 Just cs -> mapM_ (next r ((cv, fc):path) inc) cs
68 next r path inc (ULT l x, fc) = check fc r path (inc + 1) x
70 next r path inc (ULT l x, fc) = check fc r path (inc + 1) x
69 next r path inc (ULE l x, fc) = check fc r path inc x
71 next r path inc (ULE l x, fc) = check fc r path inc x