@@ -56,15 +56,16 @@ acyclic r cvs = checkCycle (fileFC "root") r [] 0 cvs
5656 = Error $ At fc UniverseError
5757 -- FIXME: Make informative
5858 -- 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
5961 -- if we reach a cycle but we're at the same universe level, it's
6062 -- fine, because they must all be equal, so stop.
6163 | inc == 0 && cv `elem` map fst path
6264 = return ()
63− | otherwise
65+ | otherwise
6466 = case M.lookup cv r of
6567 Nothing -> return ()
6668 Just cs -> mapM_ (next r ((cv, fc):path) inc) cs
6769
6870 next r path inc (ULT l x, fc) = check fc r path (inc + 1) x
6971 next r path inc (ULE l x, fc) = check fc r path inc x
70−