git.iko.soy/Idris-dev
on master help sign in
Add application context to all error messages

This makes it easier to find errors. It will also enable improved error reflection soon.

commit57c3ffcdd0de36d40903e536f16109b6519bdef4 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 22 Mar 2014, 10:01 (13 years ago) parent60f7427
6 files changed+23−7
compare with master
unifiedsplit
src/Idris/Core/Elaborate.hs+4 src/Idris/Core/TT.hs+1 src/Idris/Delaborate.hs+10−2 test/basic009/expected+2−1 test/error004/expected+4−2 test/reg034/expected+2−2
src/Idris/Core/Elaborate.hs+4
@@ -167,6 +167,10 @@ done_elaborating_app :: Name -> Elab' aux ()
167167done_elaborating_app f = updatePS (doneElaboratingAppPS f)
168168done_elaborating_arg :: Name -> Name -> Elab' aux ()
169169done_elaborating_arg f a = updatePS (doneElaboratingArgPS f a)
170+elaborating_app :: Elab' aux [(FC, Name, Name)]
171+elaborating_app = do ES (ps, _) _ _ <- get
172+ return $ map (\ (FailContext x y z) -> (x, y, z))
173+ (while_elaborating ps)
170174
171175-- Some handy gadgets for pulling out bits of state
172176
src/Idris/Core/TT.hs+1
@@ -198,6 +198,7 @@ instance Show Err where
198198 show (At f e) = show f ++ ":" ++ show e
199199 show (ElaboratingArg f x prev e) = "Elaborating " ++ show f ++ " arg " ++
200200 show x ++ ": " ++ show e
201+ show (Elaborating what n e) = "Elaborating " ++ what ++ show n ++ ":" ++ show e
201202 show _ = "Error"
202203
203204instance Pretty Err OutputAnnotation where
src/Idris/Delaborate.hs+10−2
@@ -221,11 +221,19 @@ pprintErr' i (ElaboratingArg f x _ e)
221221 | isUN x =
222222 text "When elaborating argument" <+>
223223 annotate (AnnBoundName x False) (text (showbasic x)) <+> --TODO check plicity
224− text "to function" <+> annName f <> colon <>
224+ text "to" <+> whatIsName <> annName f <> colon <>
225225 indented (pprintErr' i e)
226226 | otherwise =
227− text "When elaborating an application of function" <+>
227+ text "When elaborating an application of" <+> whatIsName <>
228228 annName f <> colon <> indented (pprintErr' i e)
229+ where whatIsName = let ctxt = tt_ctxt i
230+ in if isTConName f ctxt
231+ then text "type constructor" <> space
232+ else if isConName f ctxt
233+ then text "constructor" <> space
234+ else if isFnName f ctxt
235+ then text "function" <> space
236+ else empty
229237pprintErr' i (ProviderError msg) = text ("Type provider error: " ++ msg)
230238pprintErr' i (LoadingFailed fn e) = text "Loading" <+> text fn <+> text "failed:" <+> pprintErr' i e
231239pprintErr' i (ReflectionError parts orig) =
test/basic009/expected+2−1
@@ -1,4 +1,5 @@
11MAIN-PASS
22Faulty.idr:6:7:When elaborating type of Faulty.fault:
3−Can't disambiguate name: A.num, B.C.num
3+When elaborating an application of type constructor =:
4+ Can't disambiguate name: A.num, B.C.num
45Multiple.idr:3:1:import alias not unique: "X"
test/error004/expected+4−2
@@ -1,4 +1,6 @@
11FunErrTest.idr:33:10:When elaborating right hand side of badCadr1:
2−Could not prove that [] has at least two elements.
2+When elaborating argument cons1 to function FunErrTest.cadr:
3+ Could not prove that [] has at least two elements.
34FunErrTest.idr:36:10:When elaborating right hand side of badCadr2:
4−Could not prove that tail [(fromInteger 1)] refl has at least two elements.
5+When elaborating argument cons2 to function FunErrTest.cadr:
6+ Could not prove that tail [(fromInteger 1)] refl has at least two elements.
test/reg034/expected+2−2
@@ -1,5 +1,5 @@
11reg034.idr:6:5:When elaborating left hand side of bar:
2−When elaborating an application of function main.bar:
2+When elaborating an application of main.bar:
33 Can't unify
44 x = x
55 with
@@ -11,7 +11,7 @@ When elaborating an application of function main.bar:
1111 with
1212 length xs
1313reg034.idr:9:5:When elaborating left hand side of foo:
14−When elaborating an application of function main.foo:
14+When elaborating an application of main.foo:
1515 Can't unify
1616 x = x
1717 with