diff options
| author | Alasdair Armstrong | 2018-01-08 17:03:19 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-01-08 17:03:19 +0000 |
| commit | 6f3bf52cef2bd210fbad96f189bf3d6e13872fdb (patch) | |
| tree | d387780edce1c612ef3eefe01f2a90c4f6f8936c /src | |
| parent | 4597e503131395df087b1aa9a600a96be5a960ed (diff) | |
Potential fix for bug where different quantifer order in existentials will break alpha-equivalence.
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |