git.iko.soy/Idris-dev
on master help sign in
Elaborator warnings are now correctly reported
commit998c8f4143aff9307397a52bd346e500084262ae authorJan de Muijnck-Hughes <jan.deMuijnck-Hughes@glasgow.ac.uk> dateWed 12 Jul 2017, 22:04 (9 years ago) parent9fb9d7f
4 files changed+13−9
compare with master
unifiedsplit
src/Idris/Elab/Utils.hs+6−5 test/basic009/expected+1−1 test/basic018/expected+4−2 test/regression002/expected+2−1
src/Idris/Elab/Utils.hs+6−5
@@ -449,9 +449,12 @@ displayWarnings est
449449 = mapM_ displayImpWarning (implicit_warnings est)
450450 where
451451 displayImpWarning :: (FC, Name) -> Idris ()
452− displayImpWarning (fc, n) =
453− iputStrLn $ show fc ++ ":WARNING: " ++ show (nsroot n) ++ " is bound as an implicit\n"
454− ++ "\tDid you mean to refer to " ++ show n ++ "?"
452+ displayImpWarning (fc, n) = do
453+ ist <- getIState
454+ let msg = show (nsroot n)
455+ ++ " is bound as an implicit\n"
456+ ++ "\tDid you mean to refer to " ++ show n ++ "?"
457+ iWarn fc (pprintErr ist (Msg msg))
455458
456459propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
457460propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)
@@ -767,5 +770,3 @@ isPlausible ist var env n ty
767770 collectConstraints env tcs t
768771 | (V i, _) <- unApply t = (Just (env !! i), tcs)
769772 | otherwise = (Nothing, tcs)
770−
771−
test/basic009/expected+1−1
@@ -1,5 +1,5 @@
11MAIN-PASS
2−Faulty.idr:6:9-12:WARNING: num is bound as an implicit
2+Faulty.idr:6:9-12:num is bound as an implicit
33 Did you mean to refer to A.num?
44Faulty.idr:7:7:When checking right hand side of fault with expected type
55 num = 0
test/basic018/expected+4−2
@@ -1,6 +1,8 @@
1−basic018.idr:7:12-17:WARNING: thing is bound as an implicit
1+basic018.idr:7:12-17:
2+thing is bound as an implicit
23 Did you mean to refer to Main.thing?
3−basic018.idr:12:8-13:WARNING: thing is bound as an implicit
4+basic018.idr:12:8-13:
5+thing is bound as an implicit
46 Did you mean to refer to Main.thing?
57basic018.idr:13:6:When checking right hand side of test with expected type
68 thing = S 41
test/regression002/expected+2−1
@@ -110,7 +110,8 @@ reg068.idr:1:6:Main.nat has a name which may be implicitly bound.
110110This is likely to lead to problems!
111111reg068.idr:2:6:Main.ze has a name which may be implicitly bound.
112112This is likely to lead to problems!
113−reg068.idr:2:8-11:WARNING: nat is bound as an implicit
113+reg068.idr:2:8-11:
114+nat is bound as an implicit
114115 Did you mean to refer to Main.nat?
115116reg068.idr:2:6:When checking constructor Main.ze:
116117Type level variable nat is not Main.nat