14 files changed, 460 insertions, 6 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index de1c1ae1..02339842 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -251,6 +251,25 @@ and strip_kinded_id_aux = function
 and strip_kind = function
   | K_aux (k_aux, _) -> K_aux (k_aux, Parse_ast.Unknown)
 
+let rec typ_constraints (Typ_aux (typ_aux, l)) =
+  match typ_aux with
+  | Typ_internal_unknown -> []
+  | Typ_id v -> []
+  | Typ_var kid -> []
+  | Typ_tup typs -> List.concat (List.map typ_constraints typs)
+  | Typ_app (f, args) -> List.concat (List.map typ_arg_nexps args)
+  | Typ_exist (kids, nc, typ) -> typ_constraints typ
+  | Typ_fn (arg_typs, ret_typ, _) ->
+     List.concat (List.map typ_constraints arg_typs) @ typ_constraints ret_typ
+  | Typ_bidir (typ1, typ2) ->
+     typ_constraints typ1 @ typ_constraints typ2
+and typ_arg_nexps (A_aux (typ_arg_aux, l)) =
+  match typ_arg_aux with
+  | A_nexp n -> []
+  | A_typ typ -> typ_constraints typ
+  | A_bool nc -> [nc]
+  | A_order ord -> []
+
 let rec typ_nexps (Typ_aux (typ_aux, l)) =
   match typ_aux with
   | Typ_internal_unknown -> []
@@ -2036,7 +2055,7 @@ let rec subtyp l env typ1 typ2 =
      let env = add_existential l kopts nc env in subtyp l env typ1 typ2
   | None, Some (kopts, nc, typ2) ->
      typ_debug (lazy "Subtype check with unification");
-     let typ1 = canonicalize env typ1 in
+     let typ1, env = bind_existential l None (canonicalize env typ1) env in
      let env = add_typ_vars l kopts env in
      let kids' = KidSet.elements (KidSet.diff (KidSet.of_list (List.map kopt_kid kopts)) (tyvars_of_typ typ2)) in
      if not (kids' = []) then typ_error env l "Universally quantified constraint generated" else ();
@@ -3266,13 +3285,15 @@ and bind_typ_pat env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_aux (typ_aux, _)
   | TP_wild, _ -> env
   | TP_var kid, _ ->
      begin
-       match typ_nexps typ with
-       | [nexp] ->
+       match typ_nexps typ, typ_constraints typ with
+       | [nexp], [] ->
           Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l (mk_kopt K_int kid) env)
-       | [] ->
+       | [], [nc] ->
+          Env.add_constraint (nc_and (nc_or (nc_not nc) (nc_var kid)) (nc_or nc (nc_not (nc_var kid)))) (Env.add_typ_var l (mk_kopt K_bool kid) env)
+       | [], [] ->
           typ_error env l ("No numeric expressions in " ^ string_of_typ typ ^ " to bind " ^ string_of_kid kid ^ " to")
-       | nexps ->
-          typ_error env l ("Type " ^ string_of_typ typ ^ " has multiple numeric expressions. Cannot bind " ^ string_of_kid kid)
+       | _, _ ->
+          typ_error env l ("Type " ^ string_of_typ typ ^ " has multiple numeric or boolean expressions. Cannot bind " ^ string_of_kid kid)
      end
   | TP_app (f1, tpats), Typ_app (f2, typs) when Id.compare f1 f2 = 0 ->
      List.fold_left2 bind_typ_pat_arg env tpats typs
