From 21f45448b9bd5d2653481d6911659b35da5dd5d3 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 28 Jul 2017 15:50:08 +0100
Subject: Mips TLB existential example

---
 src/type_check.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/type_check.ml b/src/type_check.ml
index b4460992..fea94a90 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2514,7 +2514,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
 
   let nc_true = nc_eq (nconstant 0) (nconstant 0) in
   let typ_ret =
-    if existentials = []
+    if KidSet.is_empty (KidSet.inter (typ_frees typ_ret) (KidSet.of_list existentials))
     then typ_ret
     else mk_typ (Typ_exist (existentials, List.fold_left nc_and nc_true ex_constraints, typ_ret))
   in
-- 
cgit v1.2.3