on master help sign in
universe inconsistency errors can originate from two places. make the error message consistent between these two.
752174fOzgur Akgun
src/Idris/Core/Constraints.hs+5−7
@@ -167,13 +167,11 @@ solve maxUniverseLevel ucs =
167 doms <- gets domainStore
167 doms <- gets domainStore
168 let (oldDom@(Domain _ upper), suspects) = doms M.! Var var
168 let (oldDom@(Domain _ upper), suspects) = doms M.! Var var
169 let newDom = Domain lower upper
169 let newDom = Domain lower upper
170− when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines
170+ when (wipeOut newDom) $
171− $ "Universe inconsistency."
171+ lift $ Error $
172− : ("Working on: " ++ show (UVar var))
172+ UniverseError (ufc suspect) (UVar var)
173− : ("Old domain: " ++ show oldDom)
173+ (asPair oldDom) (asPair newDom)
174− : ("New domain: " ++ show newDom)
175− : "Involved constraints: "
176− : map (("\t"++) . show) (suspect : S.toList suspects)
174+ (suspect : S.toList suspects)
177 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
175 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
178 addToQueueLHS (uconstraint suspect) (Var var)
176 addToQueueLHS (uconstraint suspect) (Var var)
179 updateLowerBoundOf _ UVal{} _ = return ()
177 updateLowerBoundOf _ UVal{} _ = return ()