Make type annotations abstract in type_check.mli

Rather than exporting the implementation of type annotations as

type tannot = (Env.t * typ * effect) option

we leave it abstract as

type tannot

Some additional functions have been added to type_check.mli to work
with these abstract type annotations. Most use cases where the type
was constructed explicitly can be handled by using either mk_tannot or
empty_tannot. For pattern matching on a tannot there is a function

val destruct_tannot : tannot -> (Env.t * typ * effect) option

Note that it is specifically not guaranteed that using mk_tannot on
the elements returned by destruct_tannot re-constructs the same
tannot, as destruct_tannot is only used to give the old view of a type
annotation, and we may add additional information that will not be
returned by destruct_tannot.

13 files changed, 243 insertions, 191 deletions

diff --git a/src/anf.ml b/src/anf.ml
index d0803d4f..97565b2b 100644
--- a/src/anf.ml
+++ b/src/anf.ml
@@ -660,7 +660,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
      failwith ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF")
 
   | E_let (LB_aux (LB_val (pat, binding), _), body) ->
-     anf (E_aux (E_case (binding, [Pat_aux (Pat_exp (pat, body), (Parse_ast.Unknown, None))]), exp_annot))
+     anf (E_aux (E_case (binding, [Pat_aux (Pat_exp (pat, body), (Parse_ast.Unknown, empty_tannot))]), exp_annot))
 
   | E_tuple exps ->
      let aexps = List.map anf exps in
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 781069eb..3c6cbeb2 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -633,11 +633,6 @@ and string_of_n_constraint = function
   | NC_aux (NC_true, _) -> "true"
   | NC_aux (NC_false, _) -> "false"
 
-let string_of_annot = function
-  | Some (_, typ, eff) ->
-     "Some (_, " ^ string_of_typ typ ^ ", " ^ string_of_effect eff ^ ")"
-  | None -> "None"
-
 let string_of_quant_item_aux = function
   | QI_id (KOpt_aux (KOpt_none kid, _)) -> string_of_kid kid
   | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> "(" ^ string_of_kid kid ^ " :: " ^ string_of_kind k ^ ")"
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 083b81e0..545e669d 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -209,7 +209,6 @@ val string_of_nexp : nexp -> string
 val string_of_typ : typ -> string
 val string_of_typ_arg : typ_arg -> string
 val string_of_typ_pat : typ_pat -> string
-val string_of_annot : ('a * typ * effect) option -> string
 val string_of_n_constraint : n_constraint -> string
 val string_of_quant_item : quant_item -> string
 val string_of_typquant : typquant -> string
diff --git a/src/interpreter.ml b/src/interpreter.ml
index e4f7faf0..9a1d0ed2 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -135,7 +135,7 @@ let is_false = function
   | (E_aux (E_internal_value (V_bool b), _)) -> b == false
   | _ -> false
 
-let exp_of_value v = (E_aux (E_internal_value v, (Parse_ast.Unknown, None)))
+let exp_of_value v = (E_aux (E_internal_value v, (Parse_ast.Unknown, Type_check.empty_tannot)))
 let value_of_exp = function
   | (E_aux (E_internal_value v, _)) -> v
   | _ -> failwith "value_of_exp coerction failed"
@@ -589,7 +589,6 @@ and exp_of_lexp (LEXP_aux (lexp_aux, _) as lexp) =
   | LEXP_field (lexp, id) -> mk_exp (E_field (exp_of_lexp lexp, id))
 
 and pattern_match env (P_aux (p_aux, _) as pat) value =
-  (* print_endline ("Matching: " ^ string_of_pat pat ^ " with " ^ string_of_value value |> Util.yellow |> Util.clear); *)
   match p_aux with
   | P_lit lit -> eq_value (value_of_lit lit) value, Bindings.empty
   | P_wild -> true, Bindings.empty
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 9acb6052..3e7ef970 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -175,8 +175,8 @@ let pat_id_is_variable env id =
 
 let rec is_value (E_aux (e,(l,annot))) =
   let is_constructor id =
-    match annot with
-    | None -> 
+    match destruct_tannot annot with
+    | None ->
        (Reporting_basic.print_err false true l "Monomorphisation"
           ("Missing type information for identifier " ^ string_of_id id);
         false) (* Be conservative if we have no info *)
@@ -485,9 +485,13 @@ let reduce_nexp subst ne =
 
 let typ_of_args args =
   match args with
-  | [E_aux (E_tuple args,(_,Some (_,Typ_aux (Typ_exist _,_),_)))] ->
-     let tys = List.map Type_check.typ_of args in
-     Typ_aux (Typ_tup tys,Unknown)
+  | [(E_aux (E_tuple args, (_, tannot)) as exp)] ->
+     begin match destruct_tannot tannot with
+     | Some (_,Typ_aux (Typ_exist _,_),_) ->
+        let tys = List.map Type_check.typ_of args in
+        Typ_aux (Typ_tup tys,Unknown)
+     | _ -> Type_check.typ_of exp
+     end
   | [exp] ->
      Type_check.typ_of exp
   | _ ->
@@ -541,9 +545,10 @@ let nexp_subst_fns substs =
 (*  let s_typschm (TypSchm_aux (TypSchm_ts (q,t),l)) = TypSchm_aux (TypSchm_ts (q,s_t t),l) in
    hopefully don't need this anyway *)(*
   let s_typschm tsh = tsh in*)
-  let s_tannot = function
-    | None -> None
-    | Some (env,t,eff) -> Some (env,s_t t,eff) (* TODO: what about env? *)
+  let s_tannot tannot =
+    match destruct_tannot tannot with
+    | None -> empty_tannot
+    | Some (env,t,eff) -> mk_tannot env (s_t t) eff (* TODO: what about env? *)
   in
   let rec s_pat (P_aux (p,(l,annot))) =
     let re p = P_aux (p,(l,s_tannot annot)) in
@@ -706,7 +711,8 @@ let fabricate_nexp_exist env l typ kids nc typ' =
   | _ -> raise (Reporting_basic.err_general l
                   ("Undefined value at unsupported type " ^ string_of_typ typ))
 
-let fabricate_nexp l = function
+let fabricate_nexp l tannot =
+  match destruct_tannot tannot with
   | None -> nint 32
   | Some (env,typ,_) ->
      match Type_check.destruct_exist env typ with
@@ -725,10 +731,6 @@ let atom_typ_kid kid = function
 
 let reduce_cast typ exp l annot =
   let env = env_of_annot (l,annot) in
-  let replace_typ typ = function
-    | Some (env,_,eff) -> Some (env,typ,eff)
-    | None -> None
-  in
   let typ' = Env.base_typ_of env typ in
   match exp, destruct_exist env typ' with
   | E_aux (E_lit (L_aux (L_num n,_)),_), Some ([kid],nc,typ'') when atom_typ_kid kid typ'' ->
@@ -831,11 +833,10 @@ let try_app (l,ann) (id,args) =
     | _ -> None
   else if is_id "slice" then
     match args with
-    | [E_aux (E_lit (L_aux ((L_hex _| L_bin _),_) as lit),
-              (_,Some (vec_env,vec_typ,_)));
+    | [E_aux (E_lit (L_aux ((L_hex _| L_bin _),_) as lit), annot);
        E_aux (E_lit L_aux (L_num i,_), _);
        E_aux (E_lit L_aux (L_num len,_), _)] ->
-       (match Env.base_typ_of vec_env vec_typ with
+       (match Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) with
        | Typ_aux (Typ_app (_,[_;Typ_arg_aux (Typ_arg_order ord,_);_]),_) ->
           (match slice_lit lit i len ord with
           | Some lit' -> Some (E_aux (E_lit lit',(l,ann)))
@@ -996,7 +997,7 @@ let rec freshen_pat_bindings p =
        (mkp (P_not r), vs)
     | P_as (p,_) -> aux p
     | P_typ (typ,p) -> let p',vs = aux p in mkp (P_typ (typ,p')),vs
