33 files changed, 189 insertions, 260 deletions

diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 4c6b7974..d9ba1cde 100644
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -366,10 +366,10 @@ val break : unit -> unit
 function break () = ()
 
 union exception = {
-  Error_Undefined,
+  Error_Undefined : unit,
   Error_See : string,
   Error_Implementation_Defined : string,
-  Error_ReservedEncoding
+  Error_ReservedEncoding : unit
 }
 
 /*
diff --git a/language/l2.ott b/language/l2.ott
index e6b52482..c34dedb5 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -459,7 +459,6 @@ kind_def :: 'KD_' ::=
 type_union :: 'Tu_' ::=
   {{ com type union constructors }}
   {{ aux _ l }}
-  | id                                                  :: :: id
   | typ id                                              :: :: ty_id
 
 index_range :: 'BF_' ::= {{ com index specification, for bitfields in register types}} 
diff --git a/lib/option.sail b/lib/option.sail
new file mode 100644
index 00000000..3869167b
--- /dev/null
+++ b/lib/option.sail
@@ -0,0 +1,28 @@
+$ifndef _OPTION
+$define _OPTION
+
+// The option type is treated specially by the lem backend, so it maps
+// onto the lem maybe type. If the constructors are named differently,
+// this won't work - also no other type should be created with
+// constructors named Some or None.
+
+union option ('a : Type) = {
+  Some : 'a,
+  None : unit
+}
+
+val is_none : forall ('a : Type). option('a) -> bool
+
+function is_none opt = match opt {
+  Some(_) => false,
+  None()  => true
+}
+
+val is_some : forall ('a : Type). option('a) -> bool
+
+function is_some opt = match opt {
+  Some(_) => true,
+  None()  => false
+}
+
+$endif
diff --git a/riscv/main.sail b/riscv/main.sail
index 0cc34061..8e0b0440 100644
--- a/riscv/main.sail
+++ b/riscv/main.sail
@@ -27,7 +27,7 @@ function fetch_and_execute () =
       nextPC = PC + instr_sz;
       match instr_ast {
         Some(ast) => execute(ast),
-        None      => {print("Decode failed"); exit (())}
+	None()    => {print("Decode failed"); exit()}
       }
     };
     let tohost_val = __RISCV_read(tohost, 4);
@@ -60,9 +60,9 @@ function main () = {
     fetch_and_execute()
   } catch {
     Error_not_implemented(s) => print_string("Error: Not implemented: ", s),
-    Error_misaligned_access  => print("Error: misaligned_access"),
-    Error_EBREAK => print("EBREAK"),
-    Error_internal_error => print("Error: internal error")
+    Error_misaligned_access() => print("Error: misaligned_access"),
+    Error_EBREAK() => print("EBREAK"),
+    Error_internal_error() => print("Error: internal error")
   };
   dump_state ()
 }
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 89221596..b58ebc52 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -1,7 +1,7 @@
 default Order dec
 
 type bits ('n : Int) = vector('n, dec, bit)
-union option ('a : Type) = {None, Some : 'a}
+union option ('a : Type) = {None : unit, Some : 'a}
 
 val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
@@ -330,9 +330,9 @@ val print_string = "print_string" : (string, string) -> unit
 
 union exception = {
   Error_not_implemented : string,
-  Error_misaligned_access,
-  Error_EBREAK,
-  Error_internal_error
+  Error_misaligned_access : unit,
+  Error_EBREAK : unit,
+  Error_internal_error : unit
 }
 
 val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 004621c7..21c6fd64 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -353,40 +353,40 @@ function clause execute (FENCE(pred, succ)) = {
 }
 
 /* ****************************************************************** */
-union clause ast = FENCEI
+union clause ast = FENCEI : unit
 
-function clause decode 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111 = Some(FENCEI)
+function clause decode 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111 = Some(FENCEI())
 
-function clause execute FENCEI = MEM_fence_i()
+function clause execute FENCEI() = MEM_fence_i()
 
 /* ****************************************************************** */
-union clause ast = ECALL
+union clause ast = ECALL : unit
 
-function clause decode 0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(ECALL)
+function clause decode 0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(ECALL())
 
-function clause execute ECALL =
+function clause execute ECALL() =
   let t : sync_exception =
     struct { trap = match (cur_privilege) {
                       USER => User_ECall,
 		      MACHINE => Machine_ECall
 		    },
-             excinfo = (None : option(xlenbits)) } in
+	     excinfo = (None() : option(xlenbits)) } in
   nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
 
 /* ****************************************************************** */
-union clause ast = MRET
+union clause ast = MRET : unit
 
-function clause decode 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(MRET)
+function clause decode 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(MRET())
 
-function clause execute MRET =
-  nextPC = handle_exception_ctl(cur_privilege, CTL_MRET, PC)
+function clause execute MRET() =
+  nextPC = handle_exception_ctl(cur_privilege, CTL_MRET(), PC)
 
 /* ****************************************************************** */
-union clause ast = EBREAK
+union clause ast = EBREAK : unit
 
-function clause decode 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(EBREAK)
+function clause decode 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(EBREAK())
 
-function clause execute EBREAK = { throw(Error_EBREAK) }
+function clause execute EBREAK() = { throw Error_EBREAK() }
 
 /* ****************************************************************** */
 union clause ast = LOADRES : (bool, bool, regbits, word_width, regbits)
@@ -591,22 +591,22 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) =
 
 /* ****************************************************************** */
 
-union clause ast = NOP
+union clause ast = NOP : unit
 
 function clause decodeCompressed (0b000 @ nzi1 : bits(1) @ 0b00000 @ (nzi0 : bits(5)) @ 0b01) : bits(16) = {
-  if (nzi1 == 0b0) & (nzi0 == 0b00000) then Some(NOP)
-  else None
+  if (nzi1 == 0b0) & (nzi0 == 0b00000) then Some(NOP())
+  else None()
 }
 
-function clause execute (NOP) = ()
+function clause execute NOP() = ()
 
 /* ****************************************************************** */
 
-union clause ast = ILLEGAL
+union clause ast = ILLEGAL : unit
 
-function clause decodeCompressed (0b0000 @ 0b00000 @ 0b00000 @ 0b00) : bits(16) = Some(ILLEGAL)
+function clause decodeCompressed (0b0000 @ 0b00000 @ 0b00000 @ 0b00) : bits(16) = Some(ILLEGAL())
 
