998c8f4 · Idris-dev · git.iko.soy

src/Idris/Elab/Utils.hs+6−5

compare with master

unifiedsplit

@@ -449,9 +449,12 @@ displayWarnings est

449 = mapM_ displayImpWarning (implicit_warnings est)

450 where

451 displayImpWarning :: (FC, Name) -> Idris ()

452− displayImpWarning (fc, n) =

452+ displayImpWarning (fc, n) = do

453+ ist <- getIState

454+ let msg = show (nsroot n)

453− iputStrLn $ show fc ++ ":WARNING: " ++ show (nsroot n) ++ " is bound as an implicit\n"

455+ ++ " is bound as an implicit\n"

454− ++ "\tDid you mean to refer to " ++ show n ++ "?"

456+ ++ "\tDid you mean to refer to " ++ show n ++ "?"

457+ iWarn fc (pprintErr ist (Msg msg))

455

458

456propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm

459propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm

457propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)

460propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)

@@ -767,5 +770,3 @@ isPlausible ist var env n ty

767 collectConstraints env tcs t

770 collectConstraints env tcs t

768 | (V i, _) <- unApply t = (Just (env !! i), tcs)

771 | (V i, _) <- unApply t = (Just (env !! i), tcs)

769 | otherwise = (Nothing, tcs)

772 | otherwise = (Nothing, tcs)

770−

771−

test/basic009/expected+1−1

@@ -1,5 +1,5 @@

1MAIN-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

3 Did you mean to refer to A.num?

4Faulty.idr:7:7:When checking right hand side of fault with expected type

5 num = 0

test/basic018/expected+4−2

@@ -1,6 +1,8 @@

1+basic018.idr:7:12-17:

1−basic018.idr:7:12-17:WARNING: thing is bound as an implicit

2+thing is bound as an implicit

2 Did you mean to refer to Main.thing?

3 Did you mean to refer to Main.thing?

4+basic018.idr:12:8-13:

3−basic018.idr:12:8-13:WARNING: thing is bound as an implicit

5+thing is bound as an implicit

4 Did you mean to refer to Main.thing?

6 Did you mean to refer to Main.thing?

5basic018.idr:13:6:When checking right hand side of test with expected type

7basic018.idr:13:6:When checking right hand side of test with expected type

6 thing = S 41

8 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.

110This is likely to lead to problems!

111reg068.idr:2:6:Main.ze has a name which may be implicitly bound.

112This is likely to lead to problems!

113+reg068.idr:2:8-11:

113−reg068.idr:2:8-11:WARNING: nat is bound as an implicit

114+nat is bound as an implicit

114 Did you mean to refer to Main.nat?

115 Did you mean to refer to Main.nat?

115reg068.idr:2:6:When checking constructor Main.ze:

116reg068.idr:2:6:When checking constructor Main.ze:

116Type level variable nat is not Main.nat

117Type level variable nat is not Main.nat