support hcomp in typechecker

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 12135e7633debac3b24c826085d6d41aae5f515c..40050c0dcce0ed7d7101e4ea6256a9b736183a63 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -483,6 +483,12 @@ infer e = case e of
     check va0 t0\r
     checkPLamSystem t0 va ps\r
     return va1\r
+  HComp a u0 us -> do\r
+    check VU a\r
+    va <- evalTyping a\r
+    check va u0\r
+    checkPLamSystem u0 (constPath va) us\r
+    return va\r
   Fill a t0 ps -> do\r
     (va0, va1) <- checkPLam (constPath VU) a\r
     va <- evalTyping a\r