@@ -12,8 +12,11 @@ import qualified Data.Set as S
12-- | Check that a list of universe constraints can be satisfied.
12-- | Check that a list of universe constraints can be satisfied.
13ucheck :: [(UConstraint, FC)] -> TC ()
13ucheck :: [(UConstraint, FC)] -> TC ()
14ucheck = void . solve 10 . filter (not . ignore)
14ucheck = void . solve 10 . filter (not . ignore)
15− where ignore (c,_) = any (== Var (-1)) (varsIn c)
15+ where
16− -- TODO: remove the ignore when Idris.Core.Binary:598
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
18newtype Var = Var Int
21newtype Var = Var Int
19 deriving (Eq, Ord, Show)
22 deriving (Eq, Ord, Show)