Better error reporting for unresolved type classes
commit3b1334102dee1fb6f0547021f7ef642bd7d02bc3
authorEdwin Brady <eb@cs.st-andrews.ac.uk>
dateWed 18 Jan 2012, 14:34 (15 years ago)
parent4c3fb9b
Makefile+4
@@ -14,6 +14,10 @@ configure: .PHONY
1414test : .PHONY
1515 make -C test
1616
17+relib: .PHONY
18+ make -C lib clean
19+ make -C lib BINDIR=../dist/build/idris
20+
1721linecount : .PHONY
1822 wc -l src/Idris/*.hs src/Core/*.hs
1923
idris.cabal+1−1
@@ -61,7 +61,7 @@ Executable idris
6161 Idris.Delaborate, Idris.Primitives, Idris.Imports,
6262 Idris.Compiler, Idris.Prover, Idris.ElabTerm,
6363 Idris.Coverage, Idris.IBC, Idris.Unlit,
64− Idris.DataOpts, Idris.Transforms,
64+ Idris.DataOpts, Idris.Transforms,
6565
6666 Paths_idris
6767
lib/prelude/strings.idr+1−1
@@ -21,7 +21,7 @@ strTail' x p = prim__strTail x
2121
2222strM : (x : String) -> StrM x
2323strM x with (choose (not (x == "")))
24− strM x | (Left p) = believe_me (StrCons (strHead' x p) (strTail' x p))
24+ strM x | (Left p) = believe_me $ StrCons (strHead' x p) (strTail' x p)
2525 strM x | (Right p) = believe_me StrNil
2626
2727unpack : String -> List Char
src/Core/TT.hs+2
@@ -40,6 +40,7 @@ instance Show FC where
4040data Err = Msg String
4141 | CantUnify Term Term Err Int -- Int is 'score' - how much we did unify
4242 | NotInjective Term Term Term
43+ | CantResolve Term
4344 | IncompleteTerm Term
4445 | UniverseError
4546 | ProgramLineComment
@@ -48,6 +49,7 @@ data Err = Msg String
4849
4950score :: Err -> Int
5051score (CantUnify _ _ m s) = s + score m
52+score (CantResolve _) = 20
5153score _ = 0
5254
5355instance Show Err where
src/Idris/Delaborate.hs+1
@@ -70,6 +70,7 @@ pshow i (CantUnify x y e s) = "Can't unify " ++ show (delab i x)
7070pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++
7171 " when unifying " ++ show (delab i x) ++ " and " ++
7272 show (delab i y)
73+pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)
7374pshow i (IncompleteTerm t) = "Incomplete term " ++ show t
7475pshow i UniverseError = "Universe inconsistency"
7576pshow i ProgramLineComment = "Program line next to comment"
src/Idris/ElabTerm.hs+1−1
@@ -341,7 +341,7 @@ resolveTC depth fn ist
341341 boundVar (P Bound _ _) = True
342342 boundVar _ = False
343343
344− blunderbuss t [] = fail $ "Can't resolve type class " ++ show t
344+ blunderbuss t [] = lift $ tfail $ CantResolve t
345345 blunderbuss t (n:ns) | n /= fn && tcname n = try (resolve n depth)
346346 (blunderbuss t ns)
347347 | otherwise = blunderbuss t ns
src/Idris/Parser.hs−1
@@ -313,7 +313,6 @@ pDecl syn = do notEndBlock
313313 <|> pDirective
314314 <|> try (do reserved "import"
315315 fp <- identifier
316− lchar ';'
317316 fail "imports must be at the top of file")
318317
319318pFunDecl :: SyntaxInfo -> IParser [PDecl]
tutorial/typesfuns.tex+1−1
@@ -38,7 +38,7 @@ in each module each have their own namespace, as we will discuss in Section
3838\ref{sect:namespaces}) and a
3939collection of declarations and definitions. Each definition must have a type
4040declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc).
41−Indentation is significant --- a new declaration begins at the same leve
41+Indentation is significant --- a new declaration begins at the same level
4242of indentation as the preceding declaration. Alternatively, declarations
4343may be terminated with a semicolon.
4444