From 6f3bf52cef2bd210fbad96f189bf3d6e13872fdb Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 8 Jan 2018 17:03:19 +0000
Subject: Potential fix for bug where different quantifer order in existentials
 will break alpha-equivalence.

---
 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 5bd633ee..d03673d9 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1583,7 +1583,7 @@ let rec alpha_equivalent env typ1 typ2 =
          let kids = List.map (fun kid -> (kid, new_kid ())) kids in
          let nc = List.fold_left (fun nc (kid, nk) -> nc_subst_nexp kid (Nexp_var nk) nc) nc kids in
          let typ = List.fold_left (fun nc (kid, nk) -> typ_subst_nexp kid (Nexp_var nk) nc) typ kids in
-         Typ_exist (List.map snd kids, nc, typ)
+         Typ_exist (List.sort Kid.compare (List.map snd kids), nc, typ)
       | Typ_app (id, args) ->
          Typ_app (id, List.map relabel_arg args)
     in
-- 
cgit v1.2.3