-    | P_id id -> let id' = freshen_id id in mkp (P_id id'),[id,E_aux (E_id id',(Generated Unknown,None))]
+    | P_id id -> let id' = freshen_id id in mkp (P_id id'),[id,E_aux (E_id id',(Generated Unknown,empty_tannot))]
     | P_var (p,_) -> aux p
     | P_app (id,args) ->
        let args',vs = List.split (List.map aux args) in
@@ -1031,7 +1032,7 @@ let rec freshen_pat_bindings p =
 let stop_at_false_assertions e =
   let dummy_value_of_typ typ =
     let l = Generated Unknown in
-    E_aux (E_exit (E_aux (E_lit (L_aux (L_unit,l)),(l,None))),(l,None))
+    E_aux (E_exit (E_aux (E_lit (L_aux (L_unit,l)),(l,empty_tannot))),(l,empty_tannot))
   in
   let rec nc_false (NC_aux (nc,_)) =
     match nc with
@@ -1130,7 +1131,7 @@ let apply_pat_choices choices =
     | choice,max,subst ->
        (match List.nth cases choice with
        | Pat_aux (Pat_exp (p,E_aux (e,_)),_) ->
-          let dummyannot = (Generated Unknown,None) in
+          let dummyannot = (Generated Unknown,empty_tannot) in
           (* TODO: use a proper substitution *)
           List.fold_left (fun e (id,e') ->
             E_let (LB_aux (LB_val (P_aux (P_id id, dummyannot),e'),dummyannot),E_aux (e,dummyannot))) e subst
@@ -1386,7 +1387,7 @@ let split_defs all_errors splits defs =
               re (E_let (LB_aux (LB_val (p,e'), annot),
                          e2')) assigns in
             if is_value e' && not (is_value e) then
-              match can_match ref_vars e' [Pat_aux (Pat_exp (p,e2),(Unknown,None))] substs assigns with
+              match can_match ref_vars e' [Pat_aux (Pat_exp (p,e2),(Unknown,empty_tannot))] substs assigns with
               | None -> plain ()
               | Some (e'',bindings,kbindings) ->
                  let e'' = nexp_subst_exp (kbindings_from_list kbindings) e'' in
@@ -1490,9 +1491,9 @@ let split_defs all_errors splits defs =
       | Some (eff,_) when not (is_pure eff) -> None
       | Some (_,fcls) ->
          let arg = match args with
-           | [] -> E_aux (E_lit (L_aux (L_unit,Generated l)),(Generated l,None))
+           | [] -> E_aux (E_lit (L_aux (L_unit,Generated l)),(Generated l,empty_tannot))
            | [e] -> e
-           | _ -> E_aux (E_tuple args,(Generated l,None)) in
+           | _ -> E_aux (E_tuple args,(Generated l,empty_tannot)) in
          let cases = List.map (function
            | FCL_aux (FCL_Funcl (_,pexp), ann) -> pexp)
            fcls in
@@ -1576,7 +1577,7 @@ let split_defs all_errors splits defs =
               | L_undef ->
                  let nexp = fabricate_nexp l annot in
                  let typ = subst_src_typ (KBindings.singleton kid nexp) (typ_of_annot p_id_annot) in
-                 DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,None))),(l,None))],
+                 DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,empty_tannot))),(l,empty_tannot))],
                             [kid,nexp])
               | _ ->
                  (Reporting_basic.print_err false true lit_l "Monomorphisation"
@@ -1622,7 +1623,7 @@ let split_defs all_errors splits defs =
             let kids = equal_kids (env_of_annot p_id_annot) kid in
             let ksubst = KidSet.fold (fun k b -> KBindings.add k nexp b) kids KBindings.empty in
             let typ = subst_src_typ ksubst (typ_of_annot p_id_annot) in
-            DoesMatch ([id, E_aux (E_cast (typ,e_undef),(l,None))],
+            DoesMatch ([id, E_aux (E_cast (typ,e_undef),(l,empty_tannot))],
                        KBindings.bindings ksubst)
          | P_aux (_,(l',_)) ->
             (Reporting_basic.print_err false true l' "Monomorphisation"
@@ -2180,22 +2181,23 @@ and sizes_of_typarg (Typ_arg_aux (ta,_)) =
     -> KidSet.empty
   | Typ_arg_typ typ -> sizes_of_typ typ
 
-let sizes_of_annot = function
-  | _,None -> KidSet.empty
-  | _,Some (env,typ,_) -> sizes_of_typ (Env.base_typ_of env typ)
+let sizes_of_annot (l, tannot) =
+  match destruct_tannot tannot with
+  | None -> KidSet.empty
+  | Some (env,typ,_) -> sizes_of_typ (Env.base_typ_of env typ)
 
 let change_parameter_pat i = function
   | P_aux (P_id var, (l,_))
   | P_aux (P_typ (_,P_aux (P_id var, (l,_))),_) ->
-     P_aux (P_id var, (l,None)), ([var],[])
+     P_aux (P_id var, (l,empty_tannot)), ([var],[])
   | P_aux (P_lit lit,(l,_)) ->
      let var = mk_id ("p#" ^ string_of_int i) in
-     let annot = (Generated l, None) in
+     let annot = (Generated l, empty_tannot) in
      let test : tannot exp =
        E_aux (E_app_infix (E_aux (E_app (mk_id "size_itself_int",[E_aux (E_id var,annot)]),annot),
                            mk_id "==",
                            E_aux (E_lit lit,annot)), annot) in
-     P_aux (P_id var, (l,None)), ([],[test])
+     P_aux (P_id var, (l,empty_tannot)), ([],[test])
   | P_aux (_,(l,_)) -> raise (Reporting_basic.err_unreachable l
                                 "Expected variable pattern")
 
@@ -2214,7 +2216,7 @@ let var_maybe_used_in_exp exp var =
 let add_var_rebind unconditional exp var =
   if unconditional || var_maybe_used_in_exp exp var then
     let l = Generated Unknown in
-    let annot = (l,None) in
+    let annot = (l,empty_tannot) in
     E_aux (E_let (LB_aux (LB_val (P_aux (P_id var,annot),
                                   E_aux (E_app (mk_id "size_itself_int",[E_aux (E_id var,annot)]),annot)),annot),exp),annot)
   else exp
@@ -2241,8 +2243,8 @@ let replace_with_the_value bound_nexps (E_aux (_,(l,_)) as exp) =
     let nexp = replace_size nexp in
     E_aux (E_cast (wrap (Typ_aux (Typ_app (Id_aux (Id "itself",Generated Unknown),
                                            [Typ_arg_aux (Typ_arg_nexp nexp,l')]),Generated Unknown)),
-                   E_aux (E_app (Id_aux (Id "make_the_value",Generated Unknown),[exp]),(Generated l,None))),
-           (Generated l,None))
+                   E_aux (E_app (Id_aux (Id "make_the_value",Generated Unknown),[exp]),(Generated l,empty_tannot))),
+           (Generated l,empty_tannot))
   in
   match typ with
   | Typ_aux (Typ_app (Id_aux (Id "range",_),
@@ -2310,7 +2312,8 @@ let rewrite_size_parameters env (Defs defs) =
  print_endline ("Nexp map for " ^ string_of_id id);
  List.iter (fun (nexp, i) -> print_endline ("  " ^ string_of_nexp nexp ^ " -> " ^ string_of_int i)) nexp_list
 in *)
-    let parameters_for = function
+    let parameters_for tannot =
+      match destruct_tannot tannot with
       | Some (env,typ,_) ->
          begin match Env.base_typ_of env typ with
          | Typ_aux (Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp size,_);_;_]),_)
@@ -2361,7 +2364,7 @@ in *)
              P_aux (P_tup pats,(l,_)) ->
                let pats, vars_guards = mapat_extra change_parameter_pat to_change pats in
                let vars, new_guards = List.split vars_guards in
-               P_aux (P_tup pats,(l,None)), vars, new_guards
+               P_aux (P_tup pats,(l,empty_tannot)), vars, new_guards
            | P_aux (_,(l,_)) ->
               begin
                 if IntSet.is_empty to_change then pat, [], []
@@ -2373,7 +2376,7 @@ in *)
          let vars, new_guards = List.concat vars, List.concat new_guards in
          let body = List.fold_left (add_var_rebind true) body vars in
          let merge_guards g1 g2 : tannot exp =
-           E_aux (E_app_infix (g1, mk_id "&", g2),(Generated Unknown,None)) in
+           E_aux (E_app_infix (g1, mk_id "&", g2),(Generated Unknown,empty_tannot)) in
          let guard = match guard, new_guards with
            | None, [] -> None
            | None, (h::t) -> Some (List.fold_left merge_guards h t)
@@ -2403,7 +2406,7 @@ in *)
     let guard = match guard with
       | None -> None
       | Some exp -> Some (fold_exp { id_exp_alg with e_app = rewrite_e_app } exp) in
-    FCL_aux (FCL_Funcl (id,construct_pexp (pat,guard,body,(pl,None))),(l,None))
+    FCL_aux (FCL_Funcl (id,construct_pexp (pat,guard,body,(pl,empty_tannot))),(l,empty_tannot))
   in
   let rewrite_letbind lb =
     let rewrite_e_app (id,args) =
@@ -2417,7 +2420,7 @@ in *)
   let rewrite_def = function
     | DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,funcls),(l,_))) ->
        (* TODO rewrite tannopt? *)
-       DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,List.map rewrite_funcl funcls),(l,None)))
+       DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,List.map rewrite_funcl funcls),(l,empty_tannot)))
     | DEF_val lb -> DEF_val (rewrite_letbind lb)
     | DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,annot))) as spec ->
        begin
@@ -2433,7 +2436,7 @@ in *)
                    | _ -> replace_type env typ
                  in TypSchm_aux (TypSchm_ts (tq,typ),l)
             in
-            DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,None)))
+            DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,empty_tannot)))
          | _ -> spec
          | exception Not_found -> spec
        end
