on master help sign in
another tweak, do not register unary constraints
22914ecOzgur Akgun
src/Idris/Core/Constraints.hs+7−4
@@ -53,7 +53,9 @@ solve maxUniverseLevel inpConstraints =
53 constraints = M.map S.fromList $ M.fromListWith (++)
53 constraints = M.map S.fromList $ M.fromListWith (++)
54 [ (v, [(c,fc)])
54 [ (v, [(c,fc)])
55 | (c, fc) <- inpConstraints
55 | (c, fc) <- inpConstraints
56− , v <- varsIn c
56+ , let vars = varsIn c
57+ , length vars > 1 -- do not register unary constraints
58+ , v <- vars
57 ]
59 ]
58
60
59 -- | this is where the actual work is done.
61 -- | this is where the actual work is done.
@@ -122,9 +124,10 @@ solve maxUniverseLevel inpConstraints =
122
124
123 -- | add all constraints related to a variable.
125 -- | add all constraints related to a variable.
124 addToQueue :: MonadState SolverState m => Var -> m ()
126 addToQueue :: MonadState SolverState m => Var -> m ()
125− addToQueue var = do
127+ addToQueue var =
126− let cs = constraints M.! var
128+ case M.lookup var constraints of
129+ Nothing -> return ()
127− modify $ \ st -> st { queue = S.union cs (queue st) }
130+ Just cs -> modify $ \ st -> st { queue = S.union cs (queue st) }
128
131
129 -- | intersecting two domains, the resulting domain can be wiped out.
132 -- | intersecting two domains, the resulting domain can be wiped out.
130 domainIntersect :: (Int, Int) -> (Int, Int) -> (Int, Int)
133 domainIntersect :: (Int, Int) -> (Int, Int) -> (Int, Int)