Various typechecker improvements:

* Fixed a bug where non-polymorphic function return types could be incorrect
* Added support for LEXP_memory AST node
* Flow typing constraint generation for all inequality operators
* Better support for increasing vector indices in field access expressions

7 files changed, 208 insertions, 40 deletions

diff --git a/mips_new_tc/mips_insts.sail b/mips_new_tc/mips_insts.sail
index d85ba0a5..07d4d841 100644
--- a/mips_new_tc/mips_insts.sail
+++ b/mips_new_tc/mips_insts.sail
@@ -35,9 +35,11 @@
 (* misp_insts.sail: mips instruction decode and execute clauses and AST node 
    declarations *)
 
-scattered function unit execute
 scattered typedef ast = const union
 
+val ast -> unit effect pure execute
+scattered function unit execute
+
 val bit[32] -> option<ast> effect pure decode
 scattered function option<ast> decode
 
@@ -56,7 +58,7 @@ function clause decode (0b011001 : (regno) rs : (regno) rt : (imm16) imm) =
 
 function clause execute (DADDIU (rs, rt, imm)) =
   {
-    wGPR(rt) := rGPR(rs) + EXTS(imm)
+    wGPR(rt) := rGPR(rs) + (bit[64]) (EXTS(imm))
   }
 
 (* DADDU Doubleword Add Unsigned -- another very simple instruction,
@@ -82,7 +84,7 @@ function clause decode (0b011000 : (regno) rs : (regno) rt : (imm16) imm) =
 
 function clause execute (DADDI (rs, rt, imm)) =
   {
-    let (bit[65]) sum65 = (EXTS(rGPR(rs)) + EXTS(imm)) in
+    let (bit[65]) sum65 = ((bit[65]) (EXTS(rGPR(rs))) + (bit[65]) (EXTS(imm))) in
     {
       if (sum65[64] != sum65[63]) then
         (SignalException(Ov))
@@ -101,7 +103,7 @@ function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b0000
 
 function clause execute (DADD (rs, rt, rd)) =
   {
-    let (bit[65]) sum65 = (EXTS(rGPR(rs)) + EXTS(rGPR(rt))) in
+    let (bit[65]) sum65 = ((bit[65]) (EXTS(rGPR(rs))) + (bit[65]) (EXTS(rGPR(rt)))) in
     {
       if sum65[64] != sum65[63] then
         (SignalException(Ov))
@@ -117,18 +119,18 @@ union ast member regregreg ADD
 function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100000) =
   Some(ADD(rs, rt, rd))
 
-function clause execute (ADD(rs, rt, rd)) = 
+function clause execute (ADD(rs, rt, rd)) =
   {
     (bit[64]) opA := rGPR(rs);
     (bit[64]) opB := rGPR(rt);
     if NotWordVal(opA) | NotWordVal(opB) then
-      wGPR(rd) := undefined (* XXX could exit instead *)
+      wGPR(rd) := (bit[64]) undefined (* XXX could exit instead *)
     else
-      let (bit[33]) sum33 = (EXTS(opA[31 .. 0]) + EXTS(opB[31 .. 0])) in
+      let (bit[33]) sum33 = ((bit[33]) (EXTS(opA[31 .. 0])) + (bit[33]) (EXTS(opB[31 .. 0]))) in
         if sum33[32] != sum33[31] then
           (SignalException(Ov))
         else
-          wGPR(rd) := EXTS(sum33[31..0])
+	  wGPR(rd) := (bit[64]) (EXTS(sum33[31..0]))
   }
 
 (* ADDI  32-bit add immediate -- reg, reg, imm with possible undefined behaviour or exception *)
@@ -1011,7 +1013,7 @@ function clause execute (BCMPZ(rs, imm, cmp, link, likely)) =
 (* Co-opt syscall 0xfffff for use as thread start in pccmem  *)
 union ast member unit SYSCALL_THREAD_START
 function clause decode (0b000000 : 0xfffff : 0b001100) =
-  Some(SYSCALL_THREAD_START)
+  Some((ast) SYSCALL_THREAD_START)
 function clause execute (SYSCALL_THREAD_START) = ()
 
 
@@ -1024,7 +1026,7 @@ function clause execute (ImplementationDefinedStopFetching) = ()
 
 union ast member unit SYSCALL
 function clause decode (0b000000 : (bit[20]) code : 0b001100) =
-  Some(SYSCALL) (* code is ignored *)
+  Some((ast) SYSCALL) (* code is ignored *)
 function clause execute (SYSCALL) =
   {
     (SignalException(Sys))
@@ -1033,7 +1035,7 @@ function clause execute (SYSCALL) =
 (* BREAK is identical to SYSCALL exception for the exception raised *)
 union ast member unit BREAK
 function clause decode (0b000000 : (bit[20]) code : 0b001101) =
-  Some(BREAK) (* code is ignored *)
+  Some((ast) BREAK) (* code is ignored *)
 function clause execute (BREAK) =
   {
     (SignalException(Bp))
@@ -1042,7 +1044,7 @@ function clause execute (BREAK) =
 (* Accept WAIT as a NOP *)
 union ast member unit WAIT
 function clause decode (0b010000 : 0x80000 : 0b100000) =
-  Some(WAIT) (* we only accept code == 0 *)
+  Some((ast) WAIT) (* we only accept code == 0 *)
 function clause execute (WAIT) = {
   nextPC := PC;
 }
@@ -1397,7 +1399,7 @@ function clause execute (PREF(base, op, imm)) =
 (* SYNC  - Memory barrier *)
 union ast member unit SYNC
 function clause decode (0b000000 : 0b00000 : 0b00000 : 0b00000 : (regno) stype : 0b001111) = 
-  Some(SYNC()) (* stype is currently ignored *)
+  Some((ast) SYNC) (* stype is currently ignored *)
 function clause execute(SYNC) =
   MEM_sync()
 
@@ -1479,10 +1481,10 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
 (* simulator halt instruction "MTC0 rt, r23" (cheri specific behaviour) *)
 union ast member unit HCF
 function clause decode (0b010000 : 0b00100 : (regno) rt : 0b10111 : 0b00000000000) =
-  Some(HCF()) 
+  Some((ast) HCF)
 
 function clause decode (0b010000 : 0b00100 : (regno) rt : 0b11010 : 0b00000000000) =
-  Some(HCF())
+  Some((ast) HCF)
 
 function clause execute (HCF) =
   () (* halt instruction actually executed by interpreter framework *)
@@ -1580,21 +1582,21 @@ function unit TLBWriteEntry((TLBIndexT) idx) = {
 }
 *)
 union ast member TLBWI
-function clause decode (0b010000 : 0b10000000000000000000 : 0b000010) = Some(TLBWI)
+function clause decode (0b010000 : 0b10000000000000000000 : 0b000010) = Some((ast) TLBWI)
 function clause execute (TLBWI) = {
   checkCP0Access();
   TLBWriteEntry(TLBIndex);
 }
 
 union ast member TLBWR
-function clause decode (0b010000 : 0b10000000000000000000 : 0b000110) = Some(TLBWR)
+function clause decode (0b010000 : 0b10000000000000000000 : 0b000110) = Some((ast) TLBWR)
 function clause execute (TLBWR) = {
   checkCP0Access();
   TLBWriteEntry(TLBRandom);
 }
 
 union ast member TLBR
-function clause decode (0b010000 : 0b10000000000000000000 : 0b000001) = Some(TLBR)
+function clause decode (0b010000 : 0b10000000000000000000 : 0b000001) = Some((ast) TLBR)
 function clause execute (TLBR) = {
   checkCP0Access();
   let entry = TLBEntries[TLBIndex] in {
@@ -1620,7 +1622,7 @@ function clause execute (TLBR) = {
 }
 
 union ast member TLBP
-function clause decode (0b010000 : 0b10000000000000000000 : 0b001000) = Some(TLBP)
+function clause decode (0b010000 : 0b10000000000000000000 : 0b001000) = Some((ast) TLBP)
 function clause execute ((TLBP)) = {
   checkCP0Access();
   let result = tlbSearch(TLBEntryHi) in
@@ -1655,8 +1657,9 @@ function clause execute (RDHWR(rt, rd)) = {
 }
 
 union ast member unit ERET
+
 function clause decode (0b010000 : 0b1 : 0b0000000000000000000 : 0b011000) =
-      Some(ERET)
+      Some((ast) ERET)
 function clause execute (ERET) =
       {
         checkCP0Access();
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index d60d8280..133c6db7 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -46,7 +46,7 @@ open Util
 open Ast_util
 open Big_int
 
-let debug = ref 1
+let debug = ref 2
 let depth = ref 0
 
 let rec indent n = match n with
@@ -848,6 +848,7 @@ let rec normalize_typ env (Typ_aux (typ, l)) =
      end
   | Typ_var kid -> Tnf_var kid
   | Typ_tup typs -> Tnf_tup (List.map (normalize_typ env) typs)
+  | Typ_app (f, []) -> normalize_typ env (Typ_aux (Typ_id f, l))
   | Typ_app (Id_aux (Id "range", _), [Typ_arg_aux (Typ_arg_nexp n1, _); Typ_arg_aux (Typ_arg_nexp n2, _)]) ->
      let kid = Env.fresh_kid env in
      Tnf_index_sort (IS_prop (kid, [(n1, nvar kid); (nvar kid, n2)]))
@@ -1181,6 +1182,12 @@ let unify l env typ1 typ2 =
     | Typ_id v1, Typ_id v2 ->
        if Id.compare v1 v2 = 0 then KBindings.empty
        else unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2)
+    | Typ_id v1, Typ_app (f2, []) ->
+       if Id.compare v1 f2 = 0 then KBindings.empty
+       else unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2)
+    | Typ_app (f1, []), Typ_id v2 ->
+       if Id.compare f1 v2 = 0 then KBindings.empty
+       else unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2)
     | Typ_var kid, _ when KidSet.mem kid goals -> KBindings.singleton kid (U_typ typ2)
     | Typ_var kid1, Typ_var kid2 when Kid.compare kid1 kid2 = 0 -> KBindings.empty
     | Typ_tup typs1, Typ_tup typs2 ->
@@ -1382,6 +1389,18 @@ let rec infer_flow env (E_aux (exp_aux, (l, _))) =
      let n1 = destructure_atom_nexp (typ_of x) in
      let n2 = destructure_atom_nexp (typ_of y) in
      [], [nc_lteq n1 n2]
+  | E_app (f, [x; y]) when string_of_id f = "gteq_atom_atom" ->
+     let n1 = destructure_atom_nexp (typ_of x) in
+     let n2 = destructure_atom_nexp (typ_of y) in
+     [], [nc_gteq n1 n2]
+  | E_app (f, [x; y]) when string_of_id f = "lt_atom_atom" ->
+     let n1 = destructure_atom_nexp (typ_of x) in
+     let n2 = destructure_atom_nexp (typ_of y) in
+     [], [nc_lt n1 n2]
+  | E_app (f, [x; y]) when string_of_id f = "gt_atom_atom" ->
+     let n1 = destructure_atom_nexp (typ_of x) in
+     let n2 = destructure_atom_nexp (typ_of y) in
+     [], [nc_gt n1 n2]
   | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "lt_range_atom" ->
      let kid = Env.fresh_kid env in
      let c = destructure_atom (typ_of y) in
@@ -1436,7 +1455,10 @@ let rec match_typ (Typ_aux (typ1, _)) (Typ_aux (typ2, _)) =
   | Typ_id v, Typ_app (f, _) when string_of_id v = "nat" &&  string_of_id f = "range" -> true
   | Typ_id v, Typ_app (f, _) when string_of_id v = "int" &&  string_of_id f = "range" -> true
   | Typ_app (f1, _), Typ_app (f2, _) when string_of_id f1 = "range" && string_of_id f2 = "atom" -> true
+  | Typ_app (f1, _), Typ_app (f2, _) when string_of_id f1 = "atom" && string_of_id f2 = "range" -> true
   | Typ_app (f1, _), Typ_app (f2, _) when Id.compare f1 f2 = 0 -> true
+  | Typ_id v1, Typ_app (f2, _) when Id.compare v1 f2 = 0 -> true
+  | Typ_app (f1, _), Typ_id v2 when Id.compare f1 v2 = 0 -> true
   | _, _ -> false
 
 let rec filter_casts env from_typ to_typ casts =
@@ -1670,7 +1692,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
          | Typ_tup typs -> typs
          | _ -> [typ]
        in
-       match ctor_typ with
+       match Env.expand_synonyms env ctor_typ with
        | Typ_aux (Typ_fn (arg_typ, ret_typ, _), _) ->
           begin
             try
@@ -1762,6 +1784,8 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
           annot_assign (annot_lexp (LEXP_field (annot_lexp_effect (LEXP_id v) regtyp (mk_effect [BE_wreg]), field)) vec_typ) checked_exp, env
        | _ ->  typ_error l "Field l-expression has invalid type"
      end
+  | LEXP_memory (f, xs) ->
+     check_exp env (E_aux (E_app (f, xs @ [exp]), (l, ()))) unit_typ, env
   | _ ->
      let inferred_exp = irule infer_exp env exp in
      let tlexp, env' = bind_lexp env lexp (typ_of inferred_exp) in
@@ -1852,7 +1876,10 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        | Local (_, typ) | Enum typ -> annot_exp (E_id v) typ
        | Register typ -> annot_exp_effect (E_id v) typ (mk_effect [BE_rreg])
        | Unbound -> typ_error l ("Identifier " ^ string_of_id v ^ " is unbound")
-       | Union _ -> typ_error l ("Cannot infer the type of polymorphic union indentifier " ^ string_of_id v)
+       | Union (typq, typ) ->
+          if quant_items typq = []
+          then annot_exp (E_id v) typ
+          else typ_error l ("Cannot infer the type of polymorphic union indentifier " ^ string_of_id v)
      end
   | E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit)
   | E_sizeof nexp -> annot_exp (E_sizeof nexp) (mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp nexp)])))
@@ -1868,7 +1895,6 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        match Env.expand_synonyms env (typ_of inferred_exp) with
        (* Accessing a (bit) field of a register *)
        | Typ_aux (Typ_id regtyp, _) when Env.is_regtyp regtyp env ->
-          typ_print "REGTYP";
           let base, top, ranges = Env.get_regtyp regtyp env in
           let range, _ =
             try List.find (fun (_, id) -> Id.compare id field = 0) ranges with
@@ -1877,17 +1903,22 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
           begin
             match range, Env.get_default_order env with
             | BF_aux (BF_single n, _), Ord_aux (Ord_dec, _) ->
-               let vec_typ = dvector_typ env (nconstant n) (nconstant 1) (mk_typ (Typ_id (mk_id "bit"))) in
+               let vec_typ = dvector_typ env (nconstant n) (nconstant 1) bit_typ in
                annot_exp (E_field (inferred_exp, field)) vec_typ
             | BF_aux (BF_range (n, m), _), Ord_aux (Ord_dec, _) ->
-               let vec_typ = dvector_typ env (nconstant n) (nconstant (n - m + 1)) (mk_typ (Typ_id (mk_id "bit"))) in
+               let vec_typ = dvector_typ env (nconstant n) (nconstant (n - m + 1)) bit_typ in
+               annot_exp (E_field (inferred_exp, field)) vec_typ
+            | BF_aux (BF_single n, _), Ord_aux (Ord_inc, _) ->
+               let vec_typ = dvector_typ env (nconstant n) (nconstant 1) bit_typ in
                annot_exp (E_field (inferred_exp, field)) vec_typ
-            | _, _ -> typ_error l "Not implemented this register field type yet..." (* FIXME *)
+            | BF_aux (BF_range (n, m), _), Ord_aux (Ord_inc, _) ->
+               let vec_typ = dvector_typ env (nconstant n) (nconstant (m - n + 1)) bit_typ in
+               annot_exp (E_field (inferred_exp, field)) vec_typ
+            | _, _ -> typ_error l "Invalid register field type"
           end
        (* Accessing a field of a record *)
        | Typ_aux (Typ_id rectyp, _) as typ when Env.is_record rectyp env ->
           begin
-            typ_print "RECTYP";
             let inferred_acc = infer_funapp' l (Env.no_casts env) field (Env.get_accessor field env) [strip_exp inferred_exp] None in
             match inferred_acc with
             | E_aux (E_app (field, [inferred_exp]) ,_) -> annot_exp (E_field (inferred_exp, field)) (typ_of inferred_acc)
@@ -2027,18 +2058,23 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
          (quants', typs', ret_typ')
        end
   in
-  match f_typ with
-  | Typ_aux (Typ_fn (Typ_aux (Typ_tup typ_args, _), typ_ret, eff), _) ->
-     let (quants, typ_args, typ_ret) = instantiate_ret (quant_items typq) typ_args typ_ret in
-     let (xs_instantiated, typ_ret) = instantiate quants ([], typ_args) typ_ret ([], number 0 xs) in
-     let xs_reordered = List.map snd (List.sort (fun (n, _) (m, _) -> compare n m) xs_instantiated) in
-     annot_exp (E_app (f, xs_reordered)) typ_ret eff
-  | Typ_aux (Typ_fn (typ_arg, typ_ret, eff), _) ->
-     let (quants, typ_args, typ_ret) = instantiate_ret (quant_items typq) [typ_arg] typ_ret in
-     let (xs_instantiated, typ_ret) = instantiate quants ([], typ_args) typ_ret ([], number 0 xs) in
-     let xs_reordered = List.map snd (List.sort (fun (n, _) (m, _) -> compare n m) xs_instantiated) in
-     annot_exp (E_app (f, xs_reordered)) typ_ret eff
-  | _ -> typ_error l (string_of_typ f_typ ^ " is not a function type")
+  let exp =
+    match Env.expand_synonyms env f_typ with
+    | Typ_aux (Typ_fn (Typ_aux (Typ_tup typ_args, _), typ_ret, eff), _) ->
+       let (quants, typ_args, typ_ret) = instantiate_ret (quant_items typq) typ_args typ_ret in
+       let (xs_instantiated, typ_ret) = instantiate quants ([], typ_args) typ_ret ([], number 0 xs) in
+       let xs_reordered = List.map snd (List.sort (fun (n, _) (m, _) -> compare n m) xs_instantiated) in
+       annot_exp (E_app (f, xs_reordered)) typ_ret eff
+    | Typ_aux (Typ_fn (typ_arg, typ_ret, eff), _) ->
+       let (quants, typ_args, typ_ret) = instantiate_ret (quant_items typq) [typ_arg] typ_ret in
+       let (xs_instantiated, typ_ret) = instantiate quants ([], typ_args) typ_ret ([], number 0 xs) in
+       let xs_reordered = List.map snd (List.sort (fun (n, _) (m, _) -> compare n m) xs_instantiated) in
+       annot_exp (E_app (f, xs_reordered)) typ_ret eff
+    | _ -> typ_error l (string_of_typ f_typ ^ " is not a function type")
+  in
+  match ret_ctx_typ with
+  | None -> exp
+  | Some rct -> type_coercion env exp rct
 
 (**************************************************************************)
 (* 6. Effect system                                                       *)
diff --git a/test/typecheck/fail/funret1.sail b/test/typecheck/fail/funret1.sail
new file mode 100644
index 00000000..09a4fd54
--- /dev/null
+++ b/test/typecheck/fail/funret1.sail
@@ -0,0 +1,16 @@
+
+default Order inc
+
+typedef option = const union forall Type 'a. {
+  None;
+  'a Some
+  }
+
+typedef Test = const union {
+  A;
+  B;
+  C
+}
+
+let (option<int>) x = C
+
diff --git a/test/typecheck/fail/funret2.sail b/test/typecheck/fail/funret2.sail
new file mode 100644
index 00000000..19536599
--- /dev/null
+++ b/test/typecheck/fail/funret2.sail
@@ -0,0 +1,16 @@
+
+default Order inc
+
+typedef option = const union forall Type 'a. {
+  None;
+  'a Some
+  }
+
+typedef Test = const union {
+  A;
+  B;
+  C
+}
+
+
+function option<int> test2 () = C
diff --git a/test/typecheck/fail/funret3.sail b/test/typecheck/fail/funret3.sail
new file mode 100644
index 00000000..d178f2ad
--- /dev/null
+++ b/test/typecheck/fail/funret3.sail
@@ -0,0 +1,16 @@
+
+default Order inc
+
+typedef option = const union forall Type 'a. {
+  None;
+  'a Some
+  }
+
+typedef Test = const union {
+  A;
+  B;
+  C
+}
+
+
+function option<(option<int>)> test () = Some(C)
diff --git a/test/typecheck/pass/lexp_memory.sail b/test/typecheck/pass/lexp_memory.sail
new file mode 100644
index 00000000..83313ac7
--- /dev/null
+++ b/test/typecheck/pass/lexp_memory.sail
@@ -0,0 +1,65 @@
+default Order dec
+
+register (bit[64]) GPR00 (* should never be read or written *)
+register (bit[64]) GPR01
+register (bit[64]) GPR02
+register (bit[64]) GPR03
+register (bit[64]) GPR04
+register (bit[64]) GPR05
+register (bit[64]) GPR06
+register (bit[64]) GPR07
+register (bit[64]) GPR08
+register (bit[64]) GPR09
+register (bit[64]) GPR10
+register (bit[64]) GPR11
+register (bit[64]) GPR12
+register (bit[64]) GPR13
+register (bit[64]) GPR14
+register (bit[64]) GPR15
+register (bit[64]) GPR16
+register (bit[64]) GPR17
+register (bit[64]) GPR18
+register (bit[64]) GPR19
+register (bit[64]) GPR20
+register (bit[64]) GPR21
+register (bit[64]) GPR22
+register (bit[64]) GPR23
+register (bit[64]) GPR24
+register (bit[64]) GPR25
+register (bit[64]) GPR26
+register (bit[64]) GPR27
+register (bit[64]) GPR28
+register (bit[64]) GPR29
+register (bit[64]) GPR30
+register (bit[64]) GPR31
+
+let (vector <0, 32, inc, (register<(bit[64])>) >) GPR =
+  [ GPR00, GPR01, GPR02, GPR03, GPR04, GPR05, GPR06, GPR07, GPR08, GPR09, GPR10,
+  GPR11, GPR12, GPR13, GPR14, GPR15, GPR16, GPR17, GPR18, GPR19, GPR20,
+  GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31
+  ]
+
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
+
+overload vector_access [vector_access_inc; vector_access_dec]
+
+val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure eq_vec
+
+overload (deinfix ==) [eq_vec]
+
+val cast forall Nat 'n, Nat 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec
+val cast forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned
+val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref
+
+val (bit[5], bit[64]) -> unit effect {wreg} wGPR
+
+function unit wGPR (idx, v) =
+{
+  if idx == 0 then () else GPR[idx] := v
+}
+
+function unit test () =
+{
+  wGPR(0b00001) := 0
+}
diff --git a/test/typecheck/pass/union_infer.sail b/test/typecheck/pass/union_infer.sail
new file mode 100644
index 00000000..397525e0
--- /dev/null
+++ b/test/typecheck/pass/union_infer.sail
@@ -0,0 +1,16 @@
+
+default Order inc
+
+typedef option = const union forall Type 'a. {
+  None;
+  'a Some
+  }
+
+typedef Test = const union {
+  A;
+  B;
+  C
+}
+
+
+function option<Test> test () = Some(C)