@@ -2740,11 +2743,11 @@ let kids_bound_by_pat pat =
   let open Rewriter in
   fst (fold_pat ({ (compute_pat_alg KidSet.empty KidSet.union)
     with p_aux =
-      (function ((s,(P_var (P_aux (_,(_,Some (_,typ,_))),tpat) as p)), (_,Some (env,_,_) as ann)) ->
-        let kids = tyvars_of_typ typ in
-        let new_kids = KidSet.filter (fun kid -> not (is_kid_in_env env kid)) kids in
+      (function ((s,(P_var (P_aux (_, annot'),tpat) as p)), annot) when not (is_empty_tannot (snd annot')) ->
+        let kids = tyvars_of_typ (typ_of_annot annot') in
+        let new_kids = KidSet.filter (fun kid -> not (is_kid_in_env (env_of_annot annot) kid)) kids in
         let tpat_kids = kids_bound_by_typ_pat tpat in
-        KidSet.union s (KidSet.union new_kids tpat_kids), P_aux (p, ann)
+        KidSet.union s (KidSet.union new_kids tpat_kids), P_aux (p, annot)
       | ((s,p),ann) -> s, P_aux (p,ann))
     }) pat)
 
@@ -2853,20 +2856,20 @@ let mk_subrange_pattern vannot vstart vend =
           let end_len = Big_int.pred (Big_int.sub len vend) in
           (* Wrap pat in its type; in particular the type checker won't
              manage P_wild in the middle of a P_vector_concat *)
-          let pat = P_aux (P_typ (pat_typ_of pat, pat),(Generated (pat_loc pat),None)) in
+          let pat = P_aux (P_typ (pat_typ_of pat, pat),(Generated (pat_loc pat),empty_tannot)) in
           let pats = if Big_int.greater end_len Big_int.zero then
               [pat;P_aux (P_typ (vector_typ (nconstant end_len) ord typ,
-                                 P_aux (P_wild,(dummyl,None))),(dummyl,None))]
+                                 P_aux (P_wild,(dummyl,empty_tannot))),(dummyl,empty_tannot))]
             else [pat]
           in
           let pats = if Big_int.greater vstart Big_int.zero then
               (P_aux (P_typ (vector_typ (nconstant vstart) ord typ,
-                             P_aux (P_wild,(dummyl,None))),(dummyl,None)))::pats
+                             P_aux (P_wild,(dummyl,empty_tannot))),(dummyl,empty_tannot)))::pats
             else pats
           in
           let pats = if ord' = Ord_inc then pats else List.rev pats
           in
-          P_aux (P_vector_concat pats,(Generated (fst vannot),None)))
+          P_aux (P_vector_concat pats,(Generated (fst vannot),empty_tannot)))
      | _ -> None
 
 (* If the expression matched on in a case expression is a function argument,
@@ -3161,7 +3164,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
   in
   let r =
     (* Check for bitvector types with parametrised sizes *)
-    match annot with
+    match destruct_tannot annot with
     | None -> r
     | Some (tenv,typ,_) ->
        let typ = Env.base_typ_of tenv typ in
@@ -3209,7 +3212,7 @@ and analyse_lexp fn_id env assigns deps (LEXP_aux (lexp,(l,_))) =
      then assigns, empty
      else Bindings.add id deps assigns, empty
   | LEXP_memory (id,es) ->
-     let _, assigns, r = analyse_exp fn_id env assigns (E_aux (E_tuple es,(Unknown,None))) in
+     let _, assigns, r = analyse_exp fn_id env assigns (E_aux (E_tuple es,(Unknown,empty_tannot))) in
      assigns, r
   | LEXP_tup lexps
   | LEXP_vector_concat lexps ->
@@ -3353,7 +3356,7 @@ let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions =
       (* When there's no argument to case split on for a kid, we'll add a
          case expression instead *)
       let env = pat_env_of pat in
-      let split = default_split (Some (env,int_typ,no_effect)) (KidSet.singleton kid) in
+      let split = default_split (mk_tannot env int_typ no_effect) (KidSet.singleton kid) in
       let extra_splits = ExtraSplits.singleton (fn_id, fn_l)
         (KBindings.singleton kid split) in
       KBindings.add kid (Have (ArgSplits.empty, extra_splits)) kid_deps
@@ -3585,7 +3588,7 @@ let add_extra_splits extras (Defs defs) =
     KBindings.fold (fun kid detail (exp,split_list) ->
          let nexp = Nexp_aux (Nexp_var kid,l) in
          let var = fresh_sz_var () in
-         let size_annot = Some (env_of e,atom_typ nexp,no_effect) in
+         let size_annot = mk_tannot (env_of e) (atom_typ nexp) no_effect in
          let loc = match Analysis.translate_loc l with
            | Some l -> l
            | None ->
@@ -3666,7 +3669,7 @@ let rewrite_app env typ (id,args) =
                E_aux (E_cast (midtyp,
                               E_aux (E_app (mk_id "subrange_subrange_concat",
                                             [vector1; start1; end1; vector2; start2; end2]),
-                                     (Unknown,None))),(Unknown,None))])
+                                     (Unknown,empty_tannot))),(Unknown,empty_tannot))])
     | [E_aux (E_app (append,
               [e1;
                E_aux (E_app (slice1,
@@ -3685,7 +3688,7 @@ let rewrite_app env typ (id,args) =
                E_aux (E_cast (midtyp,
                               E_aux (E_app (mk_id "slice_slice_concat",
                                             [vector1; start1; length1; vector2; start2; length2]),
-                                     (Unknown,None))),(Unknown,None))])
+                                     (Unknown,empty_tannot))),(Unknown,empty_tannot))])
 
     (* variable-range @ variable-range *)
     | [E_aux (E_app (subrange1,
@@ -3697,7 +3700,7 @@ let rewrite_app env typ (id,args) =
        E_cast (typ,
                E_aux (E_app (mk_id "subrange_subrange_concat",
                              [vector1; start1; end1; vector2; start2; end2]),
-                      (Unknown,None)))
+                      (Unknown,empty_tannot)))
 
     (* variable-slice @ variable-slice *)
     | [E_aux (E_app (slice1,
@@ -3708,7 +3711,7 @@ let rewrite_app env typ (id,args) =
           not (is_constant length1 || is_constant length2) ->
        E_cast (typ,
                E_aux (E_app (mk_id "slice_slice_concat",
-                             [vector1; start1; length1; vector2; start2; length2]),(Unknown,None)))
+                             [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot)))
 
     | [E_aux (E_app (append1,
                      [e1;
@@ -3726,8 +3729,8 @@ let rewrite_app env typ (id,args) =
                              [e1;
                               E_aux (E_cast (midtyp,
                                              E_aux (E_app (mk_id "slice_zeros_concat",
-                                                           [vector1; start1; length1; length2]),(Unknown,None))),(Unknown,None))]),
-                      (Unknown,None)))
+                                                           [vector1; start1; length1; length2]),(Unknown,empty_tannot))),(Unknown,empty_tannot))]),
+                      (Unknown,empty_tannot)))
 
     | _ -> E_app (id,args)
 
@@ -3819,7 +3822,7 @@ let rewrite_app env typ (id,args) =
             let (_,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
             E_cast (vector_typ nlen order bittyp,
                     E_aux (E_app (mk_id "sext_slice", [vector1; start1; length1]),
-                           (Unknown,None)))
+                           (Unknown,empty_tannot)))
        end
 
     | _ -> E_app (id,args)
@@ -3840,8 +3843,12 @@ let rewrite_app env typ (id,args) =
   else E_app (id,args)
 
 let rewrite_aux = function
-  | (E_app (id,args),((_,Some (env,ty,_)) as annot)) ->
-     E_aux (rewrite_app env ty (id,args),annot)
+  | E_app (id,args), (l, tannot) ->
+     begin match destruct_tannot tannot with
+     | Some (env, ty, _) ->
+        E_aux (rewrite_app env ty (id,args), (l, tannot))
+     | None -> E_aux (E_app (id, args), (l, tannot))
+     end
   | exp,annot -> E_aux (exp,annot)
 
 let mono_rewrite defs =
@@ -3880,8 +3887,8 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ =
   in
   let at_least_one = ref None in
   let rec aux (Typ_aux (src_t,src_l) as src_typ) (Typ_aux (tar_t,tar_l) as tar_typ) =
-    let src_ann = Some (env,src_typ,no_effect) in
-    let tar_ann = Some (env,tar_typ,no_effect) in
+    let src_ann = mk_tannot env src_typ no_effect in
+    let tar_ann = mk_tannot env tar_typ no_effect in
     match src_t, tar_t with
     | Typ_tup typs, Typ_tup typs' ->
        let ps,es = List.split (List.map2 aux typs typs') in
@@ -3905,7 +3912,7 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ =
                      E_aux (E_app (Id_aux (Id "bitvector_cast", genunk),
                                    [E_aux (E_id var, (genunk, src_ann))]), (genunk, tar_ann))),
              (genunk, tar_ann))
