Cleanup code by fixing compiler warnings, and fix ocaml compilation

Add the ast.sed script we need to build sail. Currently we just need
this to fix up the locations in the AST but it will be removed once we
can share locations between ocaml and lem.

13 files changed, 174 insertions, 69 deletions

diff --git a/src/Makefile b/src/Makefile
index aa7c0f95..a39067b6 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -264,6 +264,7 @@ clean:
 	-rm -rf lem lib
 	-rm -rf sail.docdir
 	-rm -f ast.ml
+	-rm -f ast.lem
 
 doc:
 	ocamlbuild sail.docdir/index.html
diff --git a/src/_tags b/src/_tags
index 1a2d5c7f..efe34d17 100644
--- a/src/_tags
+++ b/src/_tags
@@ -2,7 +2,7 @@ true: -traverse, debug, use_menhir
 <**/*.ml>: bin_annot, annot
 # <lem_interp> or <test>: include
 <sail.{byte,native}>: package(zarith), use_pprint, use_nums, use_unix, use_str, use_lem
-<isail.{byte,native}>: package(linenoise), use_pprint, use_nums, use_unix, use_str, use_lem
+<isail.{byte,native}>: package(zarith), package(linenoise), use_pprint, use_nums, use_unix, use_str, use_lem
 <isail.ml>: package(linenoise)
 <pprint> or <pprint/src>: include
 <*.m{l,li}>: use_lem
diff --git a/src/ast.sed b/src/ast.sed
new file mode 100644
index 00000000..39c58a50
--- /dev/null
+++ b/src/ast.sed
@@ -0,0 +1,2 @@
+s/type l = | Unknown/type l = Parse_ast.l/
+s/type value = | Val/open Value/
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 61b67c31..ec572bd4 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -142,6 +142,15 @@ module Nexp = struct
     | Nexp_id v1, Nexp_id v2 -> Id.compare v1 v2
     | Nexp_var kid1, Nexp_var kid2 -> Kid.compare kid1 kid2
     | Nexp_constant c1, Nexp_constant c2 -> Big_int.compare c1 c2
+    | Nexp_app (op1, args1), Nexp_app (op2, args2) ->
+       let lex1 = Id.compare op1 op2 in
+       let lex2 = List.length args1 - List.length args2 in
+       let lex3 =
+         if lex2 = 0 then
+           List.fold_left2 (fun l n1 n2 -> if compare n1 n2 = 0 then 0 else compare n1 n2) 0 args1 args2
+         else 0
+       in
+       lex_ord (lex1, lex_ord (lex2, lex3))
     | Nexp_times (n1a, n1b), Nexp_times (n2a, n2b)
     | Nexp_sum (n1a, n1b), Nexp_sum (n2a, n2b)
     | Nexp_minus (n1a, n1b), Nexp_minus (n2a, n2b) ->
@@ -172,6 +181,7 @@ let rec is_nexp_constant (Nexp_aux (nexp, _)) = match nexp with
   | Nexp_times (n1, n2) | Nexp_sum (n1, n2) | Nexp_minus (n1, n2) ->
     is_nexp_constant n1 && is_nexp_constant n2
   | Nexp_exp n | Nexp_neg n -> is_nexp_constant n
+  | Nexp_app (_, nexps) -> List.for_all is_nexp_constant nexps
 
 let rec nexp_simp (Nexp_aux (nexp, l)) = Nexp_aux (nexp_simp_aux nexp, l)
 and nexp_simp_aux = function
@@ -365,6 +375,7 @@ and map_exp_annot_aux f = function
   | E_internal_exp_user (annot1, annot2) -> E_internal_exp_user (f annot1, f annot2)
   | E_comment str -> E_comment str
   | E_comment_struc exp -> E_comment_struc (map_exp_annot f exp)
+  | E_internal_value v -> E_internal_value v
   | E_internal_let (lexp, exp1, exp2) -> E_internal_let (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2)
   | E_internal_plet (pat, exp1, exp2) -> E_internal_plet (map_pat_annot f pat, map_exp_annot f exp1, map_exp_annot f exp2)
   | E_internal_return exp -> E_internal_return (map_exp_annot f exp)
@@ -653,7 +664,6 @@ and string_of_lexp (LEXP_aux (lexp, _)) =
      string_of_lexp lexp ^ "[" ^ string_of_exp exp1 ^ ".." ^ string_of_exp exp2 ^ "]"
   | LEXP_field (lexp, id) -> string_of_lexp lexp ^ "." ^ string_of_id id
   | LEXP_memory (f, xs) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"
-  | _ -> "LEXP"
 and string_of_letbind (LB_aux (lb, l)) =
   match lb with
   | LB_val (pat, exp) -> string_of_pat pat ^ " = " ^ string_of_exp exp
@@ -694,6 +704,7 @@ let rec nexp_frees (Nexp_aux (nexp, l)) =
   | Nexp_minus (n1, n2) -> KidSet.union (nexp_frees n1) (nexp_frees n2)
   | Nexp_exp n -> nexp_frees n
   | Nexp_neg n -> nexp_frees n
+  | Nexp_app (_, nexps) -> List.fold_left KidSet.union KidSet.empty (List.map nexp_frees nexps)
 
 let rec lexp_to_exp (LEXP_aux (lexp_aux, annot) as le) =
   let rewrap e_aux = E_aux (e_aux, annot) in
@@ -783,13 +794,11 @@ let union_effects e1 e2 =
   | Effect_aux (Effect_set base_effs1, _), Effect_aux (Effect_set base_effs2, _) ->
      let base_effs3 = BESet.elements (BESet.of_list (base_effs1 @ base_effs2)) in
      Effect_aux (Effect_set base_effs3, Parse_ast.Unknown)
-  | _, _ -> assert false (* We don't do Effect variables *)
 
 let equal_effects e1 e2 =
   match e1, e2 with
   | Effect_aux (Effect_set base_effs1, _), Effect_aux (Effect_set base_effs2, _) ->
      BESet.compare (BESet.of_list base_effs1) (BESet.of_list base_effs2) = 0
-  | _, _ -> assert false (* We don't do Effect variables *)
 
 let rec tyvars_of_nexp (Nexp_aux (nexp,_)) =
   match nexp with
@@ -801,6 +810,7 @@ let rec tyvars_of_nexp (Nexp_aux (nexp,_)) =
   | Nexp_minus (n1,n2) -> KidSet.union (tyvars_of_nexp n1) (tyvars_of_nexp n2)
   | Nexp_exp n
   | Nexp_neg n -> tyvars_of_nexp n
+  | Nexp_app (_, nexps) -> List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_nexp nexps)
 
 let rec tyvars_of_typ (Typ_aux (t,_)) =
   match t with
@@ -835,7 +845,9 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) =
      wrap (E_sizeof i) typ
   | Typ_app (id, args) ->
      wrap (E_app (prepend_id "undefined_" id,
-       List.concat (List.map (undefined_of_typ_args mwords l annot) args))) typ
+                  List.concat (List.map (undefined_of_typ_args mwords l annot) args))) typ
+  | Typ_tup typs ->
+     wrap (E_tuple (List.map (undefined_of_typ mwords l annot) typs)) typ
   | Typ_var kid ->
      (* Undefined monomorphism restriction in the type checker should
         guarantee that the typ_(kid) parameter was always one created
@@ -843,7 +855,7 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) =
         initial_check.ml. i.e. the rewriter should only encounter this
         case when re-writing those functions. *)
      wrap (E_id (prepend_id "typ_" (id_of_kid kid))) typ
-  | Typ_fn _ -> assert false
+  | Typ_fn _ | Typ_exist _ -> assert false (* Typ_exist should be re-written *)
 and undefined_of_typ_args mwords l annot (Typ_arg_aux (typ_arg_aux, _) as typ_arg) =
   match typ_arg_aux with
   | Typ_arg_nexp n -> [E_aux (E_sizeof n, (l, annot (atom_typ n)))]
diff --git a/src/initial_check.ml b/src/initial_check.ml
index d5502d63..7ec0154e 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -131,7 +131,7 @@ let string_of_parse_id_aux = function
   | Parse_ast.DeIid v -> v
 
 let string_contains str char =
-  try (String.index str char; true) with
+  try (ignore (String.index str char); true) with
   | Not_found -> false
 
 let to_ast_id (Parse_ast.Id_aux(id, l)) =
@@ -519,6 +519,7 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
     | Parse_ast.E_throw exp -> E_throw (to_ast_exp k_env def_ord exp)
     | Parse_ast.E_return exp -> E_return(to_ast_exp k_env def_ord exp)
     | Parse_ast.E_assert(cond,msg) -> E_assert(to_ast_exp k_env def_ord cond, to_ast_exp k_env def_ord msg)
+    | _ -> raise (Reporting_basic.err_unreachable l "Unparsable construct in to_ast_exp")
     ), (l,()))
 
 and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit lexp = 
@@ -747,7 +748,7 @@ let to_ast_fundef  (names,k_env,def_ord) (Parse_ast.FD_aux(fd,l):Parse_ast.funde
     (*let _ = Printf.eprintf "to_ast_fundef\n" in*)
     let tannot_opt, k_env,_ = to_ast_tannot_opt k_env def_ord tannot_opt in
     FD_aux(FD_function(to_ast_rec rec_opt, tannot_opt, to_ast_effects_opt k_env effects_opt, List.map (to_ast_funcl (names, k_env, def_ord)) funcls), (l,())), (names,k_env,def_ord)
-    
+
 type def_progress =
     No_def
   | Def_place_holder of id * Parse_ast.l
@@ -823,6 +824,9 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out
   | Parse_ast.DEF_reg_dec(dec) ->
     let d = to_ast_dec envs dec in
     ((Finished(DEF_reg_dec(d))),envs),partial_defs
+  | Parse_ast.DEF_internal_mutrec _ ->
+     (* Should never occur because of remove_mutrec *)
+    typ_error Parse_ast.Unknown "Internal mutual block found when processing scattered defs" None None None
   | Parse_ast.DEF_scattered(Parse_ast.SD_aux(sd,l)) ->
     (match sd with
     | Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) ->
@@ -887,8 +891,8 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out
 	  ((Finished def), envs),partial_defs
 	| _, true -> 
 	  typ_error l "Scattered definition ended multiple times" (Some id) None None
-	| _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type"))))
-    
+        | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type"))))
+
 let rec to_ast_defs_helper envs partial_defs = function
   | [] -> ([],envs,partial_defs)
   | d::ds  -> let ((d', envs), partial_defs) = to_ast_def envs partial_defs d in
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 1a6e6393..3356b9dc 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -63,6 +63,7 @@ let value_of_lit (L_aux (l_aux, _)) =
   | L_true -> V_bool true
   | L_false -> V_bool false
   | L_string str -> V_string str
+  | _ -> failwith "Unimplemented value_of_lit" (* TODO *)
 
 let is_value = function
   | (E_aux (E_internal_value _, _)) -> true
@@ -77,7 +78,9 @@ let is_false = function
   | _ -> false
 
 let exp_of_value v = (E_aux (E_internal_value v, (Parse_ast.Unknown, None)))
-let value_of_exp (E_aux (E_internal_value v, _)) = v
+let value_of_exp = function
+  | (E_aux (E_internal_value v, _)) -> v
+  | _ -> failwith "value_of_exp coerction failed"
 
 (**************************************************************************)
 (* 1. Interpreter Monad                                                   *)
@@ -155,6 +158,7 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
     | E_id id' -> if Id.compare id id' = 0 then unaux_exp (exp_of_value value) else E_id id'
     | E_cast (typ, exp) -> E_cast (typ, subst id value exp)
     | E_app (fn, exps) -> E_app (fn, List.map (subst id value) exps)
+    | _ -> assert false (* TODO *)
   in
   wrap e_aux
 
@@ -245,6 +249,8 @@ let rec step (E_aux (e_aux, annot)) =
 
   | E_sizeof _ | E_constraint _ -> assert false (* Must be re-written before interpreting *)
 
+  | _ -> assert false (* TODO *)
+
 and combine _ v1 v2 =
   match (v1, v2) with
   | None, None -> None
@@ -262,6 +268,7 @@ and pattern_match (P_aux (p_aux, _) as pat) value =
      matched, Bindings.add id value bindings
   | P_typ (_, pat) -> pattern_match pat value
   | P_id id -> true, Bindings.singleton id value
+  | P_var (pat, _) -> pattern_match pat value
   | P_app (id, pats) ->
      let (ctor, vals) = coerce_ctor value in
      if Id.compare id (mk_id ctor) = 0 then
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index aed736a7..b1a19482 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -181,7 +181,7 @@ let ocaml_lit (L_aux (lit_aux, _)) =
   | L_one -> string "B1"
   | L_true -> string "true"
   | L_false -> string "false"
-  | L_num n -> parens (string "Big_int.of_string" ^^ space ^^ string ("\"" ^ Big_int.to_string n ^ "\""))
+  | L_num n -> parens (string "big_int_of_string" ^^ space ^^ string ("\"" ^ Big_int.to_string n ^ "\""))
   | L_undef -> failwith "undefined should have been re-written prior to ocaml backend"
   | L_string str -> string_lit str
   | L_real str -> parens (string "real_of_string" ^^ space ^^ dquotes (string (String.escaped str)))
@@ -285,11 +285,13 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
        match ord with
        | Ord_aux (Ord_inc, _) -> string "Big_int.add" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step
        | Ord_aux (Ord_dec, _) -> string "Big_int.sub" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step
+       | Ord_aux (Ord_var _, _) -> failwith "Cannot have variable loop order!"
      in
      let loop_compare =
        match ord with
        | Ord_aux (Ord_inc, _) -> string "Big_int.less_equal"
        | Ord_aux (Ord_dec, _) -> string "Big_int.greater"
+       | Ord_aux (Ord_var _, _) -> failwith "Cannot have variable loop order!"
      in
      let loop_body =
        separate space [string "if"; loop_compare; zencode ctx id; ocaml_atomic_exp ctx exp_to]
@@ -442,7 +444,11 @@ let ocaml_funcls ctx =
   function
   | [] -> failwith "Ocaml: empty function"
   | [FCL_aux (FCL_Funcl (id, pexp),_)] ->
-     let Typ_aux (Typ_fn (typ1, typ2, _), _) = Bindings.find id ctx.val_specs in
+     let typ1, typ2 =
+       match Bindings.find id ctx.val_specs with
+       | Typ_aux (Typ_fn (typ1, typ2, _), _) -> (typ1, typ2)
+       | _ -> failwith "Found val spec which was not a function!"
+     in
      let pat_sym = gensym () in
      let pat, exp =
        match pexp with
@@ -466,7 +472,11 @@ let ocaml_funcls ctx =
      ocaml_funcl call string_of_arg string_of_ret
   | funcls ->
      let id = funcls_id funcls in
-     let Typ_aux (Typ_fn (typ1, typ2, _), _) = Bindings.find id ctx.val_specs in
+     let typ1, typ2 =
+       match Bindings.find id ctx.val_specs with
+       | Typ_aux (Typ_fn (typ1, typ2, _), _) -> (typ1, typ2)
+       | _ -> failwith "Found val spec which was not a function!"
+     in
      let pat_sym = gensym () in
      let call_header = function_header () in
      let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info typ1 typ2 in
@@ -599,7 +609,7 @@ let val_spec_typs (Defs defs) =
     | _ :: defs -> vs_typs defs
     | [] -> []
   in
-  vs_typs defs;
+  ignore (vs_typs defs);
   !typs
 
 let ocaml_defs (Defs defs) =
@@ -616,7 +626,7 @@ let ocaml_defs (Defs defs) =
     else empty
   in
   (string "open Sail_lib;;" ^^ hardline)
-  ^^ (string "module Big_int = Nat_big_num" ^^ ocaml_def_end)
+  ^^ (string "open Big_int" ^^ ocaml_def_end)
   ^^ concat (List.map (ocaml_def ctx) defs)
   ^^ empty_reg_init
 
diff --git a/src/parser2.mly b/src/parser2.mly
index 6021596f..140f1b86 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -75,7 +75,9 @@ let mk_kid str n m = Kid_aux (Var str, loc n m)
 let id_of_kid = function
   | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
 
-let deinfix (Id_aux (Id v, l)) = Id_aux (DeIid v, l)
+let deinfix = function
+  | (Id_aux (Id v, l)) -> Id_aux (DeIid v, l)
+  | (Id_aux (DeIid v, l)) -> Id_aux (Id v, l)
 
 let mk_effect e n m = BE_aux (e, loc n m)
 let mk_typ t n m = ATyp_aux (t, loc n m)
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index 33743188..71fcd587 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -157,7 +157,7 @@ let doc_quants quants =
     | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid]
     | QI_id kopt when is_nat_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])]
     | QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])]
-    | QI_id kopt when is_order_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])]
+    | QI_id kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])]
     | QI_const nc -> []
   in
   let qi_nc (QI_aux (qi_aux, _)) =
@@ -209,7 +209,6 @@ let rec doc_pat (P_aux (p_aux, _) as pat) =
   match p_aux with
   | P_id id -> doc_id id
   | P_tup pats -> lparen ^^ separate_map (comma ^^ space) doc_pat pats ^^ rparen
-  | P_app (id, pats) -> doc_id id ^^ lparen ^^ separate_map (comma ^^ space) doc_pat pats ^^ rparen
   | P_typ (typ, pat) -> separate space [doc_pat pat; colon; doc_typ typ]
   | P_lit lit -> doc_lit lit
   (* P_var short form sugar *)
@@ -346,6 +345,7 @@ and doc_infix n (E_aux (e_aux, _) as exp) =
          | (InfixL, m) when m < n -> parens (separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r])
          | (InfixR, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r]
          | (InfixR, m) when m < n -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r])
+         | _ -> assert false
        with
        | Not_found ->
           separate space [doc_atomic_exp l; doc_id op; doc_atomic_exp r]
@@ -510,7 +510,6 @@ let rec doc_def def = group (match def with
   | DEF_type t_def -> doc_typdef t_def
   | DEF_kind k_def -> doc_kind_def k_def
   | DEF_fundef f_def -> doc_fundef f_def
-  | DEF_internal_mutrec f_defs -> separate_map hardline doc_fundef f_defs
   | DEF_val lbind -> string "let" ^^ space ^^ doc_letbind lbind
   | DEF_internal_mutrec fundefs ->
      (string "mutual {" ^//^ separate_map (hardline ^^ hardline) doc_fundef fundefs)
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index 166e0517..af1f85d0 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -97,7 +97,7 @@
 
 let rec skip_lines in_chan = function
   | n when n <= 0 -> ()
-  | n -> input_line in_chan; skip_lines in_chan (n - 1)
+  | n -> ignore (input_line in_chan); skip_lines in_chan (n - 1)
 
 let rec read_lines in_chan = function
   | n when n <= 0 -> []
@@ -186,9 +186,9 @@ let read_from_file_pos2 p1 p2 =
   let ic = open_in p1.Lexing.pos_fname in
   let _ = seek_in ic s in
   let l = (e - s) in
-  let buf = String.create l in
+  let buf = Bytes.create l in
   let _ = input ic buf 0 l in
-  let _ = match multi with None -> () | Some sk -> String.fill buf 0 sk ' ' in
+  let _ = match multi with None -> () | Some sk -> Bytes.fill buf 0 sk ' ' in
   let _ = close_in ic in
   (buf, not (multi = None))
 
diff --git a/src/type_check.ml b/src/type_check.ml
index ac5f19f8..c1390e84 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -106,6 +106,9 @@ let pp_type_error err =
        ^//^ string (string_of_list ", " string_of_n_constraint constrs)
     | Err_no_num_ident id ->
        string "No num identifier" ^^ space ^^ string (string_of_id id)
+    | Err_unresolved_quants (id, quants) ->
+       string "Could not resolve quantifiers for" ^^ space ^^ string (string_of_id id)
+       ^//^ group (separate_map hardline (fun quant -> string (string_of_quant_item quant)) quants)
     | Err_other str -> string str
   in
   pp_err err
@@ -293,7 +296,8 @@ module Env : sig
   val is_union_constructor : id -> t -> bool
   val add_record : id -> typquant -> (typ * id) list -> t -> t
   val is_record : id -> t -> bool
-  val get_accessor : id -> id -> t -> typquant * typ
+  val get_accessor_fn : id -> id -> t -> typquant * typ
+  val get_accessor : id -> id -> t -> typquant * typ * typ * effect
   val add_local : id -> mut * typ -> t -> t
   val get_locals : t -> (mut * typ) Bindings.t
   val add_variant : id -> typquant * type_union list -> t -> t
@@ -685,12 +689,18 @@ end = struct
                    accessors = List.fold_left fold_accessors env.accessors fields }
       end
 
-  let get_accessor rec_id id env =
+  let get_accessor_fn rec_id id env =
     let freshen_bind bind = List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) in
     try freshen_bind (Bindings.find (field_name rec_id id) env.accessors)
     with
     | Not_found -> typ_error (id_loc id) ("No accessor found for " ^ string_of_id (field_name rec_id id))
 
+  let get_accessor rec_id id env =
+    match get_accessor_fn rec_id id env with
+    | (typq, Typ_aux (Typ_fn (rec_typ, field_typ, effect), _)) ->
+       (typq, rec_typ, field_typ, effect)
+    | _ -> typ_error (id_loc id) ("Accessor with non-function type found for " ^ string_of_id (field_name rec_id id))
+
   let is_mutable id env =
     try
       let (mut, _) = Bindings.find id env.locals in
@@ -953,6 +963,9 @@ let add_typquant (quant : typquant) (env : Env.t) : Env.t =
 
 (* Create vectors with the default order from the environment *)
 
+let default_order_error_string =
+  "No default Order (if you have set a default Order, move it earlier in the specification)"
+
 let dvector_typ env n m typ = vector_typ n m (Env.get_default_order env) typ
 
 let lvector_typ env l typ =
@@ -961,6 +974,8 @@ let lvector_typ env l typ =
      vector_typ (nint 0) l ord typ
   | Ord_aux (Ord_dec, _) as ord ->
      vector_typ (nminus l (nint 1)) l ord typ
+  | Ord_aux (Ord_var _, _) as ord ->
+     typ_error Parse_ast.Unknown default_order_error_string
 
 let ex_counter = ref 0
 
@@ -1272,6 +1287,7 @@ let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
   | Typ_tup typs -> List.fold_left KidSet.union KidSet.empty (List.map (typ_frees ~exs:exs) typs)
   | Typ_app (f, args) -> List.fold_left KidSet.union KidSet.empty (List.map (typ_arg_frees ~exs:exs) args)
   | Typ_exist (kids, nc, typ) -> typ_frees ~exs:(KidSet.of_list kids) typ
+  | Typ_fn (typ1, typ2, _) -> KidSet.union (typ_frees ~exs:exs typ1) (typ_frees ~exs:exs typ2)
 and typ_arg_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) =
   match typ_arg_aux with
   | Typ_arg_nexp n -> nexp_frees ~exs:exs n
@@ -1334,6 +1350,7 @@ let typ_identical env typ1 typ2 =
     | Typ_arg_nexp n1, Typ_arg_nexp n2 -> nexp_identical n1 n2
     | Typ_arg_typ typ1, Typ_arg_typ typ2 -> typ_identical' typ1 typ2
     | Typ_arg_order ord1, Typ_arg_order ord2 -> ord_identical ord1 ord2
+    | _, _ -> false
   in
   typ_identical' (Env.expand_synonyms env typ1) (Env.expand_synonyms env typ2)
 
@@ -1613,8 +1630,12 @@ let rec subtyp l env typ1 typ2 =
        when is_some (destruct_atom_kid env typ1) && is_some (destruct_atom_kid env typ2) ->
      let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids1 in
      let env = Env.add_constraint nc1 env in
-     let Some atom_kid1 = destruct_atom_kid env typ1 in
-     let Some atom_kid2 = destruct_atom_kid env typ2 in
+
+     (* Guaranteed to succeed because of the guard *)
+     let destruct_some x = match x with Some y -> y | _ -> assert false in
+     let atom_kid1 = destruct_some (destruct_atom_kid env typ1) in
+     let atom_kid2 = destruct_some (destruct_atom_kid env typ2) in
+
      let kids2 = List.filter (fun kid -> Kid.compare atom_kid2 kid <> 0) kids2 in
      let env = Env.add_typ_var atom_kid2 BK_nat env in
      let env = Env.add_constraint (nc_eq (nvar atom_kid1) (nvar atom_kid2)) env in
@@ -1640,6 +1661,7 @@ let rec subtyp l env typ1 typ2 =
           let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env existential_kids in
           let env = List.fold_left uv_nexp_constraint env (KBindings.bindings unifiers) in
           Env.add_constraint enc env
+       | _, None -> assert false (* Cannot have existential_kids without existential_nc *)
      in
      if prove env nc then ()
      else typ_error l ("Could not show " ^ string_of_typ typ1 ^ " is a subset of existential " ^ string_of_typ typ2)
@@ -1683,6 +1705,8 @@ let infer_lit env (L_aux (lit_aux, l) as lit) =
                      (nint (String.length str - 1))
                      (nint (String.length str))
                      (mk_typ (Typ_id (mk_id "bit")))
+       | Ord_aux (Ord_var _, _) -> typ_error l default_order_error_string
+
      end
   | L_hex str ->
      begin
@@ -1694,6 +1718,8 @@ let infer_lit env (L_aux (lit_aux, l) as lit) =
                      (nint (String.length str * 4 - 1))
                      (nint (String.length str * 4))
                      (mk_typ (Typ_id (mk_id "bit")))
+
+       | Ord_aux (Ord_var _, _) -> typ_error l default_order_error_string
      end
   | L_undef -> typ_error l "Cannot infer the type of undefined"
 
@@ -1982,7 +2008,10 @@ let strip_lexp : 'a lexp -> unit lexp = function lexp -> map_lexp_annot (fun (l,
 
 let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ_aux, _) as typ) : tannot exp =
   let annot_exp_effect exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in
-  let add_effect (E_aux (exp, (l, Some (env, typ, _)))) eff = E_aux (exp, (l, Some (env, typ, eff))) in
+  let add_effect exp eff = match exp with
+    | (E_aux (exp, (l, Some (env, typ, _)))) -> E_aux (exp, (l, Some (env, typ, eff)))
+    | _ -> failwith "Tried to add effect to unannoted expression"
+  in
   let annot_exp exp typ = annot_exp_effect exp typ no_effect in
   match (exp_aux, typ_aux) with
   | E_block exps, _ ->
@@ -2055,7 +2084,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
        | _ -> typ_error l ("The type " ^ string_of_typ typ ^ " is not a record")
      in
      let check_fexp (FE_aux (FE_Fexp (field, exp), (l, ()))) =
-       let (typq, Typ_aux (Typ_fn (rectyp_q, field_typ, _), _)) = Env.get_accessor rectyp_id field env in
+       let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in
        let unifiers, _, _ (* FIXME *) = try unify l env rectyp_q typ with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
        let field_typ' = subst_unifiers unifiers field_typ in
        let checked_exp = crule check_exp env exp field_typ' in
@@ -2070,7 +2099,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
        | _ -> typ_error l ("The type " ^ string_of_typ typ ^ " is not a record")
      in
      let check_fexp (FE_aux (FE_Fexp (field, exp), (l, ()))) =
-       let (typq, Typ_aux (Typ_fn (rectyp_q, field_typ, _), _)) = Env.get_accessor rectyp_id field env in
+       let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in
        let unifiers, _, _ (* FIXME *) = try unify l env rectyp_q typ with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
        let field_typ' = subst_unifiers unifiers field_typ in
        let checked_exp = crule check_exp env exp field_typ' in
@@ -2131,7 +2160,10 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
      let checked_exp = crule check_exp env exp exc_typ in
      annot_exp_effect (E_throw checked_exp) typ (mk_effect [BE_escape])
   | E_internal_let (lexp, bind, exp), _ ->
-     let E_aux (E_assign (lexp, bind), _), env = bind_assignment env lexp bind in
+     let lexp, bind, env = match bind_assignment env lexp bind with
+       | E_aux (E_assign (lexp, bind), _), env -> lexp, bind, env
+       | _, _ -> assert false
+     in
      let checked_exp = crule check_exp env exp typ in
      annot_exp (E_internal_let (lexp, bind, checked_exp)) typ
   | E_internal_return exp, _ ->
@@ -2214,7 +2246,10 @@ and check_case env pat_typ pexp typ =
 and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
   let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in
   let annot_exp exp typ = E_aux (exp, (l, Some (env, typ, no_effect))) in
-  let switch_typ (E_aux (exp, (l, Some (env, _, eff)))) typ = E_aux (exp, (l, Some (env, typ, eff))) in
+  let switch_typ exp typ = match exp with
+    | (E_aux (exp, (l, Some (env, _, eff)))) -> E_aux (exp, (l, Some (env, typ, eff)))
+    | _ -> failwith "Cannot switch type for unannotated function"
+  in
   let rec try_casts trigger errs = function
     | [] -> typ_raise l (Err_no_casts (trigger, errs))
     | (cast :: casts) -> begin
@@ -2245,7 +2280,10 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
 and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
   let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in
   let annot_exp exp typ = E_aux (exp, (l, Some (env, typ, no_effect))) in
-  let switch_typ (E_aux (exp, (l, Some (env, _, eff)))) typ = E_aux (exp, (l, Some (env, typ, eff))) in
+  let switch_typ exp typ = match exp with
+    | (E_aux (exp, (l, Some (env, _, eff)))) -> E_aux (exp, (l, Some (env, typ, eff)))
+    | _ -> failwith "Cannot switch type for unannotated expression"
+  in
   let rec try_casts = function
     | [] -> unify_error l "No valid casts resulted in unification"
     | (cast :: casts) -> begin
@@ -2272,7 +2310,10 @@ and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
 and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) =
   typ_print ("Binding " ^ string_of_pat pat ^  " to " ^ string_of_typ typ);
   let annot_pat pat typ = P_aux (pat, (l, Some (env, typ, no_effect))) in
-  let switch_typ (P_aux (pat_aux, (l, Some (env, _, eff)))) typ = P_aux (pat_aux, (l, Some (env, typ, eff))) in
+  let switch_typ pat typ = match pat with
+    | (P_aux (pat_aux, (l, Some (env, _, eff)))) -> P_aux (pat_aux, (l, Some (env, typ, eff)))
+    | _ -> failwith "Cannot switch type of unannotated pattern"
+  in
   let bind_tuple_pat (tpats, env) pat typ =
     let tpat, env = bind_pat env pat typ in tpat :: tpats, env
   in
@@ -2411,7 +2452,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 ->
+       | Local (Immutable, _) | Unbound | Union _ ->
           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)
@@ -2428,26 +2469,26 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
        let typed_pat, env = bind_pat env pat bit_typ in
        pats @ [typed_pat], env
      in
-     let ((typed_pat :: typed_pats) as pats), env =
+     let pats, env =
        List.fold_left fold_pats ([], env) (pat :: pats) in
      let len = nexp_simp (nint (List.length pats)) in
-     let etyp = pat_typ_of typed_pat in
-     List.map (fun pat -> typ_equality l env etyp (pat_typ_of pat)) pats;
+     let etyp = pat_typ_of (List.hd pats) in
+     List.iter (fun pat -> typ_equality l env etyp (pat_typ_of pat)) pats;
      annot_pat (P_vector pats) (lvector_typ env len etyp), env
   | P_vector_concat (pat :: pats) ->
      let fold_pats (pats, env) pat =
        let inferred_pat, env = infer_pat env pat in
        pats @ [inferred_pat], env
      in
-     let (inferred_pat :: inferred_pats), env = List.fold_left fold_pats ([], env) (pat :: pats) in
-     let (_, len, _, vtyp) = destruct_vec_typ l env (pat_typ_of inferred_pat) in
+     let inferred_pats, env = List.fold_left fold_pats ([], env) (pat :: pats) in
+     let (_, len, _, vtyp) = destruct_vec_typ l env (pat_typ_of (List.hd inferred_pats)) in
      let fold_len len pat =
        let (_, len', _, vtyp') = destruct_vec_typ l env (pat_typ_of pat) in
        typ_equality l env vtyp vtyp';
        nsum len len'
      in
-     let len = nexp_simp (List.fold_left fold_len len inferred_pats) in
-     annot_pat (P_vector_concat (inferred_pat :: inferred_pats)) (lvector_typ env len vtyp), env
+     let len = nexp_simp (List.fold_left fold_len len (List.tl inferred_pats)) in
+     annot_pat (P_vector_concat inferred_pats) (lvector_typ env len vtyp), env
   | P_as (pat, id) ->
      let (typed_pat, env) = infer_pat env pat in
      annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), Env.add_local id (Immutable, pat_typ_of typed_pat) env
@@ -2478,14 +2519,19 @@ 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
               in
               let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in
-              let E_aux (E_app (_, [_; inferred_exp]), _) = access in
+              let inferred_exp = match access with
+                | E_aux (E_app (_, [_; inferred_exp]), _) -> inferred_exp
+                | _ -> assert false
+              in
               typ_of access, LEXP_vector (annot_lexp (LEXP_id v) vtyp, inferred_exp), is_register
             end
+         | _ -> typ_error l "Field l-expression must be either a vector or an identifier"
        in
        let regtyp, inferred_flexp, is_register = infer_flexp flexp in
        typ_debug ("REGTYP: " ^ string_of_typ regtyp ^ " / " ^ string_of_typ (Env.expand_synonyms env regtyp));
@@ -2509,7 +2555,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
           annot_assign (annot_lexp (LEXP_field (annot_lexp_effect inferred_flexp regtyp eff, field)) vec_typ) checked_exp, env
        | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
           let eff = if is_register then mk_effect [BE_wreg] else no_effect in
-          let (typq, Typ_aux (Typ_fn (rectyp_q, field_typ, _), _)) = Env.get_accessor rectyp_id field env in
+          let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in
           let unifiers, _, _ (* FIXME *) = try unify l env rectyp_q regtyp with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
           let field_typ' = subst_unifiers unifiers field_typ in
           let checked_exp = crule check_exp env exp field_typ' in
@@ -2541,8 +2587,8 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
   match lexp_aux with
   | LEXP_id v ->
      begin match Env.lookup_id v env with
-     | Local (Immutable, _) | Enum _ ->
-        typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
+     | Local (Immutable, _) | Enum _ | Union _ ->
+        typ_error l ("Cannot modify let-bound constant, union 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
@@ -2550,8 +2596,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 _ ->
-          typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
+       | Local (Immutable, _) | Enum _ | Union _ ->
+          typ_error l ("Cannot modify let-bound constant, union or enumeration constructor " ^ string_of_id v)
        | Local (Mutable, vtyp) ->
           begin
             subtyp l env typ typ_annot;
@@ -2595,8 +2641,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 _ ->
-                         typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
+                      | Local (Immutable, _) | Enum _ | Union _ ->
+                         typ_error l ("Cannot modify let-bound constant, union or enumeration constructor " ^ string_of_id v)
                       | Unbound ->
                          typ_error l "Unbound variable in vector tuple assignment"
                       | Local (Mutable, vtyp) | Register vtyp ->
@@ -2614,7 +2660,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
                      | Register (Typ_aux (Typ_id rec_id, _)) -> rec_id
                      | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here")
                    in
-                   let typq, (Typ_aux (Typ_fn (_, vtyp, _), _)) = Env.get_accessor rec_id fid env in
+                   let typq, _, vtyp, _ = Env.get_accessor rec_id fid env in
                    let llen' = match destruct_vector env vtyp with
                      | Some (_, llen', _, _) -> llen'
                      | None -> typ_error l "Variables in vector tuple assignment must be vectors"
@@ -2636,12 +2682,16 @@ 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
        in
        let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_subrange", [E_aux (E_id v, (l, ())); exp1; exp2]), (l, ()))) in
-       let E_aux (E_app (_, [_; inferred_exp1; inferred_exp2]), _) = access in
+       let inferred_exp1, inferred_exp2 = match access with
+         | E_aux (E_app (_, [_; inferred_exp1; inferred_exp2]), _) -> inferred_exp1, inferred_exp2
+         | _ -> assert false
+       in
        match typ_of access with
        | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ deref_typ, _)]), _) when string_of_id id = "register" ->
           subtyp l env typ deref_typ;
@@ -2660,12 +2710,16 @@ 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
        in
        let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in
-       let E_aux (E_app (_, [_; inferred_exp]), _) = access in
+       let inferred_exp = match access with
+         | E_aux (E_app (_, [_; inferred_exp]), _) -> inferred_exp
+         | _ -> assert false
+       in
        match typ_of access with
        | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ deref_typ, _)]), _) when string_of_id id = "register" ->
           subtyp l env typ deref_typ;
@@ -2685,7 +2739,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
        | Register (Typ_aux (Typ_id rec_id, _)) -> rec_id
        | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here")
      in
-     let typq, (Typ_aux (Typ_fn (_, ret_typ, _), _)) = Env.get_accessor rec_id fid env in
+     let typq, _, ret_typ, _ = Env.get_accessor rec_id fid env in
      annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ (mk_effect [BE_wreg]), env
   | _ -> typ_error l ("Unhandled l-expression " ^ string_of_lexp lexp)
 
@@ -2743,7 +2797,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        (* Accessing a field of a record *)
        | Typ_aux (Typ_id rectyp, _) as typ when Env.is_record rectyp env ->
           begin
-            let inferred_acc, _ = infer_funapp' l (Env.no_casts env) field (Env.get_accessor rectyp field env) [strip_exp inferred_exp] None in
+            let inferred_acc, _ = infer_funapp' l (Env.no_casts env) field (Env.get_accessor_fn rectyp 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)
             | _ -> assert false (* Unreachable *)
@@ -2764,7 +2818,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        | _ -> typ_error l ("The type " ^ string_of_typ typ ^ " is not a record")
      in
      let check_fexp (FE_aux (FE_Fexp (field, exp), (l, ()))) =
-       let (typq, Typ_aux (Typ_fn (rectyp_q, field_typ, _), _)) = Env.get_accessor rectyp_id field env in
+       let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in
        let unifiers, _, _ (* FIXME *) = try unify l env rectyp_q typ with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
        let field_typ' = subst_unifiers unifiers field_typ in
        let inferred_exp = crule check_exp env exp field_typ' in
@@ -2797,6 +2851,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        let f, t, is_dec = match ord with
          | Ord_aux (Ord_inc, _) -> f, t, false
          | Ord_aux (Ord_dec, _) -> t, f, true (* reverse direction to typechecking downto as upto loop *)
+         | Ord_aux (Ord_var _, _) -> typ_error l "Cannot check a loop with variable direction!" (* This should never happen *)
        in
        let inferred_f = irule infer_exp env f in
        let inferred_t = irule infer_exp env t in
@@ -2852,6 +2907,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
                             mk_typ_arg (Typ_arg_nexp (nint (List.length vec)));
                             mk_typ_arg (Typ_arg_order (Env.get_default_order env));
                             mk_typ_arg (Typ_arg_typ (typ_of inferred_item))]))
+       | Ord_aux (Ord_var _, _) -> typ_error l default_order_error_string
      in
      annot_exp (E_vector (inferred_item :: checked_items)) vec_typ
   | E_assert (test, msg) ->
@@ -2903,7 +2959,10 @@ and instantiation_of (E_aux (exp_aux, (l, _)) as exp) =
 
 and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
   let annot_exp exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in
-  let switch_annot env typ (E_aux (exp, (l, Some (_, _, eff)))) = E_aux (exp, (l, Some (env, typ, eff))) in
+  let switch_annot env typ = function
+    | (E_aux (exp, (l, Some (_, _, eff)))) -> E_aux (exp, (l, Some (env, typ, eff)))
+    | _ -> failwith "Cannot switch annot for unannotated function"
+  in
   let all_unifiers = ref KBindings.empty in
   let ex_goal = ref None in
   let prove_goal env = match !ex_goal with
@@ -2961,6 +3020,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
                 let enc = List.fold_left (fun nc kid -> nc_subst_nexp kid (Nexp_var (prepend_kid ex_tag kid)) nc) enc ex_kids in
                 let env = List.fold_left (fun env kid -> Env.add_typ_var (prepend_kid ex_tag kid) BK_nat env) env ex_kids in
                 Env.add_constraint enc env
+             | _, None -> assert false (* Cannot have ex_kids without ex_nc *)
            in
            let tag_unifier uvar = List.fold_left (fun uvar kid -> uvar_subst_nexp kid (Nexp_var (prepend_kid ex_tag kid)) uvar) uvar ex_kids in
            let unifiers = KBindings.map tag_unifier unifiers in
@@ -3199,12 +3259,6 @@ and propagate_exp_effect_aux = function
   | E_field (exp, id) ->
      let p_exp = propagate_exp_effect exp in
      E_field (p_exp, id), effect_of p_exp
-  | E_internal_let (lexp, exp, body) ->
-     let p_lexp = propagate_lexp_effect lexp in
-     let p_exp = propagate_exp_effect exp in
-     let p_body = propagate_exp_effect body in
-     E_internal_let (p_lexp, p_exp, p_body),
-     union_effects (effect_of_lexp p_lexp) (collect_effects [p_exp; p_body])
   | E_internal_plet (pat, exp, body) ->
      let p_pat = propagate_pat_effect pat in
      let p_exp = propagate_exp_effect exp in
@@ -3322,7 +3376,6 @@ and propagate_lexp_effect_aux = function
   | LEXP_field (lexp, id) ->
      let p_lexp = propagate_lexp_effect lexp in
      LEXP_field (p_lexp, id),effect_of_lexp p_lexp
-  | _ -> typ_error Parse_ast.Unknown "Unimplemented: Cannot propagate effect in lexp"
 
 (**************************************************************************)
 (* 6. Checking toplevel definitions                                       *)
@@ -3411,12 +3464,16 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
     | None -> typ_error l "funcl list is empty"
   in
   typ_print ("\nChecking function " ^ string_of_id id);
-  let have_val_spec, (quant, (Typ_aux (Typ_fn (vtyp_arg, vtyp_ret, declared_eff), vl) as typ)), env =
+  let have_val_spec, (quant, typ), env =
     try true, Env.get_val_spec id env, env with
     | Type_error (l, _) ->
        let (quant, typ) = infer_funtyp l env tannotopt funcls in
        false, (quant, typ), env
   in
+  let vtyp_arg, vtyp_ret, declared_eff, vl = match typ with
+    | Typ_aux (Typ_fn (vtyp_arg, vtyp_ret, declared_eff), vl) -> vtyp_arg, vtyp_ret, declared_eff, vl
+    | _ -> typ_error l "Function val spec was not a function type"
+  in
   check_tannotopt env quant vtyp_ret tannotopt;
   typ_debug ("Checking fundef " ^ string_of_id id ^ " has type " ^ string_of_bind (quant, typ));
   let funcl_env = add_typquant quant env in
@@ -3488,6 +3545,7 @@ let kinded_id_arg kind_id =
      typ_arg (Typ_arg_order (Ord_aux (Ord_var kid, Parse_ast.Unknown)))
   | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), kid), _) ->
      typ_arg (Typ_arg_typ (mk_typ (Typ_var kid)))
+  | KOpt_aux (KOpt_kind (K_aux (K_kind kinds, _), kid), l) -> typ_error l "Badly formed kind"
 
 let fold_union_quant quants (QI_aux (qi, l)) =
   match qi with
diff --git a/src/type_check.mli b/src/type_check.mli
index 1931ce03..9a61f196 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -113,7 +113,8 @@ module Env : sig
 
   val is_record : id -> t -> bool
 
-  val get_accessor : id -> id -> t -> typquant * typ
+  (* Return type is: quantifier, argument type, return type, effect *)
+  val get_accessor : id -> id -> t -> typquant * typ * typ * effect
 
   (* If the environment is checking a function, then this will get the
      expected return type of the function. It's useful for checking or
diff --git a/src/value.ml b/src/value.ml
index 4974ca83..f49b230c 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -69,6 +69,7 @@ let rec string_of_value = function
   | V_bool false -> "false"
   | V_bit B0 -> "bitzero"
   | V_bit B1 -> "bitone"
+  | V_int n -> Big_int.to_string n
   | V_tuple vals -> "(" ^ Util.string_of_list ", " string_of_value vals ^ ")"
   | V_list vals -> "[" ^ Util.string_of_list ", " string_of_value vals ^ "]"
   | V_unit -> "()"
@@ -89,9 +90,17 @@ let coerce_bool = function
   | V_bool b -> b
   | _ -> assert false
 
-let and_bool [v1; v2] = V_bool (coerce_bool v1 && coerce_bool v2)
-let or_bool [v1; v2] = V_bool (coerce_bool v1 || coerce_bool v2)
-let print [v] = print_endline (string_of_value v |> Util.red |> Util.clear); V_unit
+let and_bool = function
+  | [v1; v2] -> V_bool (coerce_bool v1 && coerce_bool v2)
+  | _ -> assert false
+
+let or_bool = function
+  | [v1; v2] -> V_bool (coerce_bool v1 || coerce_bool v2)
+  | _ -> assert false
+
+let print = function
+  | [v] -> print_endline (string_of_value v |> Util.red |> Util.clear); V_unit
+  | _ -> assert false
 
 let tuple_value (vs : value list) : value = V_tuple vs