diff --git a/test/typecheck/pass/existential_ast3.sail b/test/typecheck/pass/existential_ast3.sail
new file mode 100644
index 00000000..971b919c
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+union ast = {
+  Ctor : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))}
+}
+
+val decode : bits(16) -> option(ast)
+
+// Can have a constrained pair
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then (64, unsigned(b @ a)) else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
+
+// Or just lift the function body into the body if the if for flow typing
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  if b == 0b0 then {
+    Some(Ctor(64, unsigned(b @ a)))
+  } else {
+    Some(Ctor(32, unsigned(a)))
+  }
+}
+
+// Or use boolean constraint
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let 'is_64 = b == 0b0;
+  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+    if is_64 then 64 else 32;
+  let n : range(0, 'datasize) = if is_64 then unsigned(b @ a) else unsigned(a);
+  None()
+}
+
+// Other variants
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then {
+      let c = unsigned(b @ a);
+      (64, c)
+    } else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect
new file mode 100644
index 00000000..a1975425
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v1.expect
@@ -0,0 +1,20 @@
+Type error:
+[existential_ast3/v1.sail]:17:48-65
+17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
+   |                                                ^---------------^
+   | Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (33, unsigned(a))
+   | Coercion failed because:
+   | (int(33), int('ex62#)) is not a subtype of (int('ex57#), int('ex58#))
+   | [existential_ast3/v1.sail]:17:48-65
+   | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
+   |    |                                                ^---------------^
+   |    | 'ex57# bound here
+   | [existential_ast3/v1.sail]:17:48-65
+   | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
+   |    |                                                ^---------------^
+   |    | 'ex58# bound here
+   | [existential_ast3/v1.sail]:17:48-65
+   | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
+   |    |                                                ^---------------^
+   |    | 'ex62# bound here
+   | 
diff --git a/test/typecheck/pass/existential_ast3/v1.sail b/test/typecheck/pass/existential_ast3/v1.sail
new file mode 100644
index 00000000..05e13181
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v1.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+union ast = {
+  Ctor : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))}
+}
+
+val decode : bits(16) -> option(ast)
+
+// Can have a constrained pair
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
+  Some(Ctor(datasize, n))
+}
+
+// Or just lift the function body into the body if the if for flow typing
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  if b == 0b0 then {
+    Some(Ctor(64, unsigned(b @ a)))
+  } else {
+    Some(Ctor(32, unsigned(a)))
+  }
+}
+
+// Or use boolean constraint
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let 'is_64 = b == 0b0;
+  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+    if is_64 then 64 else 32;
+  let n : range(0, 'datasize) = if is_64 then unsigned(b @ a) else unsigned(a);
+  None()
+}
+
+// Other variants
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then {
+      let c = unsigned(b @ a);
+      (64, c)
+    } else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect
new file mode 100644
index 00000000..1ac6c87c
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v2.expect
@@ -0,0 +1,20 @@
+Type error:
+[existential_ast3/v2.sail]:17:48-65
+17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
+   |                                                ^---------------^
+   | Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (31, unsigned(a))
+   | Coercion failed because:
+   | (int(31), int('ex62#)) is not a subtype of (int('ex57#), int('ex58#))
+   | [existential_ast3/v2.sail]:17:48-65
+   | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
+   |    |                                                ^---------------^
+   |    | 'ex57# bound here
+   | [existential_ast3/v2.sail]:17:48-65
+   | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
+   |    |                                                ^---------------^
+   |    | 'ex58# bound here
+   | [existential_ast3/v2.sail]:17:48-65
+   | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
+   |    |                                                ^---------------^
+   |    | 'ex62# bound here
+   | 
diff --git a/test/typecheck/pass/existential_ast3/v2.sail b/test/typecheck/pass/existential_ast3/v2.sail
new file mode 100644
index 00000000..77fc14c6
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v2.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+union ast = {
+  Ctor : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))}
+}
+
+val decode : bits(16) -> option(ast)
+
+// Can have a constrained pair
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
+  Some(Ctor(datasize, n))
+}
+
+// Or just lift the function body into the body if the if for flow typing
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  if b == 0b0 then {
+    Some(Ctor(64, unsigned(b @ a)))
+  } else {
+    Some(Ctor(32, unsigned(a)))
+  }
+}
+
+// Or use boolean constraint
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let 'is_64 = b == 0b0;
+  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+    if is_64 then 64 else 32;
+  let n : range(0, 'datasize) = if is_64 then unsigned(b @ a) else unsigned(a);
+  None()
+}
+
+// Other variants
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then {
+      let c = unsigned(b @ a);
+      (64, c)
+    } else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect
new file mode 100644
index 00000000..05dcd0a1
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v3.expect
@@ -0,0 +1,7 @@
+Type error:
+[existential_ast3/v3.sail]:25:9-40
+25 |    Some(Ctor(64, unsigned(0b0 @ b @ a)))
+   |         ^-----------------------------^
+   | Could not resolve quantifiers for Ctor
+   | * (datasize(64) & (0 <= 'ex78# & ('ex78# + 1) <= 64))
+   | 
diff --git a/test/typecheck/pass/existential_ast3/v3.sail b/test/typecheck/pass/existential_ast3/v3.sail
new file mode 100644
index 00000000..53a55109
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v3.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+union ast = {
+  Ctor : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))}
+}
+
+val decode : bits(16) -> option(ast)
+
+// Can have a constrained pair
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then (64, unsigned(b @ a)) else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
+
+// Or just lift the function body into the body if the if for flow typing
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  if b == 0b0 then {
+    Some(Ctor(64, unsigned(0b0 @ b @ a)))
+  } else {
+    Some(Ctor(32, unsigned(a)))
+  }
+}
+
+// Or use boolean constraint
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let 'is_64 = b == 0b0;
+  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+    if is_64 then 64 else 32;
+  let n : range(0, 'datasize) = if is_64 then unsigned(b @ a) else unsigned(a);
+  None()
+}
+
+// Other variants
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then {
+      let c = unsigned(b @ a);
+      (64, c)
+    } else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast3/v4.expect b/test/typecheck/pass/existential_ast3/v4.expect
new file mode 100644
index 00000000..3de8b154
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v4.expect
@@ -0,0 +1,12 @@
+Type error:
+[existential_ast3/v4.sail]:36:18-20
+36 |    if is_64 then 64 else 32;
+   |                  ^^
+   | Tried performing type coercion from int(64) to {('d : Int), (('is_64 & 'd == 63) | (not('is_64) & 'd == 32)). int('d)} on 64
+   | Coercion failed because:
+   | int(64) is not a subtype of {('d : Int), (('is_64 & 'd == 63) | (not('is_64) & 'd == 32)). int('d)}
+   | [existential_ast3/v4.sail]:34:6-12
+   | 34 |  let 'is_64 = b == 0b0;
+   |    |      ^----^
+   |    | 'is_64 bound here
+   | 
diff --git a/test/typecheck/pass/existential_ast3/v4.sail b/test/typecheck/pass/existential_ast3/v4.sail
new file mode 100644
index 00000000..c2f03a86
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v4.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+union ast = {
+  Ctor : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))}
+}
+
+val decode : bits(16) -> option(ast)
+
+// Can have a constrained pair
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then (64, unsigned(b @ a)) else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
+
+// Or just lift the function body into the body if the if for flow typing
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  if b == 0b0 then {
+    Some(Ctor(64, unsigned(b @ a)))
+  } else {
+    Some(Ctor(32, unsigned(a)))
+  }
+}
+
+// Or use boolean constraint
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let 'is_64 = b == 0b0;
+  let 'datasize : {'d, ('is_64 & 'd == 63) | (not('is_64) & 'd == 32). int('d)} =
+    if is_64 then 64 else 32;
+  let n : range(0, 'datasize) = if is_64 then unsigned(b @ a) else unsigned(a);
+  None()
+}
+
+// Other variants
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then {
+      let c = unsigned(b @ a);
+      (64, c)
+    } else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast3/v5.expect b/test/typecheck/pass/existential_ast3/v5.expect
new file mode 100644
index 00000000..da686f6a
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v5.expect
@@ -0,0 +1,12 @@
+Type error:
+[existential_ast3/v5.sail]:37:50-65
+37 |  let n : range(0, 'datasize - 2) = if is_64 then unsigned(b @ a) else unsigned(a);
+   |                                                  ^-------------^
+   | Tried performing type coercion from range(0, (2 ^ (1 + 5) - 1)) to range(0, ('datasize - 2)) on unsigned(bitvector_concat(b, a))
+   | Coercion failed because:
+   | range(0, (2 ^ (1 + 5) - 1)) is not a subtype of range(0, ('datasize - 2))
+   | [existential_ast3/v5.sail]:35:6-15
+   | 35 |  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+   |    |      ^-------^
+   |    | 'datasize bound here
+   | 
diff --git a/test/typecheck/pass/existential_ast3/v5.sail b/test/typecheck/pass/existential_ast3/v5.sail
new file mode 100644
index 00000000..5a34dd32
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v5.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+union ast = {
+  Ctor : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))}
+}
+
+val decode : bits(16) -> option(ast)
+
+// Can have a constrained pair
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then (64, unsigned(b @ a)) else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
+
+// Or just lift the function body into the body if the if for flow typing
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  if b == 0b0 then {
+    Some(Ctor(64, unsigned(b @ a)))
+  } else {
+    Some(Ctor(32, unsigned(a)))
+  }
+}
+
+// Or use boolean constraint
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let 'is_64 = b == 0b0;
+  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+    if is_64 then 64 else 32;
+  let n : range(0, 'datasize - 2) = if is_64 then unsigned(b @ a) else unsigned(a);
+  None()
+}
+
+// Other variants
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then {
+      let c = unsigned(b @ a);
+      (64, c)
+    } else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast3/v6.expect b/test/typecheck/pass/existential_ast3/v6.expect
new file mode 100644
index 00000000..696f634a
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v6.expect
@@ -0,0 +1,12 @@
+Type error:
+[existential_ast3/v6.sail]:37:71-86
+37 |  let n : range(0, 'datasize - 1) = if is_64 then unsigned(b @ a) else unsigned(b @ a);
+   |                                                                       ^-------------^
+   | Tried performing type coercion from range(0, (2 ^ (1 + 5) - 1)) to range(0, ('datasize - 1)) on unsigned(bitvector_concat(b, a))
+   | Coercion failed because:
+   | range(0, (2 ^ (1 + 5) - 1)) is not a subtype of range(0, ('datasize - 1))
+   | [existential_ast3/v6.sail]:35:6-15
+   | 35 |  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+   |    |      ^-------^
+   |    | 'datasize bound here
+   | 
diff --git a/test/typecheck/pass/existential_ast3/v6.sail b/test/typecheck/pass/existential_ast3/v6.sail
new file mode 100644
index 00000000..87496c3d
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v6.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+union ast = {
+  Ctor : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))}
+}
+
+val decode : bits(16) -> option(ast)
+
+// Can have a constrained pair
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then (64, unsigned(b @ a)) else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
+
+// Or just lift the function body into the body if the if for flow typing
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  if b == 0b0 then {
+    Some(Ctor(64, unsigned(b @ a)))
+  } else {
+    Some(Ctor(32, unsigned(a)))
+  }
+}
+
+// Or use boolean constraint
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let 'is_64 = b == 0b0;
+  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+    if is_64 then 64 else 32;
+  let n : range(0, 'datasize - 1) = if is_64 then unsigned(b @ a) else unsigned(b @ a);
+  None()
+}
+
+// Other variants
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then {
+      let c = unsigned(b @ a);
+      (64, c)
+    } else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
\ No newline at end of file