c1e2921 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add missing error message

Fixes #693

commitc1e29210a19d9ba2421a761ecf7c2b329650979b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 30 Nov 2013, 23:29 (13 years ago) parent10410de

3 files changed+4−1

unifiedsplit

src/Core/Elaborate.hs+1−1

@@ -392,7 +392,7 @@ prepare_apply fn imps =

392392 = do ctxt <- get_context

393393 case lookupTy n ctxt of

394394 [] -> lift $ tfail $ NoSuchVariable n

395− _ -> fail $ "Too many arguments for " ++ show fn

395+ _ -> lift $ tfail $ TooManyArguments n

396396 | otherwise = fail $ "Too many arguments for " ++ show fn

397397

398398 doClaim ((i, _), n, t) = do claim n t

src/Core/TT.hs+1

@@ -85,6 +85,7 @@ data Err = Msg String

8585 | UnifyScope Name Name Term [(Name, Type)]

8686 | CantInferType String

8787 | NonFunctionType Term Term

88+ | TooManyArguments Name

8889 | CantIntroduce Term

8990 | NoSuchVariable Name

9091 | NoTypeDecl Name

src/Idris/Delaborate.hs+2

@@ -154,6 +154,8 @@ pshow i (NonFunctionType f ty)

154154 let colour = idris_colourRepl i in

155155 showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("

156156 ++ showImp (Just i) imps colour (delab i ty) ++ ")"

157+pshow i (TooManyArguments f)

158+ = "Too many arguments for " ++ show f

157159pshow i (CantIntroduce ty)

158160 = let imps = opt_showimp (idris_options i) in

159161 let colour = idris_colourRepl i in