c1e2921 · Idris-dev · git.iko.soy

src/Core/Elaborate.hs+1−1

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

392 = do ctxt <- get_context

393 case lookupTy n ctxt of

394 [] -> lift $ tfail $ NoSuchVariable n

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

395+ _ -> lift $ tfail $ TooManyArguments n

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

397

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

src/Core/TT.hs+1

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

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

86 | CantInferType String

87 | NonFunctionType Term Term

88+ | TooManyArguments Name

88 | CantIntroduce Term

89 | CantIntroduce Term

89 | NoSuchVariable Name

90 | NoSuchVariable Name

90 | NoTypeDecl Name

91 | NoTypeDecl Name

src/Idris/Delaborate.hs+2

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

154 let colour = idris_colourRepl i in

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

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

157+pshow i (TooManyArguments f)

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

157pshow i (CantIntroduce ty)

159pshow i (CantIntroduce ty)

158 = let imps = opt_showimp (idris_options i) in

160 = let imps = opt_showimp (idris_options i) in

159 let colour = idris_colourRepl i in

161 let colour = idris_colourRepl i in