Make union types consistent in the AST

Previously union types could have no-argument constructors, for
example the option type was previously:

union option ('a : Type) = {
  Some : 'a,
  None
}

Now every union constructor must have a type, so option becomes:

union option ('a : Type) = {
  Some : 'a,
  None : unit
}

The reason for this is because previously these two different types of
constructors where very different in the AST, constructors with
arguments were used the E_app AST node, and no-argument constructors
used the E_id node. This was particularly awkward, because it meant
that E_id nodes could have polymorphic types, i.e. every E_id node
that was also a union constructor had to be annotated with a type
quantifier, in constrast with all other identifiers that have
unquantified types. This became an issue when monomorphising types,
because the machinery for figuring out function instantiations can't
be applied to identifier nodes. The same story occurs in patterns,
where previously unions were split across P_id and P_app nodes - now
the P_app node alone is used solely for unions.

This is a breaking change because it changes the syntax for union
constructors - where as previously option was matched as:

function is_none opt = match opt {
  Some(_) => false,
  None    => true
}

it is now matched as

function is_none opt = match opt {
  Some(_) => false,
  None()  => true
}

note that constructor() is syntactic sugar for constructor(()), i.e. a
one argument constructor with unit as it's value. This is exactly the
same as for functions where a unit-function can be called as f() and
not as f(()). (This commit also makes exit() work consistently in the
same way) An attempt to pattern match a variable with the same name as
a union-constructor now gives an error as a way to guard against
mistakes made because of this change.

There is probably an argument for supporting the old syntax via some
syntactic sugar, as it is slightly prettier that way, but for now I
have chosen to keep the implementation as simple as possible.

The RISCV spec, ARM spec, and tests have been updated to account for
this change. Furthermore the option type can now be included from
$SAIL_DIR/lib/ using

$include <option.sail>

18 files changed, 79 insertions, 178 deletions

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);