From: Simon Huber <hubsim@gmail.com>
Date: Sat, 18 Apr 2015 03:26:04 +0000 (+0200)
Subject: bugfix
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=2e872b47e36edfa97137e6e7bc4bdcab3d1612a0;p=cubicaltt.git

bugfix
---

diff --git a/TypeChecker.hs b/TypeChecker.hs
index a6d3694..d5d180e 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -169,8 +169,8 @@ check a t = case (a,t) of
       local (addSubs iis) $ localM (addTele tele) $ do
         checkSystemWith ts $ \alpha talpha ->
           local (faceEnv alpha) $ do
-            rhoAlpha <- asks env
-            check (Ter t rhoAlpha) talpha
+            -- NB: the type doesn't depend on is
+            check (Ter t rho) talpha
         rho' <- asks env
         checkCompSystem (evalSystem rho' ts)
   (VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ ty ces) -> do