b894841 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Improve some error messages

commitb8948414532e73d6a8752999330b1b7d0afef35f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 17 Oct 2012, 10:24 (14 years ago) parent5a6299b

5 files changed+38−20

compare with master

unifiedsplit

src/Core/TT.hs+4 src/Core/Typecheck.hs+8−6 src/Core/Unify.hs+7−2 src/Idris/Delaborate.hs+15−7 src/Idris/ElabDecls.hs+4−5

src/Core/TT.hs+4

@@ -48,6 +48,8 @@ data Err = Msg String

4848 -- Int is 'score' - how much we did unify

4949 -- Bool indicates recoverability, True indicates more info may make

5050 -- unification succeed

51+ | InfiniteUnify Name Term [(Name, Type)]

52+ | CantConvert Term Term [(Name, Type)]

5153 | NoSuchVariable Name

5254 | NoTypeDecl Name

5355 | NotInjective Term Term Term

@@ -64,6 +66,8 @@ instance Sized Err where

6466 size (Msg msg) = length msg

6567 size (InternalMsg msg) = length msg

6668 size (CantUnify _ left right err _ score) = size left + size right + size err

69+ size (InfiniteUnify _ right _) = size right

70+ size (CantConvert left right _) = size left + size right

6771 size (NoSuchVariable name) = size name

6872 size (NoTypeDecl name) = size name

6973 size (NotInjective l c r) = size l + size c + size r

src/Core/Typecheck.hs+8−6

@@ -19,17 +19,19 @@ convertsC ctxt env x y

1919 = do c <- convEq ctxt (finalise (normalise ctxt env x))

2020 (finalise (normalise ctxt env y))

2121 if c then return ()

22− else fail ("Can't convert between " ++

23− showEnv env (finalise (normalise ctxt env x)) ++ " and " ++

24− showEnv env (finalise (normalise ctxt env y)))

22+ else lift $ tfail (CantConvert

23+ (finalise (normalise ctxt env x))

24+ (finalise (normalise ctxt env y)) (errEnv env))

2525

2626converts :: Context -> Env -> Term -> Term -> TC ()

2727converts ctxt env x y = if (finalise (normalise ctxt env x) ==

2828 finalise (normalise ctxt env y))

2929 then return ()

30− else fail ("Can't convert between " ++

31− showEnvDbg env (finalise (normalise ctxt env x)) ++ " and " ++

32− showEnvDbg env (finalise (normalise ctxt env y)))

30+ else tfail (CantConvert

31+ (finalise (normalise ctxt env x))

32+ (finalise (normalise ctxt env y)) (errEnv env))

33+

34+errEnv = map (\(x, b) -> (x, binderTy b))

3335

3436isSet :: Context -> Env -> Term -> TC ()

3537isSet ctxt env tm = isSet' (normalise ctxt env tm)

src/Core/Unify.hs+7−2

@@ -77,12 +77,12 @@ unify ctxt env topx topy

7777 | holeIn env x = do UI s i f <- get

7878 when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i) f)

7979 sc 1

80− return [(x, tm)]

80+ checkCycle (x, tm)

8181 un' fn bnames tm (P Bound y _)

8282 | holeIn env y = do UI s i f <- get

8383 when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i) f)

8484 sc 1

85− return [(y, tm)]

85+ checkCycle (y, tm)

8686 un' fn bnames (V i) (P Bound x _)

8787 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

8888 un' fn bnames (P Bound x _) (V i)

@@ -165,6 +165,11 @@ unify ctxt env topx topy

165165 put (UI s i ((binderTy x, binderTy y, env, err) : f))

166166 return [] -- lift $ tfail err

167167

168+ checkCycle p@(x, P _ _ _) = return [p]

169+ checkCycle (x, tm)

170+ | not (x `elem` freeNames tm) = return [(x, tm)]

171+ | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))

172+

168173 combine bnames as [] = return as

169174 combine bnames as ((n, t) : bs)

170175 = case lookup n as of

src/Idris/Delaborate.hs+15−7

@@ -83,13 +83,14 @@ pshow i (CantUnify _ x y e sc s)

8383 case e of

8484 Msg "" -> ""

8585 _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++

86− if (opt_errContext (idris_options i)) then showSc sc else ""

87− where showSc [] = ""

88− showSc xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

89− showVar (x, y) = "\t" ++ showbasic x ++ " : " ++ show (delab i y)

90− showbasic n@(UN _) = show n

91− showbasic (MN _ s) = s

92− showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n

86+ if (opt_errContext (idris_options i)) then showSc i sc else ""

87+pshow i (CantConvert x y env)

88+ = "Can't unify " ++ show (delab i x) ++ " with " ++ show (delab i y) ++

89+ if (opt_errContext (idris_options i)) then showSc i env else ""

90+pshow i (InfiniteUnify x tm env)

91+ = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++

92+ " would lead to infinite value" ++

93+ if (opt_errContext (idris_options i)) then showSc i env else ""

9394pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++

9495 " when unifying " ++ show (delab i x) ++ " and " ++

9596 show (delab i y)

@@ -103,3 +104,10 @@ pshow i ProgramLineComment = "Program line next to comment"

103104pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

104105pshow i (At f e) = show f ++ ":" ++ pshow i e

105106

107+showSc i [] = ""

108+showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

109+ where showVar (x, y) = "\t" ++ showbasic x ++ " : " ++ show (delab i y)

110+

111+showbasic n@(UN _) = show n

112+showbasic (MN _ s) = s

113+showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n

src/Idris/ElabDecls.hs+4−5

@@ -241,7 +241,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

241241 tree@(CaseDef scargs sc _) <- tclift $ simpleCase tcase False CompileTime fc pdef

242242 tclift $ sameLength pdef

243243 cov <- coverage

244− pcover <-

244+ pmissing <-

245245 if cov

246246 then do -- missing <- genClauses fc n (map getLHS pdef) cs

247247 missing <- genMissing n scargs sc

@@ -250,10 +250,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

250250 showSep "\n" (map (showImp True) missing') ++

251251 "\nAgainst: " ++

252252 showSep "\n" (map (\t -> showImp True (delab ist t)) (map getLHS pdef))

253− if null missing'

254− then return True

255− else return False

256− else return False

253+ return missing'

254+ else return []

255+ let pcover = null pmissing

257256 pdef' <- applyOpts pdef

258257 ist <- get

259258-- let wf = wellFounded ist n sc