ec13063 · Idris-dev · git.iko.soy

libs/prelude/Language/Reflection/Errors.idr+1−1

compare with master

unifiedsplit

@@ -29,7 +29,7 @@ data Err = Msg String

29 | NoTypeDecl TTName

30 | NotInjective TT TT TT

31 | CantResolve TT

32− | CantResolveAlts (List String)

32+ | CantResolveAlts (List TTName)

33 | IncompleteTerm TT

34 | UniverseError

35 | ProgramLineComment

src/Idris/ElabTerm.hs+1−1

@@ -2600,7 +2600,7 @@ reflectErr (NotInjective t1 t2 t3) =

2600reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2601reflectErr (CantResolveAlts ss) =

2602 raw_apply (Var $ reflErrName "CantResolveAlts")

2603− [rawList (Var $ (sUN "String")) (map Var ss)]

2603+ [rawList (Var $ reflm "TTName") (map reflectName ss)]

2604reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2605reflectErr UniverseError = Var $ reflErrName "UniverseError"

2606reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

src/Idris/ParseHelpers.hs+1−1

@@ -326,7 +326,7 @@ commentMarkers :: [String]

326commentMarkers = [ "--", "|||" ]

327

328invalidOperators :: [String]

329−invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%"]

329+invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]

330

331-- | Parses an operator

332operator :: MonadicParsing m => m String

test/reg050/expected+5−12

@@ -1,15 +1,8 @@

1−badbangop.idr:16:1:When elaborating right hand side of opUse:

1+./badbangop.idr:7:1: error: ! is

2−When elaborating an application of function Prelude.Monad.>>=:

2+ not a valid

3− Can't unify

3+ operator, expected: space

4− List Integer

4+(!) : List a -> Nat -> Maybe a

5− with

5+^

6− argTy -> retTy

7−

8− Specifically:

9− Can't unify

10− List

11− with

12− \{uv0} => argTy -> uv

13./baddoublebang.idr:6:28: error: unexpected

6./baddoublebang.idr:6:28: error: unexpected

14 Operator without known fixity:

7 Operator without known fixity:

15 !!, expected: space

8 !!, expected: space