@@ -12,8 +12,11 @@ import qualified Data.Set as S
1212-- | Check that a list of universe constraints can be satisfied.
1313ucheck :: [(UConstraint, FC)] -> TC ()
1414ucheck = void . solve 10 . filter (not . ignore)
15− where ignore (c,_) = any (== Var (-1)) (varsIn c)
16− -- TODO: remove the ignore when Idris.Core.Binary:598
15+ where
16+ -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with
17+ ignore (c,_) | any (== Var (-1)) (varsIn c) = True
18+ ignore (ULE a b, _) = a == b
19+ ignore _ = False
1720
1821newtype Var = Var Int
1922 deriving (Eq, Ord, Show)