-function clause execute (ILLEGAL) = {
+function clause execute ILLEGAL() = {
   let t : sync_exception =
   struct { trap = Illegal_Instr,
            excinfo = Some (EXTZ(0b0)) } in
@@ -619,7 +619,7 @@ union clause ast = C_ADDI4SPN : (cregbits, bits(8))
 
 function clause decodeCompressed (0b000 @ nz54 : bits(2) @ nz96 : bits(4) @ nz2 : bits(1) @ nz3 : bits(1) @ rd : cregbits @ 0b00) : bits(16) = {
   let nzimm = (nz96 @ nz54 @ nz3 @ nz2) : bits(8) in
-  if nzimm == 0b00000000 then None
+  if nzimm == 0b00000000 then None()
   else Some(C_ADDI4SPN(rd, nzimm))
 }
 
@@ -699,7 +699,7 @@ union clause ast = C_ADDI : (bits(6), regbits)
 
 function clause decodeCompressed (0b000 @ nzi5 : bits(1) @ rsd : regbits @ nzi40 : bits(5) @ 0b01) : bits(16) = {
   let nzi = (nzi5 @ nzi40) : bits(6) in
-  if (nzi == 0b000000) | (rsd == zreg) then None
+  if (nzi == 0b000000) | (rsd == zreg) then None()
   else Some(C_ADDI(nzi, rsd))
 }
 
@@ -735,7 +735,7 @@ function clause execute (C_ADDIW(imm, rsd)) = {
 union clause ast = C_LI : (bits(6), regbits)
 
 function clause decodeCompressed (0b010 @ imm5 : bits(1) @ rd : regbits @ imm40 : bits(5) @ 0b01) = {
-  if (rd == zreg) then None
+  if (rd == zreg) then None()
   else Some(C_LI(imm5 @ imm40, rd))
 }
 
@@ -750,7 +750,7 @@ union clause ast = C_ADDI16SP : (bits(6))
 
 function clause decodeCompressed (0b011 @ nzi9 : bits(1) @ /* x2 */ 0b00010 @ nzi4 : bits(1) @ nzi6 : bits(1) @ nzi87 : bits(2) @ nzi5 : bits(1) @ 0b01) = {
   let nzimm = nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 in
-  if (nzimm == 0b000000) then None
+  if (nzimm == 0b000000) then None()
   else Some(C_ADDI16SP(nzimm))
 }
 
@@ -764,7 +764,7 @@ function clause execute (C_ADDI16SP(imm)) = {
 union clause ast = C_LUI : (bits(6), regbits)
 
 function clause decodeCompressed (0b011 @ imm17 : bits(1) @ rd : regbits @ imm1612 : bits(5) @ 0b01) = {
-  if (rd == zreg) | (rd == sp) then None
+  if (rd == zreg) | (rd == sp) then None()
   else Some(C_LUI(imm17 @ imm1612, rd))
 }
 
@@ -780,7 +780,7 @@ union clause ast = C_SRLI : (bits(6), cregbits)
 function clause decodeCompressed (0b100 @ nzui5 : bits(1) @ 0b00 @ rsd : cregbits @ nzui40 : bits(5) @ 0b01) = {
   let shamt : bits(6) = nzui5 @ nzui40 in
   if shamt == 0b000000 /* TODO: On RV32, also need shamt[5] == 0 */
-  then None
+  then None()
   else Some(C_SRLI(shamt, rsd))
 }
 
@@ -796,7 +796,7 @@ union clause ast = C_SRAI : (bits(6), cregbits)
 function clause decodeCompressed (0b100 @ nzui5 : bits(1) @ 0b01 @ rsd : cregbits @ nzui40 : bits(5) @ 0b01) = {
   let shamt : bits(6) = nzui5 @ nzui40 in
   if shamt == 0b000000 /* TODO: On RV32, also need shamt[5] == 0 */
-  then None
+  then None()
   else Some(C_SRAI(shamt, rsd))
 }
 
@@ -927,7 +927,7 @@ union clause ast = C_SLLI : (bits(6), regbits)
 function clause decodeCompressed (0b000 @ nzui5 : bits(1) @ rsd : regbits @ nzui40 : bits(5) @ 0b10) = {
   let shamt : bits(6) = nzui5 @ nzui40 in
   if shamt == 0b000000 | rsd == zreg /* TODO: On RV32, also need shamt[5] == 0 */
-  then None
+  then None()
   else Some(C_SLLI(shamt, rsd))
 }
 
@@ -941,7 +941,7 @@ union clause ast = C_LWSP : (bits(6), regbits)
 function clause decodeCompressed (0b010 @ ui5 : bits(1) @ rd : regbits @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10) = {
   let uimm : bits(6) = ui76 @ ui5 @ ui42 in
   if  rd == zreg
-  then None
+  then None()
   else Some(C_LWSP(uimm, rd))
 }
 
@@ -957,7 +957,7 @@ union clause ast = C_LDSP : (bits(6), regbits)
 function clause decodeCompressed (0b011 @ ui5 : bits(1) @ rd : regbits @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10) = {
   let uimm : bits(6) = ui86 @ ui5 @ ui43 in
   if  rd == zreg
-  then None
+  then None()
   else Some(C_LDSP(uimm, rd))
 }
 
@@ -1000,7 +1000,7 @@ union clause ast = C_JR : (regbits)
 
 function clause decodeCompressed (0b100 @ 0b0 @ rs1 : regbits @ 0b00000 @ 0b10) = {
   if rs1 == zreg
-  then None
+  then None()
   else Some(C_JR(rs1))
 }
 
@@ -1013,7 +1013,7 @@ union clause ast = C_JALR : (regbits)
 
 function clause decodeCompressed (0b100 @ 0b1 @ rs1 : regbits @ 0b00000 @ 0b10) = {
   if rs1 == zreg
-  then None
+  then None()
   else Some(C_JALR(rs1))
 }
 
@@ -1026,7 +1026,7 @@ union clause ast = C_MV : (regbits, regbits)
 
 function clause decodeCompressed (0b100 @ 0b0 @ rd : regbits @ rs2 : regbits @ 0b10) = {
   if rs2 == zreg | rd == zreg
-  then None
+  then None()
   else Some(C_MV(rd, rs2))
 }
 
@@ -1039,7 +1039,7 @@ union clause ast = C_ADD : (regbits, regbits)
 
 function clause decodeCompressed (0b100 @ 0b1 @ rsd : regbits @ rs2 : regbits @ 0b10) = {
   if rsd == zreg | rs2 == zreg
-  then None
+  then None()
   else Some(C_ADD(rsd, rs2))
 }
 
@@ -1048,8 +1048,8 @@ function clause execute (C_ADD(rsd, rs2)) =
 
 /* ****************************************************************** */
 
-function clause decode _ = None
-function clause decodeCompressed _ = None
+function clause decode _ = None()
+function clause decodeCompressed _ = None()
 
 end ast
 end decode
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 2956caae..4a80bf3a 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -221,15 +221,16 @@ union ctl_result = {
   CTL_URET,
   CTL_SRET,
 */
-  CTL_MRET
+  CTL_MRET : unit
 }
 
 /* privilege level */
 
-union privilege = {
+enum privilege = {
   MACHINE,
   USER
 }
+
 register cur_privilege : privilege
 
 function priv_to_bits(p : privilege) -> bits(2) =
@@ -262,19 +263,19 @@ function handle_exception_ctl(cur_priv : privilege, ctl : ctl_result,
         Misaligned_Fetch => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
         Fetch_Access => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
         Illegal_Instr => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
 
@@ -283,25 +284,25 @@ function handle_exception_ctl(cur_priv : privilege, ctl : ctl_result,
         Misaligned_Load => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
         Load_Access => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
         Misaligned_Store => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
         Store_Access => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
 
@@ -318,27 +319,27 @@ function handle_exception_ctl(cur_priv : privilege, ctl : ctl_result,
         Fetch_PageFault => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
         Load_PageFault => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
         Store_PageFault => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
-        _ => throw(Error_internal_error) /* Don't expect ReservedExc0 etc. here */
+        _ => throw Error_internal_error() /* Don't expect ReservedExc0 etc. here */
       };
       /* TODO: make register read explicit */
       mtvec
     },
-    (_, CTL_MRET) => {
+    (_, CTL_MRET()) => {
       mstatus->MIE()  = mstatus.MPIE();
       mstatus->MPIE() = true;
       cur_privilege   = bits_to_priv(mstatus.MPP());
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index 944c7455..8799f580 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -5,7 +5,7 @@ function not_implemented message = throw(Error_not_implemented(message))
 val internal_error : forall ('a : Type). string -> 'a effect {escape}
 function internal_error(s) = {
     assert (false, s);
-    throw (Error_internal_error)
+    throw Error_internal_error()
 }
 
 let xlen = 64
@@ -51,7 +51,7 @@ function wX (r, v) =
 overload X = {rX, wX}
 
 function check_alignment (addr : xlenbits, width : atom('n)) -> forall 'n. unit =
-  if unsigned(addr) % width != 0 then throw(Error_misaligned_access) else ()
+  if unsigned(addr) % width != 0 then throw Error_misaligned_access() else ()
 
 val MEMr                         : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
 val MEMr_acquire                 : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 1c74381f..591e8df2 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -54,7 +54,7 @@ module Big_int = Nat_big_num
 
 type mut = Immutable | Mutable
 
-type lvar = Register of typ | Enum of typ | Local of mut * typ | Union of typquant * typ | Unbound
+type lvar = Register of typ | Enum of typ | Local of mut * typ | Unbound
 
 let no_annot = (Parse_ast.Unknown, ())
 
@@ -1009,10 +1009,7 @@ let split_defs f (Defs defs) =
 let append_ast (Defs ast1) (Defs ast2) = Defs (ast1 @ ast2)
 let concat_ast asts = List.fold_right append_ast asts (Defs [])
 
-let type_union_id (Tu_aux (aux, _)) = match aux with
-  | Tu_id id -> id
-  | Tu_ty_id (_, id) -> id
-
+let type_union_id (Tu_aux (Tu_ty_id (_, id), _)) = id
 
 let rec subst id value (E_aux (e_aux, annot) as exp) =
   let wrap e_aux = E_aux (e_aux, annot) in
diff --git a/src/ast_util.mli b/src/ast_util.mli
index d1827685..de925fc3 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -58,7 +58,7 @@ type mut = Immutable | Mutable
 (** [lvar] is the type of variables - they can either be registers,
    local mutable or immutable variables, nullary union constructors
    (i.e. None in option), or unbound identifiers *)
-type lvar = Register of typ | Enum of typ | Local of mut * typ | Union of typquant * typ | Unbound
+type lvar = Register of typ | Enum of typ | Local of mut * typ | Unbound
 
 val no_annot : unit annot
 val gen_loc : Parse_ast.l -> Parse_ast.l
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 33f6f127..2542dd42 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -80,7 +80,6 @@ let lvar_typ = function
   | Local (_, typ) -> typ
   | Register typ -> typ
   | Enum typ -> typ
-  (* | Union (_, typ) -> typ *)
   | _ -> assert false
 
 let string_of_value = function
@@ -348,8 +347,6 @@ let pp_lvar lvar doc =
      string "[I/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc
   | Enum typ ->
      string "[E/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc
-  | Union (typq, typ) ->
-     string "[U/" ^^ string (string_of_typquant typq ^ "/" ^ string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc
   | Unbound -> string "[?]" ^^ doc
 
 let pp_annot typ doc =
@@ -627,7 +624,6 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) =
   | E_id id ->
      let lvar = Env.lookup_id id (env_of exp) in
      begin match lvar with
-     | Union (_, typ) -> AE_app (id, [AV_lit (mk_lit L_unit, unit_typ)], typ)
      | _ -> AE_val (AV_id (id, lvar))
      end
 
@@ -1123,16 +1119,7 @@ let cdef_ctyps ctx = function
   | CDEF_reg_dec (_, ctyp) -> [ctyp]
   | CDEF_spec (_, ctyps, ctyp) -> ctyp :: ctyps
   | CDEF_fundef (id, _, _, instrs) ->
-     (* TODO: Move this code to DEF_fundef -> CDEF_fundef translation, and modify bytecode.ott *)
-     let _, Typ_aux (fn_typ, _) =
-       try Env.get_val_spec id ctx.tc_env with
-       | Type_error _ ->
-          (* If we can't find the function type, then it must be a nullary union constructor. *)
-          begin match Env.lookup_id id ctx.tc_env with
-          | Union (typq, typ) -> typq, function_typ unit_typ typ no_effect
-          | _ -> failwith ("Got function identifier " ^ string_of_id id ^ " which is neither a function nor a constructor.")
-          end
-     in
+     let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
      let arg_typs, ret_typ = match fn_typ with
        | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ
        | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ
@@ -1455,15 +1442,7 @@ let compile_funcall ctx id args typ =
   let setup = ref [] in
   let cleanup = ref [] in
 
-  let _, Typ_aux (fn_typ, _) =
-    try Env.get_val_spec id ctx.tc_env with
-    | Type_error _ ->
-       (* If we can't find the function type, then it must be a nullary union constructor. *)
-       begin match Env.lookup_id id ctx.tc_env with
-       | Union (typq, typ) -> typq, function_typ unit_typ typ no_effect
-       | _ -> failwith ("Got function identifier " ^ string_of_id id ^ " which is neither a function nor a constructor.")
-       end
-  in
+  let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
   let arg_typs, ret_typ = match fn_typ with
     | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ
     | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ
@@ -1892,11 +1871,7 @@ let compile_type_def ctx (TD_aux (type_def, _)) =
      { ctx with records = Bindings.add id ctors ctx.records }
 
   | TD_variant (id, _, _, tus, _) ->
-     let compile_tu (Tu_aux (tu_aux, _)) =
-       match tu_aux with
-       | Tu_id id -> CT_unit, id
-       | Tu_ty_id (typ, id) -> ctyp_of_typ ctx typ, id
-     in
+     let compile_tu (Tu_aux (Tu_ty_id (typ, id), _)) = ctyp_of_typ ctx typ, id in
      let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in
      CTD_variant (id, Bindings.bindings ctus),
      { ctx with variants = Bindings.add id ctus ctx.variants }
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 9da200d9..0019f18f 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -648,15 +648,9 @@ let rec to_ast_range (Parse_ast.BF_aux(r,l)) = (* TODO add check that ranges are
     | Parse_ast.BF_concat(ir1,ir2) -> BF_concat( to_ast_range ir1, to_ast_range ir2)),
     l)
 
-let to_ast_type_union k_env default_order (Parse_ast.Tu_aux(tu,l)) =
-  match tu with
-  | Parse_ast.Tu_ty_id(atyp,id) ->
-    let typ = to_ast_typ k_env default_order atyp in
-    (match typ with
-     | Typ_aux(Typ_id (Id_aux (Id "unit",_)),_) ->
-       Tu_aux(Tu_id(to_ast_id id),l)
-     | _ -> Tu_aux(Tu_ty_id(typ, to_ast_id id), l))
-  | Parse_ast.Tu_id id -> (Tu_aux(Tu_id(to_ast_id id),l))
+let to_ast_type_union k_env default_order (Parse_ast.Tu_aux (Parse_ast.Tu_ty_id (atyp, id), l)) =
+  let typ = to_ast_typ k_env default_order atyp in
+  Tu_aux (Tu_ty_id (typ, to_ast_id id), l)
 
 let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (unit type_def) envs_out =
   match td with
@@ -1042,7 +1036,6 @@ let generate_undefineds vs_ids (Defs defs) =
       end
   in
   let undefined_tu = function
-    | Tu_aux (Tu_id id, _) -> mk_exp (E_id id)
     | Tu_aux (Tu_ty_id (Typ_aux (Typ_tup typs, _), id), _) ->
        mk_exp (E_app (id, List.map (fun _ -> mk_lit_exp L_undef) typs))
     | Tu_aux (Tu_ty_id (typ, id), _) -> mk_exp (E_app (id, [mk_lit_exp L_undef]))
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 55dcbed0..2b24d66c 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -415,7 +415,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
        | Local (Immutable, _) ->
           let chain = build_letchain id gstate.letbinds orig_exp in
           return chain
-       | Enum _ | Union _ ->
+       | Enum _ ->
           return (exp_of_value (V_ctor (string_of_id id, [])))
        | _ -> failwith ("id " ^ string_of_id id)
      end
@@ -568,7 +568,7 @@ and pattern_match env (P_aux (p_aux, _) as pat) value =
      let open Type_check in
      begin
        match Env.lookup_id id env with
-       | Enum _ | Union _ ->
+       | Enum _ ->
           if is_ctor value && string_of_id id = fst (coerce_ctor value)
           then true, Bindings.empty
           else false, Bindings.empty
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 45541585..0d63a9c3 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -165,9 +165,7 @@ let pat_id_is_variable env id =
   | Local _
   | Register _
     -> true
-  | Enum _
-  | Union _
-    -> false
+  | Enum _ -> false
 
 let rec is_value (E_aux (e,(l,annot))) =
   let is_constructor id =
@@ -179,7 +177,7 @@ let rec is_value (E_aux (e,(l,annot))) =
     | Some (env,_,_) ->
        Env.is_union_constructor id env ||
          (match Env.lookup_id id env with
-         | Enum _ | Union _ -> true 
+         | Enum _ -> true
          | Unbound | Local _ | Register _ -> false)
   in
   match e with
@@ -1118,15 +1116,12 @@ let is_env_inconsistent env ksubsts =
 let split_defs all_errors splits defs =
   let no_errors_happened = ref true in
   let split_constructors (Defs defs) =
-    let sc_type_union q (Tu_aux (tu,l) as tua) =
-      match tu with
-      | Tu_id id -> [],[tua]
-      | Tu_ty_id (ty,id) ->
-         (match split_src_type id ty q with
-         | None -> ([],[Tu_aux (Tu_ty_id (ty,id),l)])
-         | Some variants ->
-            ([(id,variants)],
-             List.map (fun (insts, id', ty) -> Tu_aux (Tu_ty_id (ty,id'),Generated l)) variants))
+    let sc_type_union q (Tu_aux (Tu_ty_id (ty, id), l) as tua) =
+      match split_src_type id ty q with
+      | None -> ([],[Tu_aux (Tu_ty_id (ty,id),l)])
+      | Some variants ->
+         ([(id,variants)],
+          List.map (fun (insts, id', ty) -> Tu_aux (Tu_ty_id (ty,id'),Generated l)) variants)
     in
     let sc_type_def ((TD_aux (tda,annot)) as td) =
       match tda with
@@ -2799,7 +2794,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
             | args -> (args,assigns,empty)
             | exception Not_found ->
                match Env.lookup_id id (Type_check.env_of_annot (l,annot)) with
-               | Enum _ | Union _ -> dempty,assigns,empty
+               | Enum _ -> dempty,assigns,empty
                | Register _ -> Unknown (l, string_of_id id ^ " is a register"),assigns,empty
                | _ ->
                   Unknown (l, string_of_id id ^ " is not in the environment"),assigns,empty
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 795b6300..c580b9fa 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -177,7 +177,6 @@ let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) =
        match Env.lookup_id id (pat_env_of pat) with
        | Local (Immutable, _) | Unbound -> zencode ctx id
        | Enum _ -> zencode_upper ctx id
-       | Union _ -> zencode_upper ctx id
        | _ -> failwith ("Ocaml: Cannot pattern match on mutable variable or register:" ^ string_of_pat pat)
      end
   | P_lit lit -> ocaml_lit lit
@@ -315,7 +314,7 @@ and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) =
      begin
        match Env.lookup_id id (env_of exp) with
        | Local (Immutable, _) | Unbound -> zencode ctx id
-       | Enum _ | Union _ -> zencode_upper ctx id
+       | Enum _ -> zencode_upper ctx id
        | Register _ when is_passed_by_name (typ_of exp) -> zencode ctx id
        | Register typ ->
           if !opt_trace_ocaml then
@@ -515,9 +514,8 @@ let rec ocaml_fields ctx =
   | [] -> empty
 
 let rec ocaml_cases ctx =
-  let ocaml_case = function
-    | Tu_aux (Tu_id id, _) -> separate space [bar; zencode_upper ctx id]
-    | Tu_aux (Tu_ty_id (typ, id), _) -> separate space [bar; zencode_upper ctx id; string "of"; ocaml_typ ctx typ]
+  let ocaml_case (Tu_aux (Tu_ty_id (typ, id), _)) =
+    separate space [bar; zencode_upper ctx id; string "of"; ocaml_typ ctx typ]
   in
   function
   | [tu] -> ocaml_case tu
@@ -525,10 +523,8 @@ let rec ocaml_cases ctx =
   | [] -> empty
 
 let rec ocaml_exceptions ctx =
-  let ocaml_exception = function
-    | Tu_aux (Tu_id id, _) -> separate space [string "exception"; zencode_upper ctx id]
-    | Tu_aux (Tu_ty_id (typ, id), _) ->
-       separate space [string "exception"; zencode_upper ctx id; string "of"; ocaml_typ ctx typ]
+  let ocaml_exception (Tu_aux (Tu_ty_id (typ, id), _)) =
+    separate space [string "exception"; zencode_upper ctx id; string "of"; ocaml_typ ctx typ]
   in
   function
   | [tu] -> ocaml_exception tu
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index ba948040..635aa46e 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -361,8 +361,7 @@ funcl_aux =  (* Function clause *)
 
 type 
 type_union_aux =  (* Type union constructors *)
-   Tu_id of id
- | Tu_ty_id of atyp * id
+   Tu_ty_id of atyp * id
 
 
 type 
diff --git a/src/parser.mly b/src/parser.mly
index c8cc49a3..7e4874f8 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -677,6 +677,8 @@ atomic_pat:
   | kid
     { mk_pat (P_var (mk_pat (P_id (id_of_kid $1)) $startpos $endpos,
 		     mk_typ (ATyp_var $1) $startpos $endpos)) $startpos $endpos }
+  | id Unit
+    { mk_pat (P_app ($1, [mk_pat P_wild $startpos $endpos])) $startpos $endpos }
   | id Lparen pat_list Rparen
     { mk_pat (P_app ($1, $3)) $startpos $endpos }
   | atomic_pat Colon typ
@@ -999,6 +1001,8 @@ atomic_exp:
     { mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos }
   | id Lparen exp_list Rparen
     { mk_exp (E_app ($1, $3)) $startpos $endpos }
+  | Exit Unit
+    { mk_exp (E_exit (mk_lit_exp L_unit $startpos $endpos)) $startpos $endpos }
   | Exit Lparen exp Rparen
     { mk_exp (E_exit $3) $startpos $endpos }
   | Sizeof Lparen typ Rparen
@@ -1155,8 +1159,6 @@ struct_fields:
 type_union:
   | id Colon typ
     { Tu_aux (Tu_ty_id ($3, $1), loc $startpos $endpos) }
-  | id
-    { Tu_aux (Tu_id $1, loc $startpos $endpos) }
 
 type_unions:
   | type_union
diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml
index 94623e6f..c13452ff 100644
--- a/src/pattern_completeness.ml
+++ b/src/pattern_completeness.ml
@@ -97,7 +97,7 @@ let rec generalize ctx (P_aux (p_aux, _) as pat) =
        | Unbound -> GP_wild
        | Local (Immutable, _) -> GP_wild
        | Register _ | Local (Mutable, _) -> Util.warn "Matching on register or mutable variable"; GP_wild
-       | Enum _ | Union _ -> GP_app (Bindings.singleton id GP_wild)
+       | Enum _ -> GP_app (Bindings.singleton id GP_wild)
      end
   | P_var (pat, _) -> generalize ctx pat
   | P_vector pats ->
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index a0390a94..f2136f07 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -445,24 +445,22 @@ let doc_typschm_lem quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
   else pt
 
 let is_ctor env id = match Env.lookup_id id env with
-| Enum _ | Union _ -> true
+| Enum _ -> true
 | _ -> false
 
 (*Note: vector concatenation, literal vectors, indexed vectors, and record should
   be removed prior to pp. The latter two have never yet been seen
 *)
 let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with
+  | P_app(id, _) when string_of_id id = "None" -> string "Nothing"
   | P_app(id, ((_ :: _) as pats)) ->
     let ppp = doc_unop (doc_id_lem_ctor id)
                        (parens (separate_map comma (doc_pat_lem ctxt true) pats)) in
     if apat_needed then parens ppp else ppp
-  | P_app(id,[]) -> doc_id_lem_ctor id
+  | P_app(id, []) -> doc_id_lem_ctor id
   | P_lit lit  -> doc_lit_lem lit
   | P_wild -> underscore
-  | P_id id ->
-     begin match id with
-     | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
-     | _ -> doc_id_lem id end
+  | P_id id -> doc_id_lem id
   | P_var(p,_) -> doc_pat_lem ctxt true p
   | P_as(p,id) -> parens (separate space [doc_pat_lem ctxt true p; string "as"; doc_id_lem id])
   | P_typ(Typ_aux (Typ_tup typs, _), P_aux (P_tup pats, _)) ->
@@ -614,6 +612,7 @@ let doc_exp_lem, doc_let_lem =
     | E_app(f,args) ->
        begin match f with
        (* temporary hack to make the loop body a function of the temporary variables *)
+       | Id_aux (Id "None", _) as none -> doc_id_lem_ctor none
        | Id_aux (Id "foreach", _) ->
           begin
             match args with
@@ -681,7 +680,7 @@ let doc_exp_lem, doc_let_lem =
           end
        | _ ->
           begin match annot with
-          | Some (env, _, _) when (is_ctor env f) ->
+          | Some (env, _, _) when Env.is_union_constructor f env ->
              let epp =
                match args with
                | [] -> doc_id_lem_ctor f
@@ -899,10 +898,9 @@ let doc_exp_lem, doc_let_lem =
   in top_exp, let_exp
 
 (*TODO Upcase and downcase type and constructors as needed*)
-let doc_type_union_lem (Tu_aux(typ_u,_)) = match typ_u with
-  | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor id; string "of";
-                                        parens (doc_typ_lem typ)]
-  | Tu_id id -> separate space [pipe; doc_id_lem_ctor id]
+let doc_type_union_lem (Tu_aux(Tu_ty_id(typ,id),_)) =
+  separate space [pipe; doc_id_lem_ctor id; string "of";
+                  parens (doc_typ_lem typ)]
 
 let rec doc_range_lem (BF_aux(r,_)) = match r with
   | BF_single i -> parens (doc_op comma (doc_int i) (doc_int i))
@@ -995,19 +993,12 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
              (separate space [string "let rec";fromInterpValueF;string "v";equals;string "match v with"])
              (
                ((separate_map (break 1))
-                  (fun (Tu_aux (tu,_)) ->
-                    match tu with
-                    | Tu_ty_id (ty,cid) ->
-                       (separate space)
-                         [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
-                          arrow;
-                          doc_id_lem_ctor cid;
-                          parens (string "fromInterpValue v")]
-                    | Tu_id cid ->
-                       (separate space)
-                         [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
-                          arrow;
-                          doc_id_lem_ctor cid])
+                  (fun (Tu_aux (Tu_ty_id (ty,cid),_)) ->
+                    (separate space)
+                      [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
+                       arrow;
+                       doc_id_lem_ctor cid;
+                       parens (string "fromInterpValue v")])
                   ar) ^/^
 
                   ((separate space) [pipe;string "SI.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^
@@ -1024,24 +1015,14 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
              (separate space [string "let";toInterpValueF;equals;string "function"])
              (
                ((separate_map (break 1))
-                  (fun (Tu_aux (tu,_)) ->
-                    match tu with
-                    | Tu_ty_id (ty,cid) ->
-                       (separate space)
-                         [pipe;doc_id_lem_ctor cid;string "v";arrow;
-                          string "SI.V_ctor";
-                          parens (make_id false cid);
-                          parens (string "SIA.T_id " ^^ string_lit (doc_id id));
-                          string "SI.C_Union";
-                          parens (string "toInterpValue v")]
-                    | Tu_id cid ->
-                       (separate space)
-                         [pipe;doc_id_lem_ctor cid;arrow;
-                          string "SI.V_ctor";
-                          parens (make_id false cid);
-                          parens (string "SIA.T_id " ^^ string_lit (doc_id id));
-                          string "SI.C_Union";
-                          parens (string "toInterpValue ()")])
+                  (fun (Tu_aux (Tu_ty_id (ty,cid),_)) ->
+                    (separate space)
+                      [pipe;doc_id_lem_ctor cid;string "v";arrow;
+                       string "SI.V_ctor";
+                       parens (make_id false cid);
+                       parens (string "SIA.T_id " ^^ string_lit (doc_id id));
+                       string "SI.C_Union";
+                       parens (string "toInterpValue v")])
                   ar) ^/^
                  string "end") in
          let fromToInterpValuePP =
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 63661bb9..559c1116 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -517,11 +517,9 @@ let pp_lem_typdef ppf (TD_aux(td,(l,annot))) =
         fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
           kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs
       | TD_variant(id,nm,typq,ar,_) ->
-        let a_pp ppf (Tu_aux(typ_u,l)) =
-          match typ_u with
-            | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]"
-                                  pp_lem_typ typ pp_lem_id id pp_lem_l l
-            | Tu_id(id) -> fprintf ppf "@[<1>(Tu_aux (Tu_id %a) %a);@]" pp_lem_id id pp_lem_l l
+        let a_pp ppf (Tu_aux(Tu_ty_id(typ,id),l)) =
+          fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]"
+                  pp_lem_typ typ pp_lem_id id pp_lem_l l
         in
         fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
           kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 7620ca50..29284262 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -456,9 +456,7 @@ let doc_dec (DEC_aux (reg,_)) =
 let doc_field (typ, id) =
   separate space [doc_id id; colon; doc_typ typ]
 
-let doc_union (Tu_aux (tu, l)) = match tu with
-  | Tu_id id -> doc_id id
-  | Tu_ty_id (typ, id) -> separate space [doc_id id; colon; doc_typ typ]
+let doc_union (Tu_aux (Tu_ty_id (typ, id), l)) = separate space [doc_id id; colon; doc_typ typ]
 
 let doc_typdef (TD_aux(td,_)) = match td with
   | TD_abbrev (id, _, typschm) ->
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 50a8ae68..0b4a864c 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1952,10 +1952,8 @@ let rewrite_constraint =
 
   rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_e_constraint) }
 
-let rewrite_type_union_typs rw_typ (Tu_aux (tu, annot)) =
-  match tu with
-  | Tu_id id -> Tu_aux (Tu_id id, annot)
-  | Tu_ty_id (typ, id) -> Tu_aux (Tu_ty_id (rw_typ typ, id), annot)
+let rewrite_type_union_typs rw_typ (Tu_aux (Tu_ty_id (typ, id), annot)) =
+  Tu_aux (Tu_ty_id (rw_typ typ, id), annot)
 
 let rewrite_type_def_typs rw_typ rw_typquant rw_typschm (TD_aux (td, annot)) =
   match td with
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 371acfdc..74312d9b 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -289,9 +289,7 @@ let init_env s = Nameset.singleton s
 
 let typ_variants consider_var bound tunions =
   List.fold_right
-    (fun (Tu_aux(t,_)) (b,n) -> match t with
-       | Tu_id id -> Nameset.add (string_of_id id) b,n
-       | Tu_ty_id(t,id) -> Nameset.add (string_of_id id) b, fv_of_typ consider_var b n t)
+    (fun (Tu_aux(Tu_ty_id(t,id),_)) (b,n) -> Nameset.add (string_of_id id) b, fv_of_typ consider_var b n t)
     tunions
     (bound,mt)
 
diff --git a/src/state.ml b/src/state.ml
index 690c7948..8e024179 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -144,7 +144,7 @@ let add_regval_conv id typ defs =
   let from_val = Printf.sprintf "val %s : register_value -> option(%s)" from_name typ_str in
   let from_function = String.concat "\n" [
     Printf.sprintf "function %s Regval_%s(v) = Some(v)" from_name id;
-    Printf.sprintf "and %s _ = None" from_name
+    Printf.sprintf "and %s _ = None()" from_name
     ] in
   let from_defs = if is_defined from_name then [] else [from_val; from_function] in
   (* Create a function that converts from target type to regval. *)
@@ -316,7 +316,7 @@ let generate_regstate_defs mwords defs =
   let regtyps = register_base_types mwords (List.map fst registers) in
   let option_typ =
     if has_def "option" then [] else
-      ["union option ('a : Type) = {None, Some : 'a}"]
+      ["union option ('a : Type) = {None : unit, Some : 'a}"]
   in
   let regval_typ = if has_def "register_value" then [] else generate_regval_typ regtyps in
   let regstate_typ = if has_def "regstate" then [] else generate_regstate registers in
diff --git a/src/type_check.ml b/src/type_check.ml
index 16e5bed2..ff4240aa 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -674,7 +674,6 @@ end = struct
 
   let is_union_constructor id env =
     let is_ctor id (Tu_aux (tu, _)) = match tu with
-      | Tu_id ctor_id when Id.compare id ctor_id = 0 -> true
       | Tu_ty_id (_, ctor_id) when Id.compare id ctor_id = 0 -> true
       | _ -> false
     in
@@ -835,14 +834,7 @@ end = struct
                 let (enum, _) = List.find (fun (enum, ctors) -> IdSet.mem id ctors) (Bindings.bindings env.enums) in
                 Enum (mk_typ (Typ_id enum))
               with
-              | Not_found ->
-                 begin
-                   try
-                     let (typq, typ) = freshen_bind env (Bindings.find id env.union_ids) in
-                     Union (typq, typ)
-                   with
-                   | Not_found -> Unbound
-                 end
+              | Not_found -> Unbound
             end
        end
 
@@ -2024,11 +2016,6 @@ let rec filter_casts env from_typ to_typ casts =
      end
   | [] -> []
 
-let is_union_id id env =
-  match Env.lookup_id id env with
-  | Union (_, _) -> true
-  | _ -> false
-
 let crule r env exp typ =
   incr depth;
   typ_print ("Check " ^ string_of_exp exp ^ " <= " ^ string_of_typ typ);
@@ -2246,14 +2233,6 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
      if is_typ_monomorphic typ || Env.polymorphic_undefineds env
      then annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef])
      else typ_error l ("Type " ^ string_of_typ typ ^ " failed undefined monomorphism restriction")
-  | E_id id, _ when is_union_id id env ->
-     begin
-       match Env.lookup_id id env with
-       | Union (typq, ctor_typ) ->
-          let inferred_exp = fst (infer_funapp' l env id (typq, mk_typ (Typ_fn (unit_typ, ctor_typ, no_effect))) [mk_lit_exp L_unit] (Some typ)) in
-          annot_exp (E_id id) (typ_of inferred_exp)
-       | _ -> assert false (* Unreachble due to guard *)
-     end
   | _, _ ->
      let inferred_exp = irule infer_exp env exp in
      type_coercion env inferred_exp typ
@@ -2381,19 +2360,18 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
   match pat_aux with
   | P_id v ->
      begin
+       (* If the identifier we're matching on is also a constructor of
+          a union, that's probably a mistake, so warn about it. *)
+       if Env.is_union_constructor v env then
+         Util.warn (Printf.sprintf "Identifier %s found in pattern is also a union constructor at %s\n"
+                                   (string_of_id v)
+                                   (Reporting_basic.loc_to_string l))
+       else ();
        match Env.lookup_id v env with
        | Local (Immutable, _) | Unbound -> annot_pat (P_id v) typ, Env.add_local v (Immutable, typ) env, []
        | Local (Mutable, _) | Register _ ->
           typ_error l ("Cannot shadow mutable local or register in switch statement pattern " ^ string_of_pat pat)
        | Enum enum -> subtyp l env enum typ; annot_pat (P_id v) typ, env, []
-       | Union (typq, ctor_typ) ->
-          begin
-            try
-              let _ = unify l env ctor_typ typ in
-              annot_pat (P_id v) typ, env, []
-            with
-            | Unification_error (l, m) -> typ_error l ("Unification error when pattern matching against union constructor: " ^ m)
-          end
      end
   | P_var (pat, typ_pat) ->
      let typ = Env.expand_synonyms env typ in
@@ -2523,7 +2501,7 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
   | P_id v ->
      begin
        match Env.lookup_id v env with
-       | Local (Immutable, _) | Unbound | Union _ ->
+       | Local (Immutable, _) | Unbound ->
           typ_error l ("Cannot infer identifier in pattern " ^ string_of_pat pat ^ " - try adding a type annotation")
        | Local (Mutable, _) | Register _ ->
           typ_error l ("Cannot shadow mutable local or register in switch statement pattern " ^ string_of_pat pat)
@@ -2617,7 +2595,6 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
               let is_immutable, vtyp, is_register = match Env.lookup_id v env with
                 | Unbound -> typ_error l "Cannot assign to element of unbound vector"
                 | Enum _ -> typ_error l "Cannot vector assign to enumeration element"
-                | Union _ -> typ_error l "Cannot vector assign to union element"
                 | Local (Immutable, vtyp) -> true, vtyp, false
                 | Local (Mutable, vtyp) -> false, vtyp, false
                 | Register vtyp -> false, vtyp, true
@@ -2678,8 +2655,8 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
      end
   | LEXP_id v ->
      begin match Env.lookup_id v env with
-     | Local (Immutable, _) | Enum _ | Union _ ->
-        typ_error l ("Cannot modify let-bound constant, union or enumeration constructor " ^ string_of_id v)
+     | Local (Immutable, _) | Enum _ ->
+        typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
      | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env
      | Register vtyp -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]), env
      | Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env
@@ -2687,8 +2664,8 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
   | LEXP_cast (typ_annot, v) ->
      begin
        match Env.lookup_id v env with
-       | Local (Immutable, _) | Enum _ | Union _ ->
-          typ_error l ("Cannot modify let-bound constant, union or enumeration constructor " ^ string_of_id v)
+       | Local (Immutable, _) | Enum _ ->
+          typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
        | Local (Mutable, vtyp) ->
           begin
             subtyp l env typ typ_annot;
@@ -2732,8 +2709,8 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
                  | LEXP_aux (LEXP_id v, _) ->
                     begin
                       match Env.lookup_id v env with
-                      | Local (Immutable, _) | Enum _ | Union _ ->
-                         typ_error l ("Cannot modify let-bound constant, union or enumeration constructor " ^ string_of_id v)
+                      | Local (Immutable, _) | Enum _ ->
+                         typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
                       | Unbound ->
                          typ_error l "Unbound variable in vector tuple assignment"
                       | Local (Mutable, vtyp) | Register vtyp ->
@@ -2773,7 +2750,6 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
        let is_immutable, is_register, vtyp = match Env.lookup_id v env with
          | Unbound -> typ_error l "Cannot assign to element of unbound vector"
          | Enum _ -> typ_error l "Cannot vector assign to enumeration element"
-         | Union _ -> typ_error l "Cannot vector assign to union element"
          | Local (Immutable, vtyp) -> true, false, vtyp
          | Local (Mutable, vtyp) -> false, false, vtyp
          | Register vtyp -> false, true, vtyp
@@ -2798,7 +2774,6 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
        let is_immutable, is_register, vtyp = match Env.lookup_id v env with
          | Unbound -> typ_error l "Cannot assign to element of unbound vector"
          | Enum _ -> typ_error l "Cannot vector assign to enumeration element"
-         | Union _ -> typ_error l "Cannot vector assign to union element"
          | Local (Immutable, vtyp) -> true, false, vtyp
          | Local (Mutable, vtyp) -> false, false, vtyp
          | Register vtyp -> false, true, vtyp
@@ -2840,10 +2815,6 @@ 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 (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)])))
@@ -3610,7 +3581,6 @@ let fold_union_quant quants (QI_aux (qi, l)) =
 let check_type_union env variant typq (Tu_aux (tu, l)) =
   let ret_typ = app_typ variant (List.fold_left fold_union_quant [] (quant_items typq)) in
   match tu with
