From a5c6f94bfc0da84e214641e0b87aa9649ea114ea Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= <anma7372@r120.math.su.se>
Date: Tue, 16 Oct 2018 13:57:55 +0200
Subject: [PATCH] support hcomp in typechecker

---
 TypeChecker.hs | 6 ++++++
 1 file changed, 6 insertions(+)

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