From 40bf33af184cccf3522e864d8ee6f989cb8a09e2 Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Wed, 10 Feb 2016 21:31:41 +0100 Subject: [PATCH] Test for correct length in checks (Fixes #27) --- TypeChecker.hs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/TypeChecker.hs b/TypeChecker.hs index 29bdad6..3b22d2c 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -405,12 +405,13 @@ checkPathSystem t0 va ps = do return v checks :: (Tele,Env) -> [Ter] -> Typing () -checks _ [] = return () +checks ([],_) [] = return () checks ((x,a):xas,nu) (e:es) = do check (eval nu a) e v' <- evalTyping e checks (xas,upd (x,v') nu) es -checks _ _ = throwError "checks" +checks _ _ = + throwError "checks: incorrect number of arguments" -- infer the type of e infer :: Ter -> Typing Val -- 2.34.1