From: Simon Huber <hubsim@gmail.com>
Date: Wed, 10 Feb 2016 20:31:41 +0000 (+0100)
Subject: Test for correct length in checks (Fixes #27)
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=40bf33af184cccf3522e864d8ee6f989cb8a09e2;p=cubicaltt.git

Test for correct length in checks (Fixes #27)
---

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