-  | Tu_id v -> Env.add_union_id v (typq, ret_typ) env
   | Tu_ty_id (typ, v) ->
      let typ' = mk_typ (Typ_fn (typ, ret_typ, no_effect)) in
      env
diff --git a/src/value.ml b/src/value.ml
index 077ad883..f865fea1 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -434,6 +434,7 @@ let primops =
       ("sub_vec", value_sub_vec);
       ("read_ram", value_read_ram);
       ("write_ram", value_write_ram);
+      ("undefined_unit", fun _ -> V_unit);
       ("undefined_bit", fun _ -> V_bit Sail_lib.B0);
       ("undefined_int", fun _ -> V_int Big_int.zero);
       ("undefined_bool", fun _ -> V_bool false);
diff --git a/test/c/exception.sail b/test/c/exception.sail
index 27248021..4e74fcae 100644
--- a/test/c/exception.sail
+++ b/test/c/exception.sail
@@ -5,7 +5,7 @@ val print_int = "print_int" : (string, int) -> unit
 
 union exception = {
   Epair : (range(0, 255), range(0, 255)),
-  Eunknown,
+  Eunknown : unit,
   Estring : string
 }
 
@@ -28,9 +28,9 @@ function main () = {
     print(g());
     f(); // will throw Estring
     throw(Epair(42, 24));
-    throw(Eunknown);
+    throw(Eunknown());
   } catch {
-    Eunknown     => print("Caught Eunknown"),
+    Eunknown()   => print("Caught Eunknown"),
     Epair(x, y)  => print("Caught Epair"),
     Estring(str) => {
       print("Caught Estring");
diff --git a/test/ocaml/string_of_struct/sos.sail b/test/ocaml/string_of_struct/sos.sail
index 6d14dfd7..69a17e6c 100644
--- a/test/ocaml/string_of_struct/sos.sail
+++ b/test/ocaml/string_of_struct/sos.sail
@@ -3,7 +3,7 @@ struct would cause the ocaml backend to generate a bad string_of
 function for the struct */
 
 union option ('a : Type) = {
-  None,
+  None : unit,
   Some : 'a
 }
 
diff --git a/test/ocaml/trycatch/tc.sail b/test/ocaml/trycatch/tc.sail
index b805f3fa..f788305d 100644
--- a/test/ocaml/trycatch/tc.sail
+++ b/test/ocaml/trycatch/tc.sail
@@ -18,6 +18,6 @@ function main () = {
   }
 }
 
-union clause exception = Test_other
+union clause exception = Test_other : unit
 
 end exception
\ No newline at end of file
diff --git a/test/ocaml/types/types.sail b/test/ocaml/types/types.sail
index a710eb25..d13b527c 100644
--- a/test/ocaml/types/types.sail
+++ b/test/ocaml/types/types.sail
@@ -24,7 +24,7 @@ struct TestStruct = {
 
 register SREG : TestStruct
 
-union option ('a : Type) = {None, Some : 'a}
+union option ('a : Type) = {None : unit, Some : 'a}
 
 register OREG : option(byte)
 
@@ -37,8 +37,8 @@ function main () = {
   SIGNALREG = High;
   print(if SIGNALREG == High then "pass" else "fail");
   SREG.field1 = 0b00;
-  print(if SREG.field1 == 0b00 then "pass" else "faiL");
+  print(if SREG.field1 == 0b00 then "pass" else "fail");
   SREG.field1 = 0b11;
-  print(if SREG.field1 == 0b11 then "pass" else "faiL");
+  print(if SREG.field1 == 0b11 then "pass" else "fail");
   print("pass")
 }
diff --git a/test/typecheck/pass/option_either.sail b/test/typecheck/pass/option_either.sail
index 632b882d..de4458ed 100644
--- a/test/typecheck/pass/option_either.sail
+++ b/test/typecheck/pass/option_either.sail
@@ -1,13 +1,13 @@
 default Order inc
 
-union option ('a : Type) = {None, Some : 'a}
+union option ('a : Type) = {None : unit, Some : 'a}
 
-function none () -> forall ('a : Type). option('a) = None
+function none () -> forall ('a : Type). option('a) = None()
 
 function some x : 'a -> forall ('a : Type). option('a) = Some(x)
 
 function test x : option('a) -> forall ('a : Type). range(0, 1) = match x {
-  None => 0,
+  None() => 0,
   Some(y) => 1
 }
 
diff --git a/test/typecheck/pass/pat_completeness.sail b/test/typecheck/pass/pat_completeness.sail
index fd4a7757..6a4036c5 100644
--- a/test/typecheck/pass/pat_completeness.sail
+++ b/test/typecheck/pass/pat_completeness.sail
@@ -1,11 +1,11 @@
-union option ('a : Type) = {None, Some : 'a}
+union option ('a : Type) = {None : unit, Some : 'a}
 
 union ast = {Foo : unit}
 
-let x : option(ast) = Some(Foo)
+let x : option(ast) = Some(Foo())
 
 let y : unit = match(x) {
-  Some(Foo) => (),
+  Some(Foo()) => (),
   Some(a)   => (),
-  None      => ()
+  None()    => ()
 }
\ No newline at end of file
diff --git a/test/typecheck/pass/union_infer.sail b/test/typecheck/pass/union_infer.sail
index 15eb5c60..bb422b65 100644
--- a/test/typecheck/pass/union_infer.sail
+++ b/test/typecheck/pass/union_infer.sail
@@ -1,7 +1,7 @@
 default Order inc
 
-union option ('a : Type) = {None, Some : 'a}
+union option ('a : Type) = {None : unit, Some : 'a}
 
-union Test = {A, B, C}
+union Test = {A : unit, B : unit, C : unit}
 
-function test () -> option(Test) = Some(C)
+function test () -> option(Test) = Some(C())