Remove unnecessary argument to addBranch

diff --git a/TypeChecker.hs b/TypeChecker.hs
index bebce3654ee41eb38c3d5054dfd4b40e98f873d7..b5544e656cb16b8cbd5a9e55a45fd63e71b0634e 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -74,8 +74,8 @@ addSubs = flip $ foldr addSub
 addType :: (Ident,Ter) -> TEnv -> TEnv\r
 addType (x,a) tenv@(TEnv _ _ rho _) = addTypeVal (x,eval rho a) tenv\r
 \r
-addBranch :: [(Ident,Val)] -> (Tele,Env) -> TEnv -> TEnv\r
-addBranch nvs (tele,env) (TEnv k ind rho v) =\r
+addBranch :: [(Ident,Val)] -> Env -> TEnv -> TEnv\r
+addBranch nvs env (TEnv k ind rho v) =\r
   TEnv (k + length nvs) ind (upds rho nvs) v\r
 \r
 addDecls :: [Decl] -> TEnv -> TEnv\r
@@ -107,7 +107,7 @@ constPath :: Val -> Val
 constPath = VPath (Name "_")\r
 \r
 mkVars :: Int -> Tele -> Env -> [(Ident,Val)]\r
-mkVars k [] _ = []\r
+mkVars _ [] _           = []\r
 mkVars k ((x,a):xas) nu =\r
   let w = mkVar k x (eval nu a)\r
   in (x,w) : mkVars (k+1) xas (Upd nu (x,w))\r
@@ -296,7 +296,7 @@ checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing ()
 checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do\r
   k <- asks index\r
   let us = map snd $ mkVars k tele nu\r
-  local (addBranch (zip ns us) (tele,nu)) $ check (app f (VCon c us)) e\r
+  local (addBranch (zip ns us) nu) $ check (app f (VCon c us)) e\r
 checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do\r
   k <- asks index\r
   mapM_ checkFresh js\r
@@ -305,7 +305,7 @@ checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do
       js'  = map Atom js\r
       vts  = evalSystem (subs (upds nu us) (zip is js')) ts\r
       vfts = intersectionWith app (border g ts) vts\r
-  local (addSubs (zip js js') . addBranch (zip ns vus) (tele,nu)) $ do\r
+  local (addSubs (zip js js') . addBranch (zip ns vus) nu) $ do\r
     check (app f (VPCon c va vus js')) e\r
     ve  <- evalTyping e -- TODO: combine with next line?\r
     unlessM (border ve ts === vfts) $\r