-       | _ -> 
+       | _ ->
           let var = fresh () in
           P_aux (P_id var,(Generated src_l,src_ann)),
           E_aux (E_id var,(Generated src_l,tar_ann))
@@ -3920,13 +3927,13 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ =
   let pat, e' = aux src_typ' target_typ' in
   match !at_least_one with
   | Some one_target_typ -> begin
-    let src_ann = Some (env,src_typ,no_effect) in
-    let tar_ann = Some (env,target_typ,no_effect) in
+    let src_ann = mk_tannot env src_typ no_effect in
+    let tar_ann = mk_tannot env target_typ no_effect in
     match src_typ' with
       (* Simple case with just the bitvector; don't need to pull apart value *)
     | Typ_aux (Typ_app _,_) ->
        (fun var exp ->
-         let exp_ann = Some (env,typ_of exp,effect_of exp) in
+         let exp_ann = mk_tannot env (typ_of exp) (effect_of exp) in
          E_aux (E_let (LB_aux (LB_val (P_aux (P_typ (one_target_typ, P_aux (P_id var,(genunk,tar_ann))),(genunk,tar_ann)),
                                        E_aux (E_app (Id_aux (Id "bitvector_cast",genunk),
                                                      [E_aux (E_id var,(genunk,src_ann))]),(genunk,tar_ann))),(genunk,tar_ann)),
@@ -3937,7 +3944,7 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ =
                (Generated exp_l,tar_ann)))
     | _ ->
        (fun var exp ->
-         let exp_ann = Some (env,typ_of exp,effect_of exp) in
+         let exp_ann = mk_tannot env (typ_of exp) (effect_of exp) in
          E_aux (E_let (LB_aux (LB_val (pat, E_aux (E_id var,(genunk,src_ann))),(genunk,src_ann)),
                        E_aux (E_let (LB_aux (LB_val (P_aux (P_id var,(genunk,tar_ann)),e'),(genunk,tar_ann)),
                                      exp),(genunk,exp_ann))),(genunk,exp_ann))),
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index ebb703db..713cfb34 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1066,7 +1066,7 @@ let doc_exp_lem, doc_let_lem =
       raise (Reporting_basic.err_unreachable l
         "E_vector_subrange should have been rewritten before pretty-printing")
     | E_field((E_aux(_,(l,fannot)) as fexp),id) ->
-       (match fannot with
+       (match destruct_tannot fannot with
         | Some(env, (Typ_aux (Typ_id tid, _)), _)
         | Some(env, (Typ_aux (Typ_app (tid, _), _)), _)
           when Env.is_record tid env ->
@@ -1115,23 +1115,23 @@ let doc_exp_lem, doc_let_lem =
     | E_tuple exps ->
        parens (align (group (separate_map (comma ^^ break 1) expN exps)))
     | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
-       let recordtyp = match annot with
+       let recordtyp = match destruct_tannot annot with
          | Some (env, Typ_aux (Typ_id tid,_), _)
          | Some (env, Typ_aux (Typ_app (tid, _), _), _) ->
            (* when Env.is_record tid env -> *)
            tid
-         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
+         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in
        let epp = enclose_record (align (separate_map
                                           (semi_sp ^^ break 1)
                                           (doc_fexp ctxt recordtyp) fexps)) in
        if aexp_needed then parens epp else epp
     | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
-       let recordtyp, env = match annot with
+       let recordtyp, env = match destruct_tannot annot with
          | Some (env, Typ_aux (Typ_id tid,_), _)
          | Some (env, Typ_aux (Typ_app (tid, _), _), _)
            when Env.is_record tid env ->
            tid, env
-         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
+         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in
        if List.length fexps > 1 then
          let _,fields = Env.get_record recordtyp env in
          let var, let_pp =
@@ -1464,8 +1464,8 @@ let doc_typdef (TD_aux(td, (l, annot))) = match td with
 let args_of_typ l env typs =
   let arg i typ =
     let id = mk_id ("arg" ^ string_of_int i) in
-    (P_aux (P_id id, (l, Some (env, typ, no_effect))), typ),
-    E_aux (E_id id, (l, Some (env, typ, no_effect))) in
+    (P_aux (P_id id, (l, mk_tannot env typ no_effect)), typ),
+    E_aux (E_id id, (l, mk_tannot env typ no_effect)) in
   List.split (List.mapi arg typs)
 
 let rec untuple_args_pat typ (P_aux (paux, ((l, _) as annot)) as pat) =
@@ -1479,12 +1479,12 @@ let rec untuple_args_pat typ (P_aux (paux, ((l, _) as annot)) as pat) =
   let identity = (fun body -> body) in
   match paux, tup_typs with
   | P_tup [], _ ->
-     let annot = (l, Some (Env.empty, unit_typ, no_effect)) in
+     let annot = (l, mk_tannot Env.empty unit_typ no_effect) in
      [P_aux (P_lit (mk_lit L_unit), annot), unit_typ], identity
   | P_tup pats, Some typs -> List.combine pats typs, identity
   | P_tup pats, _ -> raise (Reporting_basic.err_unreachable l "Tuple pattern against non-tuple type")
   | P_wild, Some typs ->
-     let wild typ = P_aux (P_wild, (l, Some (env, typ, no_effect))), typ in
+     let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)), typ in
      List.map wild typs, identity
   | P_typ (_, pat), _ -> untuple_args_pat typ pat
   | P_as _, Some typs | P_id _, Some typs ->
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index a4d446d3..75284418 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -740,7 +740,7 @@ let doc_exp_lem, doc_let_lem =
                "Unexpected number of arguments for early_return builtin")
           end
        | _ ->
-          begin match annot with
+          begin match destruct_tannot annot with
           | Some (env, _, _) when Env.is_union_constructor f env ->
              let epp =
                match args with
@@ -751,7 +751,7 @@ let doc_exp_lem, doc_let_lem =
                     parens (separate_map comma (expV false) args) in
              wrap_parens (align epp)
           | _ ->
-             let call, is_extern = match annot with
+             let call, is_extern = match destruct_tannot annot with
                | Some (env, _, _) when Env.is_extern f env "lem" ->
                  string (Env.get_extern f env "lem"), true
                | _ -> doc_id_lem f, false in
@@ -774,7 +774,7 @@ let doc_exp_lem, doc_let_lem =
         "E_vector_subrange should have been rewritten before pretty-printing")
     | E_field((E_aux(_,(l,fannot)) as fexp),id) ->
        let ft = typ_of_annot (l,fannot) in
-       (match fannot with
+       (match destruct_tannot fannot with
         | Some(env, (Typ_aux (Typ_id tid, _)), _)
         | Some(env, (Typ_aux (Typ_app (tid, _), _)), _)
           when Env.is_record tid env ->
@@ -806,22 +806,22 @@ let doc_exp_lem, doc_let_lem =
     | E_tuple exps ->
        parens (align (group (separate_map (comma ^^ break 1) expN exps)))
     | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
-       let recordtyp = match annot with
+       let recordtyp = match destruct_tannot annot with
          | Some (env, Typ_aux (Typ_id tid,_), _)
          | Some (env, Typ_aux (Typ_app (tid, _), _), _) ->
            (* when Env.is_record tid env -> *)
            tid
-         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
+         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in
        wrap_parens (anglebars (space ^^ (align (separate_map
                                         (semi_sp ^^ break 1)
                                         (doc_fexp ctxt recordtyp) fexps)) ^^ space))
     | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
-       let recordtyp = match annot with
+       let recordtyp = match destruct_tannot annot with
          | Some (env, Typ_aux (Typ_id tid,_), _)
          | Some (env, Typ_aux (Typ_app (tid, _), _), _)
            when Env.is_record tid env ->
            tid
-         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
+         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in
        anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps))
     | E_vector exps ->
        let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
@@ -1211,8 +1211,8 @@ let args_of_typ l env typ =
     | typ -> [typ] in
   let arg i typ =
     let id = mk_id ("arg" ^ string_of_int i) in
-    P_aux (P_id id, (l, Some (env, typ, no_effect))),
-    E_aux (E_id id, (l, Some (env, typ, no_effect))) in
+    P_aux (P_id id, (l, mk_tannot env typ no_effect)),
+    E_aux (E_id id, (l, mk_tannot env typ no_effect)) in
   List.split (List.mapi arg typs)
 
 let rec untuple_args_pat (P_aux (paux, ((l, _) as annot)) as pat) =
@@ -1221,11 +1221,11 @@ let rec untuple_args_pat (P_aux (paux, ((l, _) as annot)) as pat) =
   let identity = (fun body -> body) in
   match paux, taux with
   | P_tup [], _ ->
-     let annot = (l, Some (Env.empty, unit_typ, no_effect)) in
+     let annot = (l, mk_tannot Env.empty unit_typ no_effect) in
      [P_aux (P_lit (mk_lit L_unit), annot)], identity
   | P_tup pats, _ -> pats, identity
   | P_wild, Typ_tup typs ->
-     let wild typ = P_aux (P_wild, (l, Some (env, typ, no_effect))) in
+     let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)) in
      List.map wild typs, identity
   | P_typ (_, pat), _ -> untuple_args_pat pat
   | P_as _, Typ_tup _ | P_id _, Typ_tup _ ->
