4d403c7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Improve error messages of the erasure checker.

4d403c7Matus Tejiscak13 years ago

src/Idris/Erasure.hs+7−2

@@ -7,6 +7,7 @@ import Idris.Core.CaseTree

7import Idris.Core.TT

8import Idris.Core.Evaluate

9import Idris.Primitives

10+import Idris.Error

11import Debug.Trace

12import Debug.Trace

12import System.IO.Unsafe

13import System.IO.Unsafe

@@ -102,8 +103,12 @@ performUsageAnalysis = do

102 checkAccessibility opt (n, reachable)

103 checkAccessibility opt (n, reachable)

103 | [Optimise col nt forc rec inaccessible] <- lookupCtxt n opt

104 | [Optimise col nt forc rec inaccessible] <- lookupCtxt n opt

104 = let collision = IS.fromList inaccessible `IS.intersection` reachable

105 = let collision = IS.fromList inaccessible `IS.intersection` reachable

105− in unless (IS.null collision)

106+ in unless (IS.null collision) . ifail . concat $

107+ [ "Erasure checker: in function "

108+ , show n

106− . fail $ "Erasure checker: inaccessible arguments reachable: " ++ show (IS.toList collision)

109+ , ": inaccessible arguments reachable: "

110+ , show (IS.toList collision)

111+ ]

107

112

108 | otherwise = return ()

113 | otherwise = return ()

109

114