8 files changed, 248 insertions, 1 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index b058d514..a2612794 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1304,6 +1304,15 @@ let bind_existential l name typ env =
   | Some (kids, nc, typ) -> typ, add_existential l kids nc env
   | None -> typ, env
 
+let bind_tuple_existentials l name (Typ_aux (aux, annot) as typ) env =
+  match aux with
+  | Typ_tup typs ->
+     let typs, env =
+       List.fold_right (fun typ (typs, env) -> let typ, env = bind_existential l name typ env in typ :: typs, env) typs ([], env)
+     in
+     Typ_aux (Typ_tup typs, annot), env
+  | _ -> typ, env
+
 let destruct_range env typ =
   let kopts, constr, (Typ_aux (typ_aux, _)) =
     Util.option_default ([], nc_true, typ) (destruct_exist (Env.expand_synonyms env typ))
@@ -1567,6 +1576,8 @@ let merge_uvars l unifiers1 unifiers2 =
   KBindings.merge (merge_unifiers l) unifiers1 unifiers2
 
 let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as typ2) =
+  typ_debug (lazy (Util.("Unify type " |> magenta |> clear) ^ string_of_typ typ1 ^ " and " ^ string_of_typ typ2
+                   ^ " goals " ^ string_of_list ", " string_of_kid (KidSet.elements goals)));
   match aux1, aux2 with
   | Typ_internal_unknown, _ | _, Typ_internal_unknown
        when Env.allow_unknowns env ->
@@ -1577,7 +1588,14 @@ let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as
   | Typ_app (range, [A_aux (A_nexp n1, _); A_aux (A_nexp n2, _)]),
     Typ_app (atom, [A_aux (A_nexp m, _)])
        when string_of_id range = "range" && string_of_id atom = "atom" ->
-     merge_uvars l (unify_nexp l env goals n1 m) (unify_nexp l env goals n2 m)
+     let n1, n2 = nexp_simp n1, nexp_simp n2 in
+     begin match n1, n2 with
+     | Nexp_aux (Nexp_constant c1, _), Nexp_aux (Nexp_constant c2, _) ->
+        if prove __POS__ env (nc_and (nc_lteq n1 m) (nc_lteq m n2)) then KBindings.empty
+        else unify_error l (string_of_typ typ1 ^ " is not contained within " ^ string_of_typ typ1)
+     | _, _ ->
+        merge_uvars l (unify_nexp l env goals n1 m) (unify_nexp l env goals n2 m)
+     end
 
   | Typ_app (id1, args1), Typ_app (id2, args2) when List.length args1 = List.length args2 && Id.compare id1 id2 = 0 ->
      List.fold_left (merge_uvars l) KBindings.empty (List.map2 (unify_typ_arg l env goals) args1 args2)
@@ -2932,6 +2950,7 @@ and type_coercion_unify env goals (E_aux (_, (l, _)) as annotated_exp) typ =
     try
       typ_debug (lazy ("Coercing unification: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ));
       let atyp, env = bind_existential l None (typ_of annotated_exp) env in
+      let atyp, env = bind_tuple_existentials l None atyp env in
       annotated_exp, unify l env (KidSet.diff goals (ambiguous_vars typ)) typ atyp, env
     with
     | Unification_error (_, m) when Env.allow_casts env ->
diff --git a/test/typecheck/pass/existential_ast.sail b/test/typecheck/pass/existential_ast.sail
new file mode 100644
index 00000000..37cf2378
--- /dev/null
+++ b/test/typecheck/pass/existential_ast.sail
@@ -0,0 +1,54 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+type regno = range(0, 31)
+
+union ast = {
+  Ctor1 : {'d, datasize('d). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, int('d), bits(4))}
+}
+
+val decode : bits(16) -> option(ast)
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000110) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast/v1.expect b/test/typecheck/pass/existential_ast/v1.expect
new file mode 100644
index 00000000..f743abb6
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v1.expect
@@ -0,0 +1,6 @@
+Type error:
+[existential_ast/v1.sail]:46:7-21
+46 |  Some(Ctor2(y, x, c))
+   |       ^------------^
+   | No valid casts resulted in unification
+   | 
diff --git a/test/typecheck/pass/existential_ast/v1.sail b/test/typecheck/pass/existential_ast/v1.sail
new file mode 100644
index 00000000..935313f7
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v1.sail
@@ -0,0 +1,47 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+type regno = range(0, 31)
+
+union ast = {
+  Ctor1 : {'d, datasize('d). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, int('d), bits(4))}
+}
+
+val decode : bits(16) -> option(ast)
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000110) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b01);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast/v2.expect b/test/typecheck/pass/existential_ast/v2.expect
new file mode 100644
index 00000000..20738cd8
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v2.expect
@@ -0,0 +1,6 @@
+Type error:
+[existential_ast/v2.sail]:39:7-21
+39 |  Some(Ctor2(y, x, c))
+   |       ^------------^
+   | No valid casts resulted in unification
+   | 
diff --git a/test/typecheck/pass/existential_ast/v2.sail b/test/typecheck/pass/existential_ast/v2.sail
new file mode 100644
index 00000000..fd272dbb
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v2.sail
@@ -0,0 +1,54 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+type regno = range(0, 30)
+
+union ast = {
+  Ctor1 : {'d, datasize('d). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, int('d), bits(4))}
+}
+
+val decode : bits(16) -> option(ast)
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000110) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
new file mode 100644
index 00000000..1b6239bb
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -0,0 +1,7 @@
+Type error:
+[existential_ast/v3.sail]:26:7-21
+26 |  Some(Ctor1(a, x, c))
+   |       ^------------^
+   | Could not resolve quantifiers for Ctor1
+   | * datasize('ex59#)
+   | 
diff --git a/test/typecheck/pass/existential_ast/v3.sail b/test/typecheck/pass/existential_ast/v3.sail
new file mode 100644
index 00000000..1bacbf80
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v3.sail
@@ -0,0 +1,54 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+type regno = range(0, 31)
+
+union ast = {
+  Ctor1 : {'d, datasize('d). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, int('d), bits(4))}
+}
+
+val decode : bits(16) -> option(ast)
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000110) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|16, 32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file