diff --git a/src/rewriter.ml b/src/rewriter.ml
index f072f91f..01ff62b1 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -81,7 +81,7 @@ let effect_of_pexp (Pat_aux (pexp,(_,a))) =
   union_effects eff (effect_of_annot a)
 let effect_of_lb (LB_aux (_,(_,a))) = effect_of_annot a
 
-let simple_annot l typ = (gen_loc l, Some (initial_env, typ, no_effect))
+let simple_annot l typ = (gen_loc l, mk_tannot initial_env typ no_effect)
 
 
 let lookup_generated_kid env kid =
@@ -138,7 +138,7 @@ let fun_app_effects id env =
   with
   | _ -> no_effect
 
-let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
+let fix_eff_exp (E_aux (e,((l,_) as annot))) = match destruct_tannot (snd annot) with
 | Some (env, typ, eff) ->
   let effsum = match e with
     | E_block es -> union_eff_exps es
@@ -180,11 +180,11 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
     | E_internal_return e1 -> effect_of e1
     | E_internal_value v -> no_effect
   in
-  E_aux (e, (l, Some (env, typ, effsum)))
+  E_aux (e, (l, mk_tannot env typ effsum))
 | None ->
-  E_aux (e, (l, None))
+  E_aux (e, (l, empty_tannot))
 
-let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match snd annot with
+let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match destruct_tannot (snd annot) with
 | Some (env, typ, eff) ->
   let effsum = union_effects eff (match lexp with
     | LEXP_id _ -> no_effect
@@ -200,45 +200,45 @@ let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match snd annot with
       union_effects (effect_of_lexp lexp)
         (union_effects (effect_of e1) (effect_of e2))
     | LEXP_field (lexp,_) -> effect_of_lexp lexp) in
-  LEXP_aux (lexp, (l, Some (env, typ, effsum)))
+  LEXP_aux (lexp, (l, mk_tannot env typ effsum))
 | None ->
-  LEXP_aux (lexp, (l, None))
+  LEXP_aux (lexp, (l, empty_tannot))
 
-let fix_eff_fexp (FE_aux (fexp,((l,_) as annot))) = match snd annot with
+let fix_eff_fexp (FE_aux (fexp,((l,_) as annot))) = match destruct_tannot (snd annot) with
 | Some (env, typ, eff) ->
   let effsum = union_effects eff (match fexp with
     | FE_Fexp (_,e) -> effect_of e) in
-  FE_aux (fexp, (l, Some (env, typ, effsum)))
+  FE_aux (fexp, (l, mk_tannot env typ effsum))
 | None ->
-  FE_aux (fexp, (l, None))
+  FE_aux (fexp, (l, empty_tannot))
 
 let fix_eff_fexps fexps = fexps (* FES_aux have no effect information *)
 
-let fix_eff_opt_default (Def_val_aux (opt_default,((l,_) as annot))) = match snd annot with
+let fix_eff_opt_default (Def_val_aux (opt_default,((l,_) as annot))) = match destruct_tannot (snd annot) with
 | Some (env, typ, eff) ->
   let effsum = union_effects eff (match opt_default with
     | Def_val_empty -> no_effect
     | Def_val_dec e -> effect_of e) in
-  Def_val_aux (opt_default, (l, Some (env, typ, effsum)))
+  Def_val_aux (opt_default, (l, mk_tannot env typ effsum))
 | None ->
-  Def_val_aux (opt_default, (l, None))
+  Def_val_aux (opt_default, (l, empty_tannot))
 
-let fix_eff_pexp (Pat_aux (pexp,((l,_) as annot))) = match snd annot with
+let fix_eff_pexp (Pat_aux (pexp,((l,_) as annot))) = match destruct_tannot (snd annot) with
 | Some (env, typ, eff) ->
   let effsum = match pexp with
     | Pat_exp (_,e) -> effect_of e
     | Pat_when (_,e,e') -> union_effects (effect_of e) (effect_of e') in
-  Pat_aux (pexp, (l, Some (env, typ, effsum)))
+  Pat_aux (pexp, (l, mk_tannot env typ effsum))
 | None ->
-  Pat_aux (pexp, (l, None))
+  Pat_aux (pexp, (l, empty_tannot))
 
-let fix_eff_lb (LB_aux (lb,((l,_) as annot))) = match snd annot with
+let fix_eff_lb (LB_aux (lb,((l,_) as annot))) = match destruct_tannot (snd annot) with
 | Some (env, typ, eff) ->
   let effsum = match lb with
     | LB_val (_,e) -> effect_of e in
-  LB_aux (lb, (l, Some (env, typ, effsum)))
+  LB_aux (lb, (l, mk_tannot env typ effsum))
 | None ->
-  LB_aux (lb, (l, None))
+  LB_aux (lb, (l, empty_tannot))
 
 let explode s =
   let rec exp i l = if i < 0 then l else exp (i - 1) (s.[i] :: l) in
@@ -287,7 +287,7 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot)) as orig_pat) =
   let rewrite = rewriters.rewrite_pat rewriters in
   match pat with
   | P_lit (L_aux ((L_hex _ | L_bin _) as lit,_)) ->
-    let ps =  List.map (fun p -> P_aux (P_lit p, (l, Some (pat_env_of orig_pat, bit_typ, no_effect))))
+    let ps =  List.map (fun p -> P_aux (P_lit p, (l, mk_tannot (pat_env_of orig_pat) bit_typ no_effect)))
         (vector_string_to_bit_list l lit) in
     rewrap (P_vector ps)
   | P_lit _ | P_wild | P_id _ | P_var _ -> rewrap pat
@@ -313,7 +313,7 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) =
   | E_block exps -> rewrap (E_block (List.map rewrite exps))
   | E_nondet exps -> rewrap (E_nondet (List.map rewrite exps))
   | E_lit (L_aux ((L_hex _ | L_bin _) as lit,_)) ->
-    let es = List.map (fun p -> E_aux (E_lit p, (l, Some (env_of orig_exp, bit_typ, no_effect))))
+    let es = List.map (fun p -> E_aux (E_lit p, (l, mk_tannot (env_of orig_exp) bit_typ no_effect)))
         (vector_string_to_bit_list l lit) in
     rewrap (E_vector es)
   | E_id _ | E_lit _  -> rewrap exp
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 5a903a40..5ed174ea 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -83,11 +83,11 @@ let get_loc_exp (E_aux (_,(l,_))) = l
 
 let gen_vs (id, spec) = Initial_check.extern_of_string dec_ord (mk_id id) spec
 
-let annot_exp_effect e_aux l env typ effect = E_aux (e_aux, (l, Some (env, typ, effect)))
+let annot_exp_effect e_aux l env typ effect = E_aux (e_aux, (l, mk_tannot env typ effect))
 let annot_exp e_aux l env typ = annot_exp_effect e_aux l env typ no_effect
-let annot_pat p_aux l env typ = P_aux (p_aux, (l, Some (env, typ, no_effect)))
+let annot_pat p_aux l env typ = P_aux (p_aux, (l, mk_tannot env typ no_effect))
 let annot_letbind (p_aux, exp) l env typ =
-  LB_aux (LB_val (annot_pat p_aux l env typ, exp), (l, Some (env, typ, effect_of exp)))
+  LB_aux (LB_val (annot_pat p_aux l env typ, exp), (l, mk_tannot env typ (effect_of exp)))
 
 let simple_num l n = E_aux (
   E_lit (L_aux (L_num n, gen_loc l)),
@@ -141,7 +141,7 @@ let rec lexp_is_local_intro (LEXP_aux (lexp, _)) env = match lexp with
   | LEXP_vector_range (lexp,_,_)
   | LEXP_field (lexp,_) -> lexp_is_local_intro lexp env
 
-let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with
+let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match destruct_tannot annot with
   | Some (_, _, eff) -> effectful_effs eff
   | _ -> false
 
@@ -238,18 +238,22 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids =
        Typ_arg_aux (Typ_arg_order ord, l)
   in
 
-  let rewrite_annot = function
-    | (l, Some (env, typ, eff)) -> (l, Some (env, rewrite_typ env typ, eff))
-    | (l, None) -> (l, None)
+  let rewrite_annot (l, tannot) =
+    match destruct_tannot tannot with
+    | Some (env, typ, eff) -> l, replace_typ (rewrite_typ env typ) tannot
+    | None -> l, empty_tannot
   in
 
   let rewrite_def rewriters = function
-    | DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), (l, Some (env, typ, eff)))) ->
+    | DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), (l, tannot))) when not (is_empty_tannot tannot) ->
+       let env = env_of_annot (l, tannot) in
+       let typ = typ_of_annot (l, tannot) in
+       let eff = effect_of_annot tannot in
        let typschm = match typschm with
          | TypSchm_aux (TypSchm_ts (tq, typ), l) ->
             TypSchm_aux (TypSchm_ts (tq, rewrite_typ env typ), l)
        in
