Add fc to universe error message
commit928429414243451c32c19a99036af8b3bcd90987
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSat 21 Mar 2015, 16:02 (12 years ago)
parent09ff7ed
src/Idris/Core/Constraints.hs+1−1
@@ -127,7 +127,7 @@ solve maxUniverseLevel inpConstraints =
127127 updateDomainOf suspect (UVar var) newDom = do
128128 doms <- gets domainStore
129129 let (oldDom, suspects) = doms M.! Var var
130− when (wipeOut newDom) $ lift $ Error $ Msg $ unlines
130+ when (wipeOut newDom) $ lift $ Error $ At (snd suspect) $ Msg $ unlines
131131 $ "Universe inconsistency."
132132 : ("Working on: " ++ show (UVar var))
133133 : ("Old domain: " ++ show oldDom)
test/error001/expected+10−1
@@ -1 +1,10 @@
1−test002.idr:5:6:Universe inconsistency
1+test002.idr:5:6:Universe inconsistency.
2+Working on: f2
3+Old domain: Domain 7 7
4+New domain: Domain 7 6
5+Involved constraints:
6+ (f2 <= i1,test002.idr:5:6)
7+ (e2 < f2,test002.idr:5:6)
8+ (j1 <= f2,test002.idr:5:6)
9+ (f2 <= i1,test002.idr:5:6)
10+