-       let a = rewrite_annot (l, Some (env, typ, eff)) in
+       let a = rewrite_annot (l, mk_tannot env typ eff) in
        DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), a))
     | d -> Rewriter.rewrite_def rewriters d
   in
@@ -262,8 +266,11 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids =
 
 let rewrite_bitvector_exps defs =
   let e_aux = function
-    | (E_vector es, ((l, Some (env, typ, eff)) as a)) when is_bitvector_typ typ ->
-       begin
+    | (E_vector es, ((l, tannot) as a)) when not (is_empty_tannot tannot) ->
+       let env = env_of_annot (l, tannot) in
+       let typ = typ_of_annot (l, tannot) in
+       let eff = effect_of_annot tannot in
+       if is_bitvector_typ typ then
          try
            let len = mk_lit_exp (L_num (Big_int.of_int (List.length es))) in
            let es = mk_exp (E_list (List.map strip_exp es)) in
@@ -271,7 +278,8 @@ let rewrite_bitvector_exps defs =
            check_exp env exp typ
          with
          | _ -> E_aux (E_vector es, a)
-       end
+       else
+         E_aux (E_vector es, a)
     | (e_aux, a) -> E_aux (e_aux, a)
   in
   let rewrite_exp _ = fold_exp { id_exp_alg with e_aux = e_aux } in
@@ -285,7 +293,7 @@ let rewrite_bitvector_exps defs =
    variables in scope. *)
 let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
   let extract_typ_var l env nexp (id, (_, typ)) =
-    let var = E_aux (E_id id, (l, Some (env, typ, no_effect))) in
+    let var = E_aux (E_id id, (l, mk_tannot env typ no_effect)) in
     match destruct_atom_nexp env typ with
     | Some size when prove env (nc_eq size nexp) -> Some var
     (* AA: This next case is a bit of a hack... is there a more
@@ -294,12 +302,12 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
        scope. *)
     | Some size when prove env (nc_eq (nsum size (nint 1)) nexp) ->
        let one_exp = infer_exp env (mk_lit_exp (L_num (Big_int.of_int 1))) in
-       Some (E_aux (E_app (mk_id "add_atom", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect))))
+       Some (E_aux (E_app (mk_id "add_atom", [var; one_exp]), (gen_loc l, mk_tannot env (atom_typ (nsum size (nint 1))) no_effect)))
     | _ ->
        begin
          match destruct_vector env typ with
          | Some (len, _, _) when prove env (nc_eq len nexp) ->
-            Some (E_aux (E_app (mk_id "length", [var]), (l, Some (env, atom_typ len, no_effect))))
+            Some (E_aux (E_app (mk_id "length", [var]), (l, mk_tannot env (atom_typ len) no_effect)))
          | _ -> None
        end
   in
@@ -318,12 +326,12 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
     let env = env_of orig_exp in
     match e_aux with
     | E_sizeof (Nexp_aux (Nexp_constant c, _) as nexp) ->
-       E_aux (E_lit (L_aux (L_num c, l)), (l, Some (env, atom_typ nexp, no_effect)))
+       E_aux (E_lit (L_aux (L_num c, l)), (l, mk_tannot env (atom_typ nexp) no_effect))
     | E_sizeof nexp ->
        begin
          match nexp_simp (rewrite_nexp_ids (env_of orig_exp) nexp) with
          | Nexp_aux (Nexp_constant c, _) ->
-            E_aux (E_lit (L_aux (L_num c, l)), (l, Some (env, atom_typ nexp, no_effect)))
+            E_aux (E_lit (L_aux (L_num c, l)), (l, mk_tannot env (atom_typ nexp) no_effect))
          | _ ->
             let locals = Env.get_locals env in
             let exps = Bindings.bindings locals
@@ -428,7 +436,7 @@ let rewrite_sizeof (Defs defs) =
              let uvar = try Some (KBindings.find (orig_kid kid) inst) with Not_found -> None in
              match uvar with
              | Some (U_nexp nexp) ->
-                let sizeof = E_aux (E_sizeof nexp, (l, Some (env, atom_typ nexp, no_effect))) in
+                let sizeof = E_aux (E_sizeof nexp, (l, mk_tannot env (atom_typ nexp) no_effect)) in
                 (try rewrite_trivial_sizeof_exp sizeof with
                 | Type_error (l, err) ->
                   raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err)))
@@ -554,11 +562,11 @@ let rewrite_sizeof (Defs defs) =
              let ptyp' = Typ_aux (Typ_tup (kid_typs @ typs), l) in
              (match pat with
               | P_tup pats ->
-                 P_aux (P_tup (kid_pats @ pats), (l, Some (penv, ptyp', peff)))
-              | P_wild -> P_aux (pat, (l, Some (penv, ptyp', peff)))
+                 P_aux (P_tup (kid_pats @ pats), (l, mk_tannot penv ptyp' peff))
+              | P_wild -> P_aux (pat, (l, mk_tannot penv ptyp' peff))
               | P_typ (Typ_aux (Typ_tup typs, l), pat) ->
                  P_aux (P_typ (Typ_aux (Typ_tup (kid_typs @ typs), l),
-                               rewrite_pat pat), (l, Some (penv, ptyp', peff)))
+                               rewrite_pat pat), (l, mk_tannot penv ptyp' peff))
               | P_as (_, id) | P_id id ->
                  (* adding parameters here would change the type of id;
               we should remove the P_as/P_id here and add a let-binding to the body *)
@@ -569,7 +577,7 @@ let rewrite_sizeof (Defs defs) =
                                                         "unexpected pattern while rewriting function parameters for sizeof expressions"))
           | ptyp ->
              let ptyp' = Typ_aux (Typ_tup (kid_typs @ [ptyp]), l) in
-             P_aux (P_tup (kid_pats @ [paux]), (l, Some (penv, ptyp', peff))) in
+             P_aux (P_tup (kid_pats @ [paux]), (l, mk_tannot penv ptyp' peff)) in
       let pat,guard,exp,pannot = destruct_pexp pexp in
       let pat' = rewrite_pat pat in
       let guard' = match guard with
@@ -907,7 +915,7 @@ let remove_vector_concat_pat pat =
         let typ = Env.base_typ_of env (typ_of_annot annot) in
         let eff = effect_of_annot (snd annot) in
         let (l,_) = annot in
-        let wild _ = P_aux (P_wild,(gen_loc l, Some (env, bit_typ, eff))) in
+        let wild _ = P_aux (P_wild,(gen_loc l, mk_tannot env bit_typ eff)) in
         if is_vector_typ typ then
           match p, vector_typ_args_of typ with
           | P_vector ps,_ -> acc @ ps
@@ -1136,7 +1144,7 @@ let subst_id_pat pat (id1,id2) =
   fold_pat {id_pat_alg with p_id = p_id} pat
 
 let subst_id_exp exp (id1,id2) =
-  Ast_util.subst (Id_aux (id1,Parse_ast.Unknown)) (E_aux (E_id (Id_aux (id2,Parse_ast.Unknown)),(Parse_ast.Unknown,None))) exp
+  Ast_util.subst (Id_aux (id1,Parse_ast.Unknown)) (E_aux (E_id (Id_aux (id2,Parse_ast.Unknown)),(Parse_ast.Unknown,empty_tannot))) exp
 
 let rec pat_to_exp (P_aux (pat,(l,annot))) =
   let rewrap e = E_aux (e,(l,annot)) in
@@ -1370,7 +1378,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
     let rannot = simple_annot l typ in
     let elem = access_bit_exp rootid l typ idx in
     let e = annot_pat (P_id id) l env bit_typ in
-    let letbind = LB_aux (LB_val (e,elem), (l, Some (env, bit_typ, no_effect))) in
+    let letbind = LB_aux (LB_val (e,elem), (l, mk_tannot env bit_typ no_effect)) in
     let letexp = (fun body ->
       let (E_aux (_,(_,bannot))) = body in
       if IdSet.mem id (find_used_vars body)
@@ -1614,7 +1622,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) =
     if (effectful e) then
       let e = rewrite_rec e in
       let (E_aux (_,(el,eannot))) = e in
-      let pat_e' = fresh_id_pat "p__" (el, Some (env_of e, typ_of e, no_effect)) in
+      let pat_e' = fresh_id_pat "p__" (el, mk_tannot (env_of e) (typ_of e) no_effect) in
       let exp_e' = pat_to_exp pat_e' in
       let letbind_e = LB_aux (LB_val (pat_e',e), (el,eannot)) in
       let exp' = case_exp exp_e' (typ_of full_exp) clauses in
@@ -1631,7 +1639,7 @@ let rewrite_fun_guarded_pats rewriters (FD_aux (FD_function (r,t,e,funcls),(l,fd
          (pat,guard,exp,annot) in
        let cs = rewrite_guarded_clauses l (List.map clause funcls) in
        List.map (fun (pat,exp,annot) ->
-         FCL_aux (FCL_Funcl(id,construct_pexp (pat,None,exp,(Parse_ast.Unknown,None))),annot)) cs
+         FCL_aux (FCL_Funcl(id,construct_pexp (pat,None,exp,(Parse_ast.Unknown,empty_tannot))),annot)) cs
      | _ -> funcls (* TODO is the empty list possible here? *) in
    FD_aux (FD_function(r,t,e,funcls),(l,fdannot))
 
@@ -1681,14 +1689,15 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
   | E_block exps ->
     let rec walker exps = match exps with
       | [] -> []
-      | (E_aux(E_assign(le,e), ((l, Some (env,typ,eff)) as annot)) as exp)::exps
-        when lexp_is_local_intro le env && not (lexp_is_effectful le) ->
-        let (le', re') = rewrite_lexp_to_rhs le in
-        let e' = re' (rewrite_base e) in
-        let exps' = walker exps in
-        let effects = union_eff_exps exps' in
-        let block = E_aux (E_block exps', (l, Some (env, unit_typ, effects))) in
-        [fix_eff_exp (E_aux (E_var(le', e', block), annot))]
+      | (E_aux(E_assign(le,e), (l, tannot)) as exp)::exps
+           when not (is_empty_tannot tannot) && lexp_is_local_intro le (env_of_annot (l, tannot)) && not (lexp_is_effectful le) ->
+         let env = env_of_annot (l, tannot) in
+         let (le', re') = rewrite_lexp_to_rhs le in
+         let e' = re' (rewrite_base e) in
+         let exps' = walker exps in
+         let effects = union_eff_exps exps' in
+         let block = E_aux (E_block exps', (l, mk_tannot env unit_typ effects)) in
+         [fix_eff_exp (E_aux (E_var(le', e', block), annot))]
       (*| ((E_aux(E_if(c,t,e),(l,annot))) as exp)::exps ->
         let vars_t = introduced_variables t in
         let vars_e = introduced_variables e in
@@ -1919,7 +1928,7 @@ let rewrite_defs_early_return (Defs defs) =
     let annot = match List.map get_return_pexp pes with
     | Pat_aux (Pat_exp (_, E_aux (_, annot)), _) :: _ -> annot
     | Pat_aux (Pat_when (_, _, E_aux (_, annot)), _) :: _ -> annot
-    | [] -> (Parse_ast.Unknown, None) in
+    | [] -> (Parse_ast.Unknown, empty_tannot) in
     if List.for_all is_return_pexp pes
     then E_return (E_aux (E_case (e, List.map get_return_pexp pes), annot))
     else E_case (e, pes) in
@@ -1945,12 +1954,15 @@ let rewrite_defs_early_return (Defs defs) =
     let full_exp = propagate_exp_effect (E_aux (exp, (l, annot))) in
     let env = env_of full_exp in
     match full_exp with
-    | E_aux (E_return exp, (l, Some (env, typ, eff))) ->
+    | E_aux (E_return exp, (l, tannot)) when not (is_empty_tannot tannot) ->
       (* Add escape effect annotation, since we use the exception mechanism
          of the state monad to implement early return in the Lem backend *)
-      let annot' = Some (env, typ, union_effects eff (mk_effect [BE_escape])) in
-      let exp' = add_e_cast (typ_of exp) exp in
-      E_aux (E_app (mk_id "early_return", [exp']), (l, annot'))
+       let typ = typ_of_annot (l, tannot) in
+       let env = env_of_annot (l, tannot) in
+       let eff = effect_of_annot tannot in
+       let tannot' = mk_tannot env typ (union_effects eff (mk_effect [BE_escape])) in
+       let exp' = add_e_cast (typ_of exp) exp in
+       E_aux (E_app (mk_id "early_return", [exp']), (l, tannot'))
     | _ -> full_exp in
 
   (* Make sure that all final leaves of an expression (e.g. all branches of
@@ -1998,10 +2010,10 @@ let rewrite_defs_early_return (Defs defs) =
           (if is_return exp' then get_return exp' else exp)
       else exp
     in
-    let a = match a with
-    | (l, Some (env, typ, eff)) ->
-      (l, Some (env, typ, union_effects eff (effect_of exp)))
-    | _ -> a in
+    let a = match destruct_tannot (snd a) with
+      | Some (env, typ, eff) ->
+         (fst a, mk_tannot env typ (union_effects eff (effect_of exp)))
+      | _ -> a in
     FCL_aux (FCL_Funcl (id, construct_pexp (pat, guard, exp, pannot)), a) in
 
   let rewrite_fun_early_return rewriters
@@ -2016,14 +2028,14 @@ let rewrite_defs_early_return (Defs defs) =
     { rewriters_base with rewrite_fun = rewrite_fun_early_return }
     (Defs (early_ret_spec @ defs))
 
-let swaptyp typ (l,tannot) = match tannot with
-  | Some (env, typ', eff) -> (l, Some (env, typ, eff))
+let swaptyp typ (l,tannot) = match destruct_tannot tannot with
+  | Some (env, typ', eff) -> (l, mk_tannot env typ eff)
   | _ -> raise (Reporting_basic.err_unreachable l "swaptyp called with empty type annotation")
 
 let is_funcl_rec (FCL_aux (FCL_Funcl (id, pexp), _)) =
   let pat,guard,exp,pannot = destruct_pexp pexp in
   let exp = match guard with None -> exp
-    | Some exp' -> E_aux (E_block [exp';exp],(Parse_ast.Unknown,None)) in
+    | Some exp' -> E_aux (E_block [exp';exp],(Parse_ast.Unknown,empty_tannot)) in
   fst (fold_exp
     { (compute_exp_alg false (||) ) with
       e_app = (fun (f, es) ->
@@ -2126,7 +2138,7 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
       let val_spec =
         VS_aux (VS_val_spec
           (mk_typschm typquant fun_typ, id, (fun _ -> None), false),
-          (Parse_ast.Unknown, None))
+          (Parse_ast.Unknown, empty_tannot))
       in
       let fundef = FD_aux (FD_function (r_o, t_o, e_o, funcls), fdannot) in
       [DEF_spec val_spec; DEF_fundef fundef] @ defs
@@ -2173,13 +2185,17 @@ let rewrite_fix_val_specs (Defs defs) =
 
   let e_aux val_specs (exp, (l, annot)) =
     match fix_eff_exp (E_aux (exp, (l, annot))) with
-    | E_aux (E_app_infix (_, f, _) as exp, (l, Some (env, typ, eff)))
-    | E_aux (E_app (f, _) as exp, (l, Some (env, typ, eff))) ->
+    | E_aux (E_app_infix (_, f, _) as exp, (l, tannot))
+    | E_aux (E_app (f, _) as exp, (l, tannot))
+         when not (is_empty_tannot tannot) ->
+       let env = env_of_annot (l, tannot) in
+       let typ = typ_of_annot (l, tannot) in
+       let eff = effect_of_annot tannot in
        let vs = find_vs env val_specs f in
        (* The (updated) environment is used later by fix_eff_exp to look up
           the actual effects of a function call *)
        let env = Env.update_val_spec f vs env in
-       E_aux (exp, (l, Some (env, typ, union_effects eff (eff_of_vs vs))))
+       E_aux (exp, (l, mk_tannot env typ (union_effects eff (eff_of_vs vs))))
     | e_aux -> e_aux
   in
 
@@ -2567,7 +2583,7 @@ let rewrite_defs_remove_blocks =
 let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
   (* body is a function : E_id variable -> actual body *)
   let (E_aux (_,(l,annot))) = v in
-  match annot with
+  match destruct_tannot annot with
   | Some (env, typ, eff) when is_unit_typ typ ->
      let body = body (annot_exp (E_lit (mk_lit L_unit)) l env unit_typ) in
      let body_typ = try typ_of body with _ -> unit_typ in
@@ -2964,7 +2980,7 @@ let fresh_stringappend_id () =
   id
 
 let unk = Parse_ast.Unknown
-let unkt = (Parse_ast.Unknown, None)
+let unkt = (Parse_ast.Unknown, empty_tannot)
 
 let construct_bool_match env (match_on : tannot exp) (pexp : tannot pexp) : tannot exp =
   let true_exp = annot_exp (E_lit (mk_lit L_true)) unk env bool_typ in
@@ -3384,13 +3400,13 @@ let rewrite_defs_pat_lits rewrite_lit =
          match !guards with
          | [] -> pexp
          | (g :: gs) ->
-            let guard_annot = (fst annot, Some (env_of exp, bool_typ, no_effect)) in
+            let guard_annot = (fst annot, mk_tannot (env_of exp) bool_typ no_effect) in
             Pat_aux (Pat_when (pat, List.fold_left (fun g g' -> E_aux (E_app (mk_id "and_bool", [g; g']), guard_annot)) g gs, exp), annot)
        end
     | Pat_when (pat, guard, exp) ->
        begin
          let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat } pat in
-         let guard_annot = (fst annot, Some (env_of exp, bool_typ, no_effect)) in
+         let guard_annot = (fst annot, mk_tannot (env_of exp) bool_typ no_effect) in
          Pat_aux (Pat_when (pat, List.fold_left (fun g g' -> E_aux (E_app (mk_id "and_bool", [g; g']), guard_annot)) guard !guards, exp), annot)
        end
   in
@@ -3562,7 +3578,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
          let env = env_of_annot annot in
          let typ = typ_of e1 in
          let eff = union_eff_exps [c;e1;e2] in
-         let v = E_aux (E_if (c,e1,e2), (gen_loc el, Some (env, typ, eff))) in
+         let v = E_aux (E_if (c,e1,e2), (gen_loc el, mk_tannot env typ eff)) in
          Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats))
     | E_case (e1,ps) | E_try (e1, ps) ->
        let is_case = match expaux with E_case _ -> true | _ -> false in
@@ -3587,7 +3603,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
          let rewrite_pexp (Pat_aux (pexp, (l, _))) = match pexp with
            | Pat_exp (pat, exp) ->
              let exp = rewrite_var_updates (add_vars overwrite exp vars) in
-             let pannot = (l, Some (env_of exp, typ_of exp, effect_of exp)) in
+             let pannot = (l, mk_tannot (env_of exp) (typ_of exp) (effect_of exp)) in
              Pat_aux (Pat_exp (pat, exp), pannot)
            | Pat_when _ ->
              raise (Reporting_basic.err_unreachable l
@@ -3689,9 +3705,10 @@ let remove_reference_types exp =
     | Typ_arg_aux (Typ_arg_typ t, a) -> Typ_arg_aux (Typ_arg_typ (rewrite_t t), a)
     | _ -> t_arg in
 
-  let rec rewrite_annot = function
-    | (l, None) -> (l, None)
-    | (l, Some (env, typ, eff)) -> (l, Some (env, rewrite_t typ, eff)) in
+  let rec rewrite_annot (l, tannot) =
+    match destruct_tannot tannot with
+    | None -> l, empty_tannot
+    | Some (_, typ, _) -> l, replace_typ (rewrite_t typ) tannot in
 
   map_exp_annot rewrite_annot exp
 
@@ -3715,7 +3732,7 @@ let rewrite_defs_remove_superfluous_letbinds =
          when Id.compare id id' = 0 && small exp1 ->
           let (E_aux (_,e1annot)) = exp1 in
           E_aux (E_internal_return (exp1),e1annot)
-       | _ -> E_aux (exp,annot) 
+       | _ -> E_aux (exp,annot)
        end
     | _ -> E_aux (exp,annot) in
 
@@ -3729,7 +3746,6 @@ let rewrite_defs_remove_superfluous_letbinds =
     ; rewrite_def = rewrite_def
     ; rewrite_defs = rewrite_defs_base
     }
-  
 
 let rewrite_defs_remove_superfluous_returns =
 
@@ -3808,12 +3824,12 @@ let merge_funcls (Defs defs) =
     | (FCL_aux (FCL_Funcl (id,_),(l,_)))::_ ->
        let var = mk_id "merge#var" in
        let l_g = Parse_ast.Generated l in
-       let ann_g : _ * tannot = (l_g,None) in
+       let ann_g : _ * tannot = (l_g,empty_tannot) in
        let clauses = List.map (fun (FCL_aux (FCL_Funcl (_,pexp),_)) -> pexp) fcls in
        FD_aux (FD_function (r,t,e,[
          FCL_aux (FCL_Funcl (id,Pat_aux (Pat_exp (P_aux (P_id var,ann_g),
                                                   E_aux (E_case (E_aux (E_id var,ann_g),clauses),ann_g)),ann_g)),
-                  (l,None))]),ann)
+                  (l,empty_tannot))]),ann)
   in
   let merge_in_def = function
     | DEF_fundef f -> DEF_fundef (merge_function f)
@@ -4261,11 +4277,11 @@ let rewrite_case (e,ann) =
             (fst ann) "Non-exhaustive matching" ("Example: " ^ string_of_rp example) in
 
         let l = Parse_ast.Generated Parse_ast.Unknown in
-        let p = P_aux (P_wild, (l, None)) in
-        let ann' = Some (env, typ_of_annot ann, mk_effect [BE_escape]) in
+        let p = P_aux (P_wild, (l, empty_tannot)) in
+        let ann' = mk_tannot env (typ_of_annot ann) (mk_effect [BE_escape]) in
         (* TODO: use an expression that specifically indicates a failed pattern match *)
-        let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,None))),(l,ann')) in
-        E_aux (E_case (e1,cases@[Pat_aux (Pat_exp (p,b),(l,None))]),ann)
+        let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,empty_tannot))),(l,ann')) in
+        E_aux (E_case (e1,cases@[Pat_aux (Pat_exp (p,b),(l,empty_tannot))]),ann)
      end
   | _ -> E_aux (e,ann)
 
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 9481d6b1..b459610d 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -105,7 +105,8 @@ and free_type_names_t_args consider_var targs =
   nameset_bigunion (List.map (free_type_names_t_arg consider_var) targs)
 
 
-let rec free_type_names_tannot consider_var = function
+let rec free_type_names_tannot consider_var tannot =
+  match Type_check.destruct_tannot tannot with
   | None -> mt
   | Some (_, t, _) -> free_type_names_t consider_var t
 
diff --git a/src/state.ml b/src/state.ml
index 245d450c..70e53a52 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -69,9 +69,9 @@ let find_registers defs =
   List.fold_left
     (fun acc def ->
       match def with
-      | DEF_reg_dec (DEC_aux(DEC_reg (typ, id), annot)) ->
-         let env = match annot with
-           | (_, Some (env, _, _)) -> env
+      | DEF_reg_dec (DEC_aux(DEC_reg (typ, id), (_, tannot))) ->
+         let env = match destruct_tannot tannot with
+           | Some (env, _, _) -> env
            | _ -> Env.empty
          in
          (Env.expand_synonyms env typ, id) :: acc
diff --git a/src/type_check.ml b/src/type_check.ml
index 28e0f930..0c0fc212 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1953,6 +1953,25 @@ let subtype_check env typ1 typ2 =
    of these type annotations. *)
 type tannot = (Env.t * typ * effect) option
 
+let mk_tannot env typ effect = Some (env, typ, effect)
+
+let empty_tannot = None
+let is_empty_tannot = function
+  | None -> true
+  | Some _ -> false
+
+let destruct_tannot tannot = tannot
+
+let string_of_tannot tannot =
+  match destruct_tannot tannot with
+  | Some (_, typ, eff) ->
+     "Some (_, " ^ string_of_typ typ ^ ", " ^ string_of_effect eff ^ ")"
+  | None -> "None"
+
+let replace_typ typ = function
+  | Some (env, _, eff) -> Some (env, typ, eff)
+  | None -> None
+
 let infer_lit env (L_aux (lit_aux, l) as lit) =
   match lit_aux with
   | L_unit -> unit_typ
diff --git a/src/type_check.mli b/src/type_check.mli
index 286c2be9..aa9d6385 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -220,7 +220,23 @@ val dvector_typ : Env.t -> nexp -> typ -> typ
 val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ
 
 (** The type of type annotations *)
-type tannot = (Env.t * typ * effect) option
+type tannot
+
+(** The canonical view of a type annotation is that it is a tuple
+   containing an environment (env), a type (typ), and an effect such
+   that check_X env (strip_X X) typ succeeds, where X is typically exp
+   (i.e an expression). Note that it is specifically not guaranteed
+   that calling destruct_tannot followed by mk_tannot returns an
+   identical type annotation. *)
+val destruct_tannot : tannot -> (Env.t * typ * effect) option
+val mk_tannot : Env.t -> typ -> effect -> tannot
+
+val empty_tannot : tannot
+val is_empty_tannot : tannot -> bool
+
+val destruct_tannot : tannot -> (Env.t * typ * effect) option
+val string_of_tannot : tannot -> string (* For debugging only *)
+val replace_typ : typ -> tannot -> tannot
 
 (** {2 Removing type annotations} *)
 
@@ -270,7 +286,7 @@ val check_case : Env.t -> typ -> unit pexp -> typ -> tannot pexp
 
 val check_fundef : Env.t -> 'a fundef -> tannot def list * Env.t
 
-val check_val_spec : Env.t -> 'a val_spec -> tannot def list * Env.t  
+val check_val_spec : Env.t -> 'a val_spec -> tannot def list * Env.t
 
 val prove : Env.t -> n_constraint -> bool