Add a return exp form to Sail, supported in type checker and in interpreter.

TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem

11 files changed, 205 insertions, 116 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index a539d268..a69be9bf 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -443,6 +443,7 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
     | Parse_ast.E_assign(lexp,exp) -> E_assign(to_ast_lexp k_env def_ord lexp, to_ast_exp k_env def_ord exp)
     | Parse_ast.E_sizeof(nexp) -> E_sizeof(to_ast_nexp k_env nexp)
     | Parse_ast.E_exit exp -> E_exit(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)
     ), (l,NoTyp))
 
diff --git a/src/initial_check_full_ast.ml b/src/initial_check_full_ast.ml
index 19f7cc94..1443af5d 100644
--- a/src/initial_check_full_ast.ml
+++ b/src/initial_check_full_ast.ml
@@ -363,6 +363,7 @@ and to_exp (k_env : kind Envmap.t) (def_ord : Ast.order) (E_aux(exp,(l,_)) :  ex
     | E_assign(lexp,exp) -> E_assign(to_lexp k_env def_ord lexp, to_exp k_env def_ord exp)
     | E_sizeof(nexp) -> E_sizeof(to_nexp k_env nexp)
     | E_exit exp -> E_exit(to_exp k_env def_ord exp)
+    | E_return exp -> E_return(to_exp k_env def_ord exp)
     | E_assert(cond,msg) -> E_assert(to_exp k_env def_ord cond, to_exp k_env def_ord msg)
     | E_comment s -> E_comment s
     | E_comment_struc e -> E_comment_struc e
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 92fa4ec0..a2b496e0 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -250,6 +250,7 @@ type action =
  | Footprint of id * value
  | Nondet of list (exp tannot) * tag
  | Call_extern of string * value
+ | Return of value
  | Exit of (exp tannot)
  (* For the error case of a failed assert, carries up an optional error message*)
  | Fail of value 
@@ -853,6 +854,15 @@ let rec clear_stack_state stack =
     | Thunk_frame e t_level env lmem s -> Thunk_frame e t_level env lmem (clear_stack_state s)
 end
 
+let remove_top_stack_frame stack =
+  match stack with
+  | Top -> Nothing
+  | Hole_frame _ _ _ _ _ Top -> Nothing
+  | Thunk_frame _ _ _ _ Top -> Nothing
+  | Hole_frame _ _ _ _ _ stack -> Just stack
+  | Thunk_frame _ _ _ _ stack -> Just stack
+end
+
 (*functions for converting in progress evaluation back into expression for building current continuation*)
 let rec combine_typs ts =
   match ts with
@@ -1300,12 +1310,16 @@ and vec_concat_match_plev t_level pat r_vals dir l last_pat t =
           | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
             if last_pat
             then 
-              (true,false,(add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length r_vals)) dir r_vals)) eenv),r_vals,[])
+              (true,false,
+               (add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length r_vals)) dir r_vals)) eenv),
+               r_vals,[])
             else (false,false,eenv,[],[]) (*TODO use some constraint bounds here*)
           | _ -> 
             if last_pat
             then 
-              (true,false,(add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length r_vals)) dir r_vals)) eenv),r_vals,[])
+              (true,false,
+               (add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length r_vals)) dir r_vals)) eenv),
+               r_vals,[])
             else (false,false,eenv,[],[]) end)
       | P_wild -> (match t with
           | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
@@ -1550,32 +1564,36 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                                     (to_exp mode env (taint (V_lit diff) (r1 union r2)))
                                   | _ -> Assert_extra.failwith "For loop from and by values not range" end in
                                 let  e = 
-                                  (E_aux (E_block 
-                                            [(E_aux 
-                                                (E_let 
-                                                   (LB_aux (LB_val_implicit (P_aux (P_id id) (fl,val_annot ftyp)) from_e)
-                                                      (Unknown,val_annot ftyp))
-                                                   exp) (l,annot));
-                                             (E_aux (E_for id augment_e to_e by_e order exp) (l,annot))])
-                                            (l,annot)) in
+                                  (E_aux
+                                     (E_block 
+                                        [(E_aux 
+                                            (E_let 
+                                               (LB_aux (LB_val_implicit (P_aux (P_id id) (fl,val_annot ftyp)) from_e)
+                                                  (Unknown,val_annot ftyp))
+                                               exp) (l,annot));
+                                         (E_aux (E_for id augment_e to_e by_e order exp) (l,annot))])
+                                     (l,annot)) in
                                 if mode.eager_eval
                                 then interp_main mode t_level env lm e 
                                 else debug_out Nothing Nothing e t_level lm env
                             | V_unknown -> 
                               let e = 
-                                (E_aux (E_let 
-                                          (LB_aux 
-                                             (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
-                                             (fl, val_annot (val_typ from_val)))
-                                          exp) (l,annot)) in
+                                (E_aux
+                                   (E_let 
+                                      (LB_aux 
+                                         (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
+                                         (fl, val_annot (val_typ from_val)))
+                                      exp) (l,annot)) in
                               interp_main mode t_level env lm e
                             | _ -> (Error l "internal error: by must be a number",lm,le) end)
                         (fun a -> update_stack a 
                           (add_to_top_frame (fun b env -> (E_aux (E_for id from_e to_e b order exp) (l,annot), env))))
                     | V_unknown -> 
                       let e =
-                        (E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
-                                              (fl, val_annot (val_typ from_val))) exp) (l,annot)) in
+                        (E_aux
+                           (E_let (LB_aux
+                                     (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
+                                     (fl, val_annot (val_typ from_val))) exp) (l,annot)) in
                       interp_main mode t_level env lm e
                     | _ -> (Error l "internal error: to must be a number",lm,env) end)
                 (fun a -> update_stack a 
@@ -1583,11 +1601,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                     (E_aux (E_for id from_e t by order exp) (l,annot), env))))
             | V_unknown ->
               let e =
-                (E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_id id) (Unknown, val_annot (val_typ from_val))) from_e)
-                                      (Unknown, val_annot (val_typ from_val))) exp) (l,annot)) in
+                (E_aux
+                   (E_let (LB_aux (LB_val_implicit (P_aux (P_id id) (Unknown, val_annot (val_typ from_val))) from_e)
+                             (Unknown, val_annot (val_typ from_val))) exp) (l,annot)) in
               interp_main mode t_level env lm e
             | _ -> (Error l "internal error: from must be a number",lm,le) end)
-        (fun a -> update_stack a (add_to_top_frame (fun f env -> (E_aux (E_for id f to_ by order exp) (l,annot), env))))
+          (fun a -> update_stack a
+              (add_to_top_frame (fun f env -> (E_aux (E_for id f to_ by order exp) (l,annot), env))))
     | E_case exp pats ->
       resolve_outcome 
         (interp_main mode t_level l_env l_mem exp)
@@ -1974,7 +1994,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                             (Def_val_aux (Def_val_dec ev) dannot))
                      (l,annot), env''))
                 (fun vs -> 
-                  (V_vector_sparse b len dir (map2 (fun i v -> ((natFromInteger i),v)) indexes vs) v)) l_env l_mem [] exps)
+                   (V_vector_sparse b len dir
+                      (map2 (fun i v -> ((natFromInteger i),v)) indexes vs) v)) l_env l_mem [] exps)
             (fun a -> 
               update_stack a 
                 (add_to_top_frame (fun e env -> 
@@ -2015,7 +2036,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                     List.foldr (fun (env,_,exp) (rst,taint_env) -> 
                       let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
                   let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in
-                  interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,(non_det_annot annot maybe_id)))
+                  let exp = E_aux (E_nondet branches) (l,(non_det_annot annot maybe_id)) in
+                  interp_main mode t_level taint_env lm exp
                end)
             | Nothing -> 
               (Error l ("Internal error: function with tag global unfound " ^ name),lm,le) end)
@@ -2169,6 +2191,12 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
         (fun a -> update_stack a (add_to_top_frame (fun lft env -> (E_aux (E_app_infix lft op r) (l,annot), env))))
   | E_exit exp ->
     (Action (Exit exp) (mk_thunk l annot t_level l_env l_mem),l_mem, l_env)
+  | E_return exp ->
+    resolve_outcome
+      (interp_main mode t_level l_env l_mem exp)
+      (fun v lm le ->
+         (Action (Return v) (mk_thunk l annot t_level l_env l_mem), l_mem, l_env))
+      (fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_return e) (l,annot), env)))) 
   | E_assert cond msg ->
     resolve_outcome 
       (interp_main mode t_level l_env l_mem msg)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index a2988ee5..04af1f94 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -331,8 +331,28 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
                | Ivh_decode -> (Ivh_error (Not_an_instruction_error arg), events_out)
                | Ivh_illegal -> (Ivh_error (Not_an_instruction_error arg), events_out)
                | Ivh_unsupported -> (Ivh_error (Unsupported_instruction_error instr), events_out)
-               | Ivh_translate -> Assert_extra.failwith "Reached unreachable pattern" end) end) end)
+               | Ivh_translate -> Assert_extra.failwith "Reached unreachable pattern" end)
+            | _ -> (Ivh_error (Internal_error ("Value not an option for " ^ errk_str)), events_out) end) end)
     | (Interp.Error l msg,_,_) -> (Ivh_error (Internal_error msg), events_out)
+    | (Interp.Action (Interp.Return value) stack,_,_) ->
+      (match Interp.remove_top_stack_frame stack with
+       | Nothing ->
+         if exn_seen
+         then (Ivh_value_after_exn value, events_out)
+         else (match ivh_mode with
+             | Ivh_translate -> (Ivh_value value, events_out)
+             | _ ->
+                          (match value with
+            | Interp.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Ivh_value vinstr,events_out)
+            | Interp.V_ctor (Id_aux (Id "None") _) _ _ _ ->
+              (match ivh_mode with
+               | Ivh_decode -> (Ivh_error (Not_an_instruction_error arg), events_out)
+               | Ivh_illegal -> (Ivh_error (Not_an_instruction_error arg), events_out)
+               | Ivh_unsupported -> (Ivh_error (Unsupported_instruction_error instr), events_out)
+               | Ivh_translate -> Assert_extra.failwith "Reached unreachable pattern" end)
+            | _ -> (Ivh_error (Internal_error ("Value not an option for " ^ errk_str)), events_out)end) end)
+       | Just stack -> interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen
+                                              (fun _ -> Interp.resume mode stack (Just value)) end)
     | (Interp.Action (Interp.Call_extern i value) stack,_,_) ->
       match List.lookup i (Interp_lib.library_functions direction) with
         | Nothing -> (Ivh_error (Internal_error ("External function not available " ^ i)), events_out)
@@ -642,6 +662,11 @@ let rec interp_to_outcome mode context thunk =
                       (Just (fun _ -> (Interp.string_of_value value) ^ "=>" ^ (Interp.string_of_value new_v)))
                       (IState (Interp.add_answer_to_stack next_state new_v) context), lm)
             end)
+         | Interp.Return value ->
+           (match Interp.remove_top_stack_frame next_state with
+            | Nothing -> (Done, lm)
+            | Just stack ->
+              interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode stack (Just value)) end)
          | Interp.Step l Nothing Nothing -> (Internal Nothing Nothing (IState next_state context), lm)
          | Interp.Step l (Just name) Nothing -> (Internal (Just name) Nothing (IState next_state context), lm)
          | Interp.Step l (Just name) (Just value) ->
diff --git a/src/lexer.mll b/src/lexer.mll
index d8f530b6..c2b95004 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -95,6 +95,7 @@ let kw_table =
      ("pure",                    (fun x -> Pure));
      ("rec",			 (fun x -> Rec));
      ("register",		 (fun x -> Register));
+     ("return",                  (fun x -> Return));
      ("scattered",               (fun x -> Scattered));
      ("sizeof",                  (fun x -> Sizeof));
      ("struct",                  (fun x -> Struct));
diff --git a/src/parser.mly b/src/parser.mly
index 6a94219f..7027d7a6 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -134,7 +134,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 
 %token And Alias As Assert Bitzero Bitone Bits By Case Clause Const Dec Def Default Deinfix Effect EFFECT End 
 %token Enumerate Else Exit Extern False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order 
-%token Pure Rec Register Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef 
+%token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef 
 %token Undefined Union With Val
 %token Barr Depend Rreg Wreg Rmem Wmem Wmv Eamem Undef Unspec Nondet Escape
 
@@ -593,6 +593,8 @@ atomic_exp:
     { eloc (E_sizeof($2)) }
   | Exit atomic_exp
       { eloc (E_exit $2) }
+  | Return atomic_exp
+      { eloc (E_return $2) }
   | Assert Lparen exp Comma exp Rparen
       { eloc (E_assert ($3,$5)) }
 
diff --git a/src/pre_lexer.mll b/src/pre_lexer.mll
index 818f8fe6..e6534524 100644
--- a/src/pre_lexer.mll
+++ b/src/pre_lexer.mll
@@ -89,6 +89,7 @@ let kw_table =
      ("pure",                    (fun x -> Other));
      ("rec",			 (fun x -> Other));
      ("register",		 (fun x -> Other));
+     ("return",                  (fun x -> Other));
      ("scattered",               (fun x -> Other));
      ("struct",                  (fun x -> Other));
      ("sizeof",                  (fun x -> Other));
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 4b1ac213..24906734 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -442,6 +442,8 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
       fprintf ppf "@[<0>(E_aux (E_sizeof %a) (%a, %a))@]" pp_lem_nexp nexp pp_lem_l l pp_annot annot
     | E_exit exp ->
       fprintf ppf "@[<0>(E_aux (E_exit %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot
+    | E_return exp ->
+      fprintf ppf "@[<0>(E_aux (E_return %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot
     | E_assert(c,msg) ->
       fprintf ppf "@[<0>(E_aux (E_assert %a %a) (%a, %a))@]" pp_lem_exp c pp_lem_exp msg pp_lem_l l pp_annot annot
     | E_internal_exp ((l, Base((_,t),_,_,_,_,bindings))) ->
@@ -465,10 +467,13 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
         | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given non-vector or implicit"))
     | E_comment _ | E_comment_struc _ ->
       fprintf ppf "@[(E_aux (E_lit (L_aux L_unit %a)) (%a,%a))@]" pp_lem_l l pp_lem_l l pp_annot annot
-    | E_internal_cast ((_, Overload (_,_, _)), _) | E_internal_exp _ ->
-      raise (Reporting_basic.err_unreachable l "Found internal cast or exp with overload")
+    | E_internal_cast _ | E_internal_exp _ ->
+      raise (Reporting_basic.err_unreachable l "Found internal cast or exp")
     | E_internal_exp_user _ -> (raise (Reporting_basic.err_unreachable l "Found non-rewritten internal_exp_user"))
     | E_sizeof_internal _ -> (raise (Reporting_basic.err_unreachable l "Internal sizeof not removed"))
+    | E_internal_let _ -> (raise (Reporting_basic.err_unreachable l "Found non-rewritten internal_let"))
+    | E_internal_return _ -> (raise (Reporting_basic.err_unreachable l "Found non-rewritten internal_return"))
+    | E_internal_plet _ -> raise (Reporting_basic.err_unreachable l "Found non-rewritten internal_plet")
   in
   print_e ppf e
 
@@ -1074,6 +1079,8 @@ let doc_exp, doc_let =
     separate space [string "sizeof"; doc_nexp n]
   | E_exit e ->
     separate space [string "exit"; atomic_exp e;]
+  | E_return e ->
+    separate space [string "return"; atomic_exp e;]
   | E_assert(c,m) ->
     separate space [string "assert"; parens (separate comma [exp c; exp m])]
   (* adding parens and loop for lower precedence *)
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 4e147b36..d3d843f3 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -84,11 +84,14 @@ let fix_effsum_exp (E_aux (e,(l,annot))) =
     | E_list es -> eff_union_exps es
     | E_cons (e1,e2) -> eff_union_exps [e1;e2]
     | E_record fexps -> get_effsum_fexps fexps
+    | E_record_update(e,fexps) -> union_effs ((get_effsum_exp e)::[(get_effsum_fexps fexps)])
     | E_field (e,_) -> get_effsum_exp e
     | E_case (e,pexps) -> union_effs (get_effsum_exp e :: List.map get_effsum_pexp pexps)
     | E_let (lb,e) -> union_effs [get_effsum_lb lb;get_effsum_exp e]
     | E_assign (lexp,e) -> union_effs [get_effsum_lexp lexp;get_effsum_exp e]
     | E_exit e -> get_effsum_exp e
+    | E_return e -> get_effsum_exp e
+    | E_sizeof _ | E_sizeof_internal _ -> pure_e
     | E_assert (c,m) -> pure_e
     | E_comment _ | E_comment_struc _ -> pure_e
     | E_internal_cast (_,e) -> get_effsum_exp e
@@ -330,6 +333,7 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) =
   | E_assign (lexp,exp) -> rewrap (E_assign(rewriters.rewrite_lexp rewriters nmap lexp,rewrite exp))
   | E_sizeof n -> rewrap (E_sizeof n)
   | E_exit e -> rewrap (E_exit (rewrite e))
+  | E_return e -> rewrap (E_return (rewrite e))
   | E_assert(e1,e2) -> rewrap (E_assert(rewrite e1,rewrite e2))
   | E_internal_cast ((l,casted_annot),exp) -> 
     let new_exp = rewrite exp in
@@ -604,6 +608,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
   ; e_let                    : 'letbind * 'exp -> 'exp_aux
   ; e_assign                 : 'lexp * 'exp -> 'exp_aux
   ; e_exit                   : 'exp -> 'exp_aux
+  ; e_return                 : 'exp -> 'exp_aux
   ; e_assert                 : 'exp * 'exp -> 'exp_aux
   ; e_internal_cast          : 'a annot * 'exp -> 'exp_aux
   ; e_internal_exp           : 'a annot -> 'exp_aux
@@ -666,6 +671,7 @@ let rec fold_exp_aux alg = function
   | E_let (letbind,e) -> alg.e_let (fold_letbind alg letbind, fold_exp alg e)
   | E_assign (lexp,e) -> alg.e_assign (fold_lexp alg lexp, fold_exp alg e)
   | E_exit e -> alg.e_exit (fold_exp alg e)
+  | E_return e -> alg.e_return (fold_exp alg e)
   | E_assert(e1,e2) -> alg.e_assert (fold_exp alg e1, fold_exp alg e2)
   | E_internal_cast (annot,e) -> alg.e_internal_cast (annot, fold_exp alg e)
   | E_internal_exp annot -> alg.e_internal_exp annot
@@ -729,6 +735,7 @@ let id_exp_alg =
   ; e_let = (fun (lb,e2) -> E_let (lb,e2))
   ; e_assign = (fun (lexp,e2) -> E_assign (lexp,e2))
   ; e_exit = (fun e1 -> E_exit (e1))
+  ; e_return = (fun e1 -> E_return e1)
   ; e_assert = (fun (e1,e2) -> E_assert(e1,e2)) 
   ; e_internal_cast = (fun (a,e1) -> E_internal_cast (a,e1))
   ; e_internal_exp = (fun a -> E_internal_exp a)
@@ -1578,6 +1585,7 @@ let find_updated_vars exp =
       ; e_let = (fun (lb,e2) -> lb @@ e2)
       ; e_assign = (fun ((ids,acc),e2) -> ([],ids) @@ acc @@ e2)
       ; e_exit = (fun e1 -> ([],[]))
+      ; e_return = (fun e1 -> e1)
       ; e_assert = (fun (e1,e2) -> ([],[]))
       ; e_internal_cast = (fun (_,e1) -> e1)
       ; e_internal_exp = (fun _ -> ([],[]))
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 3bfb766c..ab4645f3 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -73,6 +73,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
  ; e_let                    : 'letbind * 'exp -> 'exp_aux
  ; e_assign                 : 'lexp * 'exp -> 'exp_aux
  ; e_exit                   : 'exp -> 'exp_aux
+ ; e_return                 : 'exp -> 'exp_aux
  ; e_assert                 : 'exp * 'exp -> 'exp_aux
  ; e_internal_cast          : 'a annot * 'exp -> 'exp_aux
  ; e_internal_exp           : 'a annot -> 'exp_aux
diff --git a/src/type_check.ml b/src/type_check.ml
index 1b320d5d..4c7fb8e0 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -477,20 +477,24 @@ let simp_exp e l t = E_aux(e,(l,simple_annot t))
   This is relevent largely for vector accesses and sub ranges, 
   where if there's a constant we really want to look at that constant,
   and if there's a known vector base, we want to use that directly, vs assignments or branching values *)
-let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(e,(l,annot)):tannot exp)
+let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool)
+    (ret_t:t) (expect_t:t) (E_aux(e,(l,annot)):tannot exp)
   : (tannot exp * t * tannot emap * nexp_range list * bounds_env * effect) =
   let Env(d_env,t_env,b_env,tp_env) = envs in
   let expect_t,_ = get_abbrev d_env expect_t in
+  let ret_t,_ = get_abbrev d_env ret_t in
   let rebuild annot = E_aux(e,(l,annot)) in
   match e with
     | E_block exps -> 
-      let (exps',annot',sc,t,ef) = check_block envs imp_param expect_t exps in
+      let (exps',annot',sc,t,ef) = check_block envs imp_param ret_t expect_t exps in
       (E_aux(E_block(exps'),(l,annot')),t,Envmap.empty,sc,nob,ef)
     | E_nondet exps ->
       let base_ef = add_effect (BE_aux(BE_nondet,l)) pure_e in
       let (ces, sc, ef)  = 
-        List.fold_right (fun e (es,sc,ef) -> let (e,_,_,sc',_,ef') = (check_exp envs imp_param true unit_t e) in
-                          (e::es,sc@sc',union_effects ef ef')) exps ([],[],base_ef) in
+        List.fold_right
+          (fun e (es,sc,ef) ->
+             let (e,_,_,sc',_,ef') = (check_exp envs imp_param true true ret_t unit_t e) in
+             (e::es,sc@sc',union_effects ef ef')) exps ([],[],base_ef) in
       let _,_ = type_consistent (Expr l) d_env Require false unit_t expect_t in
       (E_aux (E_nondet ces,(l,cons_efs_annot unit_t sc base_ef ef)),unit_t,t_env,sc,nob,ef)
     | E_id id -> 
@@ -536,7 +540,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
                         ("Identifier " ^ (id_to_string id) ^ " is bound to a function and cannot be used as a value")
          | Tapp("register",[TA_typ(t')]),Tapp("register",[TA_typ(expect_t')]) -> 
            let tannot = Base(([],t),(match tag with | External _ -> Emp_global | _ -> tag),cs,pure_e,pure_e,bounds) in
-           let t',cs' = type_consistent (Expr l) d_env Require widen t' expect_t' in
+           let t',cs' = type_consistent (Expr l) d_env Require widen_vec t' expect_t' in
            (rebuild tannot,t,t_env,cs@cs',bounds,ef)
          | Tapp("register",[TA_typ(t')]),Tuvar _ ->
            (*let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
@@ -544,19 +548,22 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
            let tannot = Base(([],t),
                              (if is_alias then tag else (if tag = Emp_local then tag else Emp_global)),
                              cs,pure_e,pure_e,bounds) in
-           let _,cs',ef',e' = type_coerce (Expr l) d_env Require false widen b_env t' (rebuild tannot) expect_actual in
+           let _,cs',ef',e' =
+             type_coerce (Expr l) d_env Require false widen_vec b_env t' (rebuild tannot) expect_actual in
            (e',t,t_env,cs@cs',bounds,ef')
          | Tapp("register",[TA_typ(t')]),_ ->
            let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
            let tannot = Base(([],t),(if is_alias then tag else External (Some i)),cs,ef',ef',bounds) in
-           let t',cs',_,e' = type_coerce (Expr l) d_env Require false widen b_env t' (rebuild tannot) expect_actual in
+           let t',cs',_,e' =
+             type_coerce (Expr l) d_env Require false widen_vec b_env t' (rebuild tannot) expect_actual in
            (e',t',t_env,cs@cs',bounds,ef')
          | Tapp("reg",[TA_typ(t')]),_ ->
            let tannot = cons_bs_annot t cs bounds in
-           let t',cs',_,e' = type_coerce (Expr l) d_env Require false widen b_env t' (rebuild tannot) expect_actual in
+           let t',cs',_,e' =
+             type_coerce (Expr l) d_env Require false widen_num b_env t' (rebuild tannot) expect_actual in
            (e',t',t_env,cs@cs',bounds,pure_e)
         | _ -> 
-          let t',cs',ef',e' = type_coerce (Expr l) d_env Require false widen b_env
+          let t',cs',ef',e' = type_coerce (Expr l) d_env Require false widen_num b_env
               t (rebuild (Base(([],t),tag,cs,pure_e,ef,bounds))) expect_t in
           (e',t',t_env,cs@cs',bounds,union_effects ef ef')
         )
@@ -629,14 +636,14 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
               E_aux(E_app((Id_aux((Id f),l)),
                           [(E_aux (E_internal_exp(internal_tannot), tannot));]),tannot),[],ef
             | _ -> simp_exp e l (new_t ()),[],ef)) in
-      let t',cs',_,e' = type_coerce (Expr l) d_env Require false widen b_env (get_e_typ e) e expect_t in
+      let t',cs',_,e' = type_coerce (Expr l) d_env Require false widen_num b_env (get_e_typ e) e expect_t in
       (e',t',t_env,cs@cs',nob,effect)
     | E_cast(typ,e) ->
       let cast_t = typ_to_t envs false false typ in
       let cast_t,cs_a = get_abbrev d_env cast_t in
       let cast_t = typ_subst tp_env false cast_t in
       let ct = {t = Toptions(cast_t,None)} in
-      let (e',u,t_env,cs,bounds,ef) = check_exp envs imp_param true ct e in
+      let (e',u,t_env,cs,bounds,ef) = check_exp envs imp_param true true ret_t ct e in
       (*let _ = Printf.eprintf "Type checking cast: cast_t is %s constraints after checking e are %s\n" 
         (t_to_string cast_t) (constraints_to_string cs) in*)
       let t',cs2,ef',e' = type_coerce (Expr l) d_env Require true true b_env u e' cast_t in
@@ -651,10 +658,10 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
       let check_parms p_typ parms = (match parms with
         | [] | [(E_aux (E_lit (L_aux (L_unit,_)),_))] 
           -> let (_,cs') = type_consistent (Expr l) d_env Require false unit_t p_typ in [],unit_t,cs',pure_e 
-        | [parm] -> let (parm',arg_t,t_env,cs',_,ef_p) = check_exp envs imp_param true p_typ parm
+        | [parm] -> let (parm',arg_t,t_env,cs',_,ef_p) = check_exp envs imp_param true true ret_t p_typ parm
           in [parm'],arg_t,cs',ef_p
         | parms -> 
-          (match check_exp envs imp_param true p_typ (E_aux (E_tuple parms,(l,NoTyp))) with
+          (match check_exp envs imp_param true true ret_t p_typ (E_aux (E_tuple parms,(l,NoTyp))) with
           | ((E_aux(E_tuple parms',tannot')),arg_t,t_env,cs',_,ef_p) -> parms',arg_t,cs',ef_p
           | _ ->
             raise (Reporting_basic.err_unreachable l
@@ -769,7 +776,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
     | E_app_infix(lft,op,rht) -> 
       let i = id_to_string op in
       let check_parms arg_t lft rht =
-        match check_exp envs imp_param true arg_t (E_aux(E_tuple [lft;rht],(l,NoTyp))) with
+        match check_exp envs imp_param true true ret_t arg_t (E_aux(E_tuple [lft;rht],(l,NoTyp))) with
         | ((E_aux(E_tuple [lft';rht'],_)),arg_t,_,cs',_,ef') -> (lft',rht',arg_t,cs',ef')
         | _ -> 
           raise (Reporting_basic.err_unreachable l "check exp given tuple and tuple type and returned non-tuple") 
@@ -854,7 +861,8 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
             List.fold_right2 
               (fun e t (exps,typs,consts,effect) -> 
                  let (e',t',_,c,_,ef) =
-                   check_exp envs imp_param true t e in ((e'::exps),(t'::typs),c@consts,union_effects ef effect))
+                   check_exp envs imp_param true true ret_t t e in
+                 ((e'::exps),(t'::typs),c@consts,union_effects ef effect))
               exps ts ([],[],[],pure_e) in
           let t = {t = Ttup typs} in
           (E_aux(E_tuple(exps),(l,simple_annot_efr t effect)),t,t_env,consts,nob,effect)
@@ -864,7 +872,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
         let exps,typs,consts,effect = 
           List.fold_right 
             (fun e (exps,typs,consts,effect) -> 
-              let (e',t,_,c,_,ef) = check_exp envs imp_param true (new_t ()) e in
+              let (e',t,_,c,_,ef) = check_exp envs imp_param true true ret_t (new_t ()) e in
               ((e'::exps),(t::typs),c@consts,union_effects ef effect))
             exps ([],[],[],pure_e) in
         let t = { t=Ttup typs } in
@@ -873,12 +881,12 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
             t (E_aux(E_tuple(exps),(l,simple_annot_efr t effect))) expect_t in
         (e',t',t_env,consts@cs',nob,union_effects ef' effect))
     | E_if(cond,then_,else_) ->
-      let (cond',_,_,c1,_,ef1) = check_exp envs imp_param true bit_t cond in
+      let (cond',_,_,c1,_,ef1) = check_exp envs imp_param true true ret_t bit_t cond in
       let (c1,c1p,c1n) = split_conditional_constraints c1 in
       (match expect_t.t with
       | Tuvar _ -> 
-        let then',then_t,then_env,then_c,then_bs,then_ef = check_exp envs imp_param true (new_t ()) then_ in
-        let else',else_t,else_env,else_c,else_bs,else_ef = check_exp envs imp_param true (new_t ()) else_ in
+        let then',then_t,then_env,then_c,then_bs,then_ef = check_exp envs imp_param true true ret_t (new_t ()) then_ in
+        let else',else_t,else_env,else_c,else_bs,else_ef = check_exp envs imp_param true true ret_t (new_t ()) else_ in
         (*TOTHINK Possibly I should first consistency check else and then, with Guarantee,
           then check against expect_t with Require*)
         let then_t',then_c' = type_consistent (Expr l) d_env Require true then_t expect_t in
@@ -893,8 +901,8 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
          merge_bounds then_bs else_bs, (*TODO Should be an intersecting merge*)
          sub_effects)
       | _ ->
-        let then',then_t,then_env,then_c,then_bs,then_ef = check_exp envs imp_param true expect_t then_ in
-        let else',else_t,else_env,else_c,else_bs,else_ef = check_exp envs imp_param true expect_t else_ in
+        let then',then_t,then_env,then_c,then_bs,then_ef = check_exp envs imp_param true true ret_t expect_t then_ in
+        let else',else_t,else_env,else_c,else_bs,else_ef = check_exp envs imp_param true true ret_t expect_t else_ in
         let t_cs = CondCons((Expr l),Positive,None,c1,then_c) in
         let e_cs = CondCons((Expr l),Negative,None,[],else_c) in
         let sub_effects = union_effects ef1 (union_effects then_ef else_ef) in
@@ -908,9 +916,9 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
         without coercion as these nu variables are likely floating*)
       let f,t,s = new_n(),new_n(),new_n() in
       let ft,tt,st = mk_atom f, mk_atom t, mk_atom s in
-      let from',from_t,_,from_c,_,from_ef = check_exp envs imp_param false ft from in
-      let to_',to_t,_,to_c,_,to_ef = check_exp envs imp_param false tt to_ in
-      let step',step_t,_,step_c,_,step_ef = check_exp envs imp_param false st step in
+      let from',from_t,_,from_c,_,from_ef = check_exp envs imp_param false false ret_t ft from in
+      let to_',to_t,_,to_c,_,to_ef = check_exp envs imp_param false false ret_t tt to_ in
+      let step',step_t,_,step_c,_,step_ef = check_exp envs imp_param false false ret_t st step in
       let new_annot,local_cs = 
         match (aorder_to_ord order).order with
           | Oinc ->
@@ -922,7 +930,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
       (*TODO Might want to extend bounds here for the introduced variable*)
       let (block',b_t,_,b_c,_,b_ef)=
         check_exp (Env(d_env,Envmap.insert t_env (id_to_string id,new_annot),b_env,tp_env))
-          imp_param true expect_t block
+          imp_param true true ret_t expect_t block
       in
       let sub_effects = union_effects b_ef (union_effects step_ef (union_effects to_ef from_ef)) in
       (E_aux(E_for(id,from',to_',step',order,block'),(l,constrained_annot_efr b_t local_cs sub_effects)),expect_t,
@@ -934,7 +942,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
         | _ -> new_t (),d_env.default_o in
       let es,cs,effect,item_t = (List.fold_right 
                             (fun (e,t,_,c,_,ef) (es,cs,effect,_) -> (e::es),(c@cs),union_effects ef effect,t)
-                            (List.map (check_exp envs imp_param true item_t) es) ([],[],pure_e,item_t)) in
+                            (List.map (check_exp envs imp_param true true ret_t item_t) es) ([],[],pure_e,item_t)) in
       let len = List.length es in
       let t = match ord.order,d_env.default_o.order with
         | (Oinc,_) | (Ouvar _,Oinc) | (Ovar _,Oinc) -> 
@@ -966,7 +974,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
               else if i = prev
               then (typ_error l ("Indexed vector contains a duplicate definition of index " ^ (string_of_int i)))
               else (typ_error l ("Indexed vector is not consistently " ^ (if is_inc then "increasing" else "decreasing"))))
-           (List.map (fun (i,e) -> let (e,_,_,cs,_,eft) = (check_exp envs imp_param true item_t e) in ((i,e),cs,eft))
+           (List.map (fun (i,e) -> let (e,_,_,cs,_,eft) = (check_exp envs imp_param true true ret_t item_t e) in ((i,e),cs,eft))
               eis) ([],[],pure_e,false,(if is_inc then (last+1) else (last-1)))) in
       let (default',fully_enumerate,cs_d,ef_d) = match (default,contains_skip) with
         | (Def_val_empty,false) -> (Def_val_aux(Def_val_empty,(ld,simple_annot item_t)),true,[],pure_e)
@@ -974,7 +982,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
           let ef = add_effect (BE_aux(BE_unspec,l)) pure_e in
           let de = E_aux(E_lit (L_aux(L_undef,l)), (l,simple_annot item_t)) in
           (Def_val_aux(Def_val_dec de, (l, cons_efs_annot item_t [] ef ef)),false,[],ef)
-        | (Def_val_dec e,_) -> let (de,t,_,cs_d,_,ef_d) = (check_exp envs imp_param true item_t e) in
+        | (Def_val_dec e,_) -> let (de,t,_,cs_d,_,ef_d) = (check_exp envs imp_param true true ret_t item_t e) in
           (*Check that ef_d doesn't write to memory or registers? *)
           (Def_val_aux(Def_val_dec de,(ld,cons_efs_annot item_t cs_d pure_e ef_d)),false,cs_d,ef_d) in
       let (base_bound,length_bound,cs_bounds) = 
@@ -995,9 +1003,9 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
       let item_t = new_t () in
       let index = new_n () in
       let vt = {t= Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord ord; TA_typ item_t])} in
-      let (vec',t',cs,ef),va_lef,tag = recheck_for_register envs imp_param false vt vec in
+      let (vec',t',cs,ef),va_lef,tag = recheck_for_register envs imp_param false false ret_t vt vec in
       let it = mk_atom index in
-      let (i',ti',_,cs_i,_,ef_i) = check_exp envs imp_param false it i in
+      let (i',ti',_,cs_i,_,ef_i) = check_exp envs imp_param false false ret_t it i in
       let ord,item_t = match t'.t with
         | Tabbrev(_,{t=Tapp("vector",[_;_;TA_ord ord;TA_typ t])}) | Tapp("vector",[_;_;TA_ord ord;TA_typ t])
         | Tabbrev(_,{t=Tapp("register",[TA_typ{t=Tapp ("vector",[_;_;TA_ord ord;TA_typ t])}])})
@@ -1033,11 +1041,11 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
         | Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord_n; TA_typ item_t]) -> item_t
         | _ -> new_t() in
       let vt = {t=Tapp("vector",[TA_nexp base;TA_nexp length;TA_ord ord;TA_typ item_t])} in
-      let (vec',vt',cs,ef),v_efs,tag = recheck_for_register envs imp_param false vt vec in      
+      let (vec',vt',cs,ef),v_efs,tag = recheck_for_register envs imp_param false false ret_t vt vec in      
       let i1t = {t=Tapp("atom",[TA_nexp n1_start])} in
-      let (i1', ti1, _,cs_i1,_,ef_i1) = check_exp envs imp_param false i1t i1 in
+      let (i1', ti1, _,cs_i1,_,ef_i1) = check_exp envs imp_param false false ret_t i1t i1 in
       let i2t = {t=Tapp("atom",[TA_nexp n2_end])} in
-      let (i2', ti2, _,cs_i2,_,ef_i2) = check_exp envs imp_param false i2t i2 in
+      let (i2', ti2, _,cs_i2,_,ef_i2) = check_exp envs imp_param false false ret_t i2t i2 in
       let cs_loc =
         match (ord.order,d_env.default_o.order) with
           | (Oinc,_) -> 
@@ -1074,10 +1082,10 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
         | Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord_n; TA_typ item_t]) -> item_t
         | _ -> new_t() in
       let vt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ item_t])} in
-      let (vec',t',_,cs,_,ef) = check_exp envs imp_param true vt vec in
+      let (vec',t',_,cs,_,ef) = check_exp envs imp_param true true ret_t vt vec in
       let it = {t=Tapp("range",[TA_nexp min;TA_nexp m_rise])} in
-      let (i', ti, _,cs_i,_,ef_i) = check_exp envs imp_param false it i in
-      let (e', te, _,cs_e,_,ef_e) = check_exp envs imp_param true item_t e in
+      let (i', ti, _,cs_i,_,ef_i) = check_exp envs imp_param false false ret_t it i in
+      let (e', te, _,cs_e,_,ef_e) = check_exp envs imp_param true true ret_t item_t e in
       let cs_loc = 
         match (ord.order,d_env.default_o.order) with
           | (Oinc,_) ->
@@ -1104,17 +1112,17 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
         | Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord_n; TA_typ item_t]) -> item_t
         | _ -> new_t() in
       let vt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ item_t])} in
-      let (vec',t',_,cs,_,ef) = check_exp envs imp_param true vt vec in
+      let (vec',t',_,cs,_,ef) = check_exp envs imp_param true true ret_t vt vec in
       let i1t = {t=Tapp("range",[TA_nexp min1;TA_nexp m_rise1])} in
-      let (i1', ti1, _,cs_i1,_,ef_i1) = check_exp envs imp_param false i1t i1 in
+      let (i1', ti1, _,cs_i1,_,ef_i1) = check_exp envs imp_param false false ret_t i1t i1 in
       let i2t = {t=Tapp("range",[TA_nexp min2;TA_nexp m_rise2])} in
-      let (i2', ti2, _,cs_i2,_,ef_i2) = check_exp envs imp_param false i2t i2 in
+      let (i2', ti2, _,cs_i2,_,ef_i2) = check_exp envs imp_param false false ret_t i2t i2 in
       let (e',item_t',_,cs_e,_,ef_e) =
-        try check_exp envs imp_param true item_t e with
+        try check_exp envs imp_param true true ret_t item_t e with
           | _ ->
             let (base_e,rise_e) = new_n(),new_n() in
             let (e',ti',env_e,cs_e,bs_e,ef_e) = 
-              check_exp envs imp_param true
+              check_exp envs imp_param true true ret_t
                 {t=Tapp("vector",[TA_nexp base_e;TA_nexp rise_e;TA_ord ord;TA_typ item_t])} e 
             in
             let cs_add = [Eq((Expr l),base_e,min1);LtEq((Expr l),Guarantee,rise,m_rise2)] in
@@ -1151,9 +1159,9 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
       let base1,rise1 = new_n(), new_n() in
       let base2,rise2 = new_n(),new_n() in
       let (v1',t1',_,cs_1,_,ef_1) = 
-        check_exp envs imp_param true {t=Tapp("vector",[TA_nexp base1;TA_nexp rise1;TA_ord ord;TA_typ item_t])} v1 in
+        check_exp envs imp_param true true ret_t {t=Tapp("vector",[TA_nexp base1;TA_nexp rise1;TA_ord ord;TA_typ item_t])} v1 in
       let (v2',t2',_,cs_2,_,ef_2) = 
-        check_exp envs imp_param true {t=Tapp("vector",[TA_nexp base2;TA_nexp rise2;TA_ord ord;TA_typ item_t])} v2 in
+        check_exp envs imp_param true true ret_t {t=Tapp("vector",[TA_nexp base2;TA_nexp rise2;TA_ord ord;TA_typ item_t])} v2 in
       let result_rise = mk_add rise1 rise2 in
       let result_base = match ord.order with
         | Odec -> mk_sub result_rise n_one
@@ -1170,7 +1178,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
         | _ -> new_t() in
       let es,cs,effect,item_t = 
         (List.fold_left (fun (es,cs,effect,_) (e,t,_,c,_,ef) -> (e::es),(c@cs),union_effects ef effect,t) 
-           ([],[],pure_e,item_t) (List.map (check_exp envs imp_param true item_t) es) ) in
+           ([],[],pure_e,item_t) (List.map (check_exp envs imp_param true true ret_t item_t) es) ) in
       let t = {t = Tapp("list",[TA_typ item_t])} in
       let t',cs',ef',e' = type_coerce (Expr l) d_env Require false false b_env t 
         (E_aux(E_list es,(l,simple_annot_efr t effect))) expect_t in
@@ -1180,8 +1188,8 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
         | Tapp("list",[TA_typ i]) -> i
         | _ -> new_t() in
       let lt = {t=Tapp("list",[TA_typ item_t])} in
-      let (ls',t',_,cs,_,ef) = check_exp envs imp_param true lt ls in
-      let (i', ti, _,cs_i,_,ef_i) = check_exp envs imp_param true item_t i in
+      let (ls',t',_,cs,_,ef) = check_exp envs imp_param true true ret_t lt ls in
+      let (i', ti, _,cs_i,_,ef_i) = check_exp envs imp_param true true ret_t item_t i in
       let sub_effects = union_effects ef ef_i in
       let (t',cs',ef',e') = 
         type_coerce (Expr l) d_env Require false false b_env lt
@@ -1198,7 +1206,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
               typ_error l ("Expected a struct of type " ^ n ^ ", which should not have a field " ^ i)
             | Some(ft) ->
               let ft = typ_subst subst_env false ft in
-              let (e,t',_,c,_,ef) = check_exp envs imp_param true ft exp in
+              let (e,t',_,c,_,ef) = check_exp envs imp_param true true ret_t ft exp in
               (FE_aux(FE_Fexp(id,e),(l,Base(([],t'),tag,c,ef,ef,bounds)))::fexps,cons@c,union_effects ef ef')) in  
       (match u_actual.t with
         | Tid(n) | Tapp(n,_)->
@@ -1227,7 +1235,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
             | _ -> typ_error l "No struct type matches the set of fields given")
         | _ -> typ_error l ("Expected an expression of type " ^ t_to_string expect_t ^ " but found a struct"))
     | E_record_update(exp,FES_aux(FES_Fexps(fexps,_),l')) -> 
-      let (e',t',_,c,_,ef) = check_exp envs imp_param true expect_t exp in
+      let (e',t',_,c,_,ef) = check_exp envs imp_param true true ret_t expect_t exp in
       let field_walker r subst_env bounds tag i =
         (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) (fexps,cons,ef') ->
            let fi = id_to_string id in
@@ -1235,7 +1243,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
            | None -> typ_error l ("Expected a struct with type " ^ i ^ ", which does not have a field " ^ fi)
            | Some ft ->
              let ft = typ_subst subst_env false ft in
-             let (e,t',_,c,_,ef) = check_exp envs imp_param true ft exp in
+             let (e,t',_,c,_,ef) = check_exp envs imp_param true true ret_t ft exp in
              (FE_aux(FE_Fexp(id,e),(l,Base(([],t'),tag,c,pure_e,ef,bounds)))::fexps,cons@c,union_effects ef ef')) in
       (match t'.t with
         | Tid i | Tabbrev(_, {t=Tid i}) | Tapp(i,_) ->
@@ -1267,7 +1275,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
             | records -> typ_error l "Multiple structs contain this set of fields, try adding a cast to disambiguate")
         | _ -> typ_error l ("Expected a struct to update but found an expression of type " ^ t_to_string expect_t))
     | E_field(exp,id) ->
-      let (e',t',env_sub,c_sub,bounds,ef_sub) = check_exp envs imp_param true (new_t()) exp in
+      let (e',t',env_sub,c_sub,bounds,ef_sub) = check_exp envs imp_param true true ret_t (new_t()) exp in
       let fi = id_to_string id in
       (match t'.t with
       | Tabbrev({t=Tid i}, _) | Tabbrev({t=Tapp(i,_)},_) | Tid i | Tapp(i,_) ->
@@ -1282,7 +1290,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
                   let (e',t',_,c_sub,_,ef_sub),ef_update =
                     match rec_kind with
                       | Register ->
-                        (check_exp envs imp_param true (into_register_typ t') exp,
+                        (check_exp envs imp_param true true ret_t (into_register_typ t') exp,
                          add_effect (BE_aux(BE_rreg, l)) pure_e)
                       | Record -> ((e',t',env_sub,c_sub,bounds,ef_sub), pure_e) in
                   let (et',c',ef',acc) = 
@@ -1309,7 +1317,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
               let (e',t',_,c_sub,_,ef_sub),ef_update =
                 match rec_kind with
                   | Register ->
-                    (check_exp envs imp_param true (into_register_typ t') exp, add_effect (BE_aux(BE_rreg, l)) pure_e)
+                    (check_exp envs imp_param true true ret_t (into_register_typ t') exp, add_effect (BE_aux(BE_rreg, l)) pure_e)
                   | Record -> ((e',t',env_sub,c_sub,bounds,ef_sub), pure_e) in
               let (et',c',ef',acc) = 
                 type_coerce (Expr l) d_env Require false false b_env ft 
@@ -1321,7 +1329,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
            typ_error l ("Multiple structs or registers contain field " ^ fi ^ ", try adding a cast to disambiguate"))
       | _ -> typ_error l ("Expected a struct or register for access but found an expression of type " ^ t_to_string t'))
     | E_case(exp,pexps) ->
-      let (e',t',_,cs,_,ef) = check_exp envs imp_param true (new_t()) exp in
+      let (e',t',_,cs,_,ef) = check_exp envs imp_param true true ret_t (new_t()) exp in
       (*let _ = Printf.eprintf "Type of pattern after expression check %s\n" (t_to_string t') in*)
       let t' = 
         match t'.t with
@@ -1329,32 +1337,34 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
           | _ -> t' in
       (*let _ = Printf.eprintf "Type of pattern after register check %s\n" (t_to_string t') in*)
       let (pexps',t,cs',ef') = 
-        check_cases envs imp_param t' expect_t (if (List.length pexps) = 1 then Solo else Switch) pexps in
+        check_cases envs imp_param ret_t t' expect_t (if (List.length pexps) = 1 then Solo else Switch) pexps in
       let effects = union_effects ef ef' in
       (E_aux(E_case(e',pexps'),(l,simple_annot_efr t effects)),t,t_env,cs@[BranchCons(Expr l, None, cs')],nob,effects)
     | E_let(lbind,body) -> 
-      let (lb',t_env',cs,b_env',ef) = (check_lbind envs imp_param false Emp_local lbind) in
+      let (lb',t_env',cs,b_env',ef) = (check_lbind envs imp_param false (Some ret_t) Emp_local lbind) in
       let new_env = 
         (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env false)
                t_env t_env', merge_bounds b_env' b_env,tp_env)) 
       in
-      let (e,t,_,cs',_,ef') = check_exp new_env imp_param true expect_t body in
+      let (e,t,_,cs',_,ef') = check_exp new_env imp_param true true ret_t expect_t body in
       let effects = union_effects ef ef' in
       (E_aux(E_let(lb',e),(l,simple_annot_efr t effects)),t,t_env,cs@cs',nob,effects)
     | E_assign(lexp,exp) ->
-      let (lexp',t',_,t_env',tag,cs,b_env',efl,efr) = check_lexp envs imp_param true lexp in
+      let (lexp',t',_,t_env',tag,cs,b_env',efl,efr) = check_lexp envs imp_param ret_t true lexp in
       let t' = match t'.t with | Tapp("reg",[TA_typ t]) | Tapp("register",[TA_typ t])
                                | Tabbrev(_,{t=Tapp("register",[TA_typ t])}) -> t
                                | _ -> t' in
-      let (exp',t'',_,cs',_,efr') = check_exp envs imp_param true t' exp in
+      let (exp',t'',_,cs',_,efr') = check_exp envs imp_param true true ret_t t' exp in
       let (t',c') = type_consistent (Expr l) d_env Require false unit_t expect_t in
       let effects = union_effects efl (union_effects efr efr') in
       (E_aux(E_assign(lexp',exp'),(l,(Base(([],unit_t),tag,[],efl,effects,nob)))),
        unit_t,t_env',cs@cs'@c',b_env',effects)
     | E_exit e ->
-      let (e',t',_,_,_,_) = check_exp envs imp_param true (new_t ()) e in
+      let (e',t',_,_,_,_) = check_exp envs imp_param true true ret_t (new_t ()) e in
       let efs = add_effect (BE_aux(BE_escape, l)) pure_e in
       (E_aux (E_exit e',(l,(simple_annot_efr expect_t efs))),expect_t,t_env,[],nob,efs)
+    | E_return e ->
+      check_exp envs imp_param true true ret_t ret_t e
     | E_sizeof nexp ->
       let n = anexp_to_nexp envs nexp in
       let n_subst = subst_n_with_env tp_env n in
@@ -1364,8 +1374,8 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
       let t',cs,ef,e' = type_coerce (Expr l) d_env Require false false b_env n_typ e expect_t in
       (e',t',t_env,cs,nob,ef)
     | E_assert(cond,msg) ->
-      let (cond',t',_,_,_,_) = check_exp envs imp_param true bit_t cond in
-      let (msg',mt',_,_,_,_) = check_exp envs imp_param true {t= Tapp("option",[TA_typ string_t])} msg in
+      let (cond',t',_,_,_,_) = check_exp envs imp_param true true ret_t bit_t cond in
+      let (msg',mt',_,_,_,_) = check_exp envs imp_param true true ret_t {t= Tapp("option",[TA_typ string_t])} msg in
       let (t',c') = type_consistent (Expr l) d_env Require false unit_t expect_t in
       (E_aux (E_assert(cond',msg'), (l, (simple_annot expect_t))), expect_t,t_env,c',nob,pure_e)
     | E_comment s ->
@@ -1376,37 +1386,38 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
     | E_internal_plet _ | E_internal_return _ | E_sizeof_internal _ -> 
       raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker")
 
-and recheck_for_register envs imp_param widen expect_t exp = 
-  match check_exp envs imp_param widen expect_t exp with
+and recheck_for_register envs imp_param widen_num widen_vec ret_t expect_t exp = 
+  match check_exp envs imp_param widen_num widen_vec ret_t expect_t exp with
   | exp',t',_,cs,_,ef ->
     match exp' with
     | E_aux(_, (l, Base(_, _, _, leff, ceff, _))) ->
       if has_rreg_effect ceff
-      then try let (exp',t',_,cs,_,ef) = check_exp envs imp_param widen (into_register_typ t') exp in
+      then try let (exp',t',_,cs,_,ef) = check_exp envs imp_param widen_num widen_vec ret_t (into_register_typ t') exp in
           (exp',t',cs,ef),(add_effect (BE_aux(BE_rreg,l)) pure_e),External None
         with | _ -> (exp',t',cs,ef),pure_e, Emp_local
       else (exp',t',cs,ef),pure_e, Emp_local
     | _ -> (exp',t',cs,ef),pure_e, Emp_local
 
-and check_block envs imp_param expect_t exps:((tannot exp) list * tannot * nexp_range list * t * effect) =
+and check_block envs imp_param ret_t expect_t exps:((tannot exp) list * tannot * nexp_range list * t * effect) =
   let Env(d_env,t_env,b_env,tp_env) = envs in
   match exps with
     | [] -> ([],NoTyp,[],unit_t,pure_e)
     | [e] -> 
-      let (E_aux(e',(l,annot)),t,envs,sc,_,ef) = check_exp envs imp_param true expect_t e in
+      let (E_aux(e',(l,annot)),t,envs,sc,_,ef) = check_exp envs imp_param true true ret_t expect_t e in
       ([E_aux(e',(l,annot))],annot,sc,t,ef)
     | e::exps -> 
-      let (e',t',t_env',sc,b_env',ef') = check_exp envs imp_param true unit_t e in
+      let (e',t',t_env',sc,b_env',ef') = check_exp envs imp_param true true ret_t unit_t e in
       let (exps',annot',sc',t,ef) = 
         check_block (Env(d_env,
                          Envmap.union_merge (tannot_merge (Expr Parse_ast.Unknown) d_env false) t_env t_env',
-                         merge_bounds b_env' b_env, tp_env)) imp_param expect_t exps in
+                         merge_bounds b_env' b_env, tp_env)) imp_param ret_t expect_t exps in
       let annot' = match annot' with
         | Base(pt,tag,cs,efl,efr,bounds) -> Base(pt,tag,cs,efl,union_effects efr ef',bounds)
         | _ -> annot' in
       ((e'::exps'),annot',sc@sc',t,union_effects ef ef')
 
-and check_cases envs imp_param check_t expect_t kind pexps : ((tannot pexp) list * typ * nexp_range list * effect) =
+and check_cases envs imp_param ret_t check_t expect_t kind pexps
+  : ((tannot pexp) list * typ * nexp_range list * effect) =
   let (Env(d_env,t_env,b_env,tp_env)) = envs in
   match pexps with
     | [] -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "switch with no cases found")
@@ -1415,7 +1426,7 @@ and check_cases envs imp_param check_t expect_t kind pexps : ((tannot pexp) list
       let e,t,_,cs_e,_,ef = 
         check_exp (Env(d_env,
                        Envmap.union_merge (tannot_merge (Expr l) d_env true) t_env env,
-                       merge_bounds b_env bounds, tp_env)) imp_param true expect_t exp in
+                       merge_bounds b_env bounds, tp_env)) imp_param true true ret_t expect_t exp in
       let cs = [CondCons(Expr l,kind,None, cs_p, cs_e)] in
       [Pat_aux(Pat_exp(pat',e),(l,cons_efs_annot t cs pure_e ef))],t,cs,ef
     | ((Pat_aux(Pat_exp(pat,exp),(l,annot)))::pexps) ->
@@ -1423,12 +1434,12 @@ and check_cases envs imp_param check_t expect_t kind pexps : ((tannot pexp) list
       let (e,t,_,cs_e,_,ef) = 
         check_exp (Env(d_env,
                        Envmap.union_merge (tannot_merge (Expr l) d_env true) t_env env,
-                       merge_bounds b_env bounds, tp_env)) imp_param true expect_t exp in
+                       merge_bounds b_env bounds, tp_env)) imp_param true true ret_t expect_t exp in
       let cs = CondCons(Expr l,kind,None,cs_p,cs_e) in
-      let (pes,tl,csl,efl) = check_cases envs imp_param check_t expect_t kind pexps in      
+      let (pes,tl,csl,efl) = check_cases envs imp_param ret_t check_t expect_t kind pexps in      
       ((Pat_aux(Pat_exp(pat',e),(l,cons_efs_annot t [cs] pure_e ef)))::pes,tl,cs::csl,union_effects efl ef)
 
-and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) 
+and check_lexp envs imp_param ret_t is_top (LEXP_aux(lexp,(l,annot))) 
     : (tannot lexp * typ * bool * tannot emap * tag * nexp_range list * bounds_env * effect * effect ) =
   let (Env(d_env,t_env,b_env,tp_env)) = envs in
   match lexp with
@@ -1525,14 +1536,14 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
                         let (es, cs_es, ef_es) = 
                           match args,exps with
                             | [],[] -> ([],[],pure_e)
-                            | [],[e] -> let (e',_,_,cs_e,_,ef_e) = check_exp envs imp_param true unit_t e
+                            | [],[e] -> let (e',_,_,cs_e,_,ef_e) = check_exp envs imp_param true true ret_t unit_t e
                               in ([e'],cs_e,ef_e)
                             | [],es -> typ_error l ("Expected no arguments for assignment function " ^ i)
                             | args,[] -> 
                               typ_error l ("Expected arguments with types " ^ (t_to_string args_t) ^
                                            "for assignment function " ^ i)
                             | args,es -> 
-                              (match check_exp envs imp_param true args_t (E_aux (E_tuple exps,(l,NoTyp))) with
+                              (match check_exp envs imp_param true true ret_t args_t (E_aux (E_tuple exps,(l,NoTyp))) with
                                 | (E_aux(E_tuple es,(l',tannot)),_,_,cs_e,_,ef_e) -> (es,cs_e,ef_e)
                                 | _ -> 
                                   raise (Reporting_basic.err_unreachable l 
@@ -1546,7 +1557,7 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
                           | [] -> E_aux(E_lit(L_aux(L_unit,l)),(l,NoTyp))
                           | [(E_aux(E_lit(L_aux(L_unit,_)),(_,NoTyp)) as e)] -> e
                           | es -> typ_error l ("Expected no arguments for assignment function " ^ i) in
-                        let (e,_,_,cs_e,_,ef_e) = check_exp envs imp_param true apps e in
+                        let (e,_,_,cs_e,_,ef_e) = check_exp envs imp_param true true ret_t apps e in
                         let ef_all = union_effects ef ef_e in
                         (LEXP_aux(LEXP_memory(id,[e]),(l,Base(([],out),tag,cs_call,ef,ef_all,nob))),
                          app,false,Envmap.empty,tag,cs_call@cs_e,nob,ef,ef_all))
@@ -1609,7 +1620,7 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
           let tannot = (Base(([],t),Emp_intro,[],pure_e,pure_e,new_bounds)) in
           (LEXP_aux(lexp,(l,tannot)),ty,false,Envmap.from_list [i,tannot],Emp_intro,[],new_bounds,pure_e,pure_e))
     | LEXP_vector(vec,acc) -> 
-      let (vec',vec_t,reg_required,env,tag,csi,bounds,efl,efr) = check_lexp envs imp_param false vec in
+      let (vec',vec_t,reg_required,env,tag,csi,bounds,efl,efr) = check_lexp envs imp_param ret_t false vec in
       let vec_t,cs' = get_abbrev d_env vec_t in
       let vec_actual,writing_reg_bit = match vec_t.t with
         | Tapp("register",[TA_typ {t=Tabbrev(_,t)}]) | Tapp("register",[TA_typ t])
@@ -1625,7 +1636,7 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
                                      GtEq(Specc l, Require, acc_n, (mk_sub (mk_add base n_one) rise))] 
             | _ -> typ_error l ("Assignment to one vector element requires a non-polymorphic order")
           in
-         let (e,acc_t',_,cs',_,ef_e) = check_exp envs imp_param false acc_t acc in
+         let (e,acc_t',_,cs',_,ef_e) = check_exp envs imp_param false false ret_t acc_t acc in
          let item_t_act,_ = get_abbrev d_env item_t in
          let item_t,add_reg_write,reg_still_required = 
            match item_t_act.t with
@@ -1645,7 +1656,7 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
          typ_error l "Assignment expected a vector with a known order, try adding an annotation."
        | _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string vec_t))) 
     | LEXP_vector_range(vec,e1,e2)-> 
-      let (vec',vec_t,reg_required,env,tag,csi,bounds,efl,efr) = check_lexp envs imp_param false vec in
+      let (vec',vec_t,reg_required,env,tag,csi,bounds,efl,efr) = check_lexp envs imp_param ret_t false vec in
       let vec_t,cs = get_abbrev d_env vec_t in
       let vec_actual,writing_reg_bits = match vec_t.t with
         | Tapp("register",[TA_typ {t=Tabbrev(_,t)}]) | Tapp("register",[TA_typ t])
@@ -1665,8 +1676,8 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
           let size_e1,size_e2 = new_n(),new_n() in
           let e1_t = {t=Tapp("atom",[TA_nexp size_e1])} in
           let e2_t = {t=Tapp("atom",[TA_nexp size_e2])} in
-          let (e1',e1_t',_,cs1,_,ef_e) = check_exp envs imp_param false e1_t e1 in
-          let (e2',e2_t',_,cs2,_,ef_e') = check_exp envs imp_param false e2_t e2 in
+          let (e1',e1_t',_,cs1,_,ef_e) = check_exp envs imp_param false false ret_t e1_t e1 in
+          let (e2',e2_t',_,cs2,_,ef_e') = check_exp envs imp_param false false ret_t e2_t e2 in
           let len = new_n() in
           let needs_reg = match t.t with
             | Tapp("reg",_) -> false
@@ -1702,7 +1713,7 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
         | Tuvar _ -> typ_error l "Assignement to a range of elements requires a vector with a known order, try adding an annotation."
         | _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string vec_t))) 
     | LEXP_field(vec,id)-> 
-      let (vec',item_t,reg_required,env,tag,csi,bounds,efl,efr) = check_lexp envs imp_param false vec in
+      let (vec',item_t,reg_required,env,tag,csi,bounds,efl,efr) = check_lexp envs imp_param ret_t false vec in
       let vec_t = match vec' with
         | LEXP_aux(_,(l',Base((parms,t),_,_,_,_,_))) -> t
         | _ -> item_t in
@@ -1725,7 +1736,8 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
               typ_error l ("Expected a register or struct for this update, instead found an expression with type " ^ i))
         | _ -> typ_error l ("Expected a register binding here, found " ^ (t_to_string item_t)))
 
-and check_lbind envs imp_param is_top_level emp_tag (LB_aux(lbind,(l,annot))) : tannot letbind * tannot emap * nexp_range list * bounds_env * effect =
+and check_lbind envs imp_param is_top_level opt_ret_t emp_tag (LB_aux(lbind,(l,annot)))
+  : tannot letbind * tannot emap * nexp_range list * bounds_env * effect =
   let Env(d_env,t_env,b_env,tp_env) = envs in
   match lbind with
   | LB_val_explicit(typ,pat,e) -> 
@@ -1735,7 +1747,8 @@ and check_lbind envs imp_param is_top_level emp_tag (LB_aux(lbind,(l,annot))) :
       let t,cs,ef,tp_env' = subst params false true t cs ef in
       let envs' = (Env(d_env,t_env,b_env,Envmap.union tp_env tp_env')) in
       let (pat',env,cs1,bounds,u) = check_pattern envs' emp_tag t pat in
-      let (e,t,_,cs2,_,ef2) = check_exp envs' imp_param true t e in
+      let ret_t = match opt_ret_t with Some t -> t | None -> t in
+      let (e,t,_,cs2,_,ef2) = check_exp envs' imp_param true true ret_t t e in
       let (cs,map) = if is_top_level then resolve_constraints (cs@cs1@cs2) else (cs@cs1@cs2,None) in
       let ef = union_effects ef ef2 in
       (*let _ = Printf.eprintf "checking tannot in let1\n" in*)
@@ -1751,7 +1764,8 @@ and check_lbind envs imp_param is_top_level emp_tag (LB_aux(lbind,(l,annot))) :
     | NoTyp | Overload _ -> raise (Reporting_basic.err_unreachable l "typschm_to_tannot failed to produce a Base"))
   | LB_val_implicit(pat,e) -> 
     let (pat',env,cs1,bounds,u) = check_pattern envs emp_tag (new_t ()) pat in
-    let (e,t',_,cs2,_,ef) = check_exp envs imp_param true u e in
+    let ret_t = match opt_ret_t with Some t -> t | None -> u in
+    let (e,t',_,cs2,_,ef) = check_exp envs imp_param true true ret_t u e in
     let (cs,map) = if is_top_level then resolve_constraints (cs1@cs2) else (cs1@cs2),None in
     (*let _ = Printf.eprintf "checking tannot in let2\n" in*)
     let tannot = 
@@ -2015,7 +2029,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
         let _, _ = type_consistent (Patt l) d_env Require false param_t t' in
         let exp',_,_,cs_e,_,ef = 
           check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env true) t_env t_env', 
-                         merge_bounds b_env b_env',tp_env)) imp_param true ret_t exp in
+                         merge_bounds b_env b_env',tp_env)) imp_param true true ret_t ret_t exp in
         (*let _ = Printf.eprintf "checked function %s : %s -> %s\n" 
           (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in
         let _ = Printf.eprintf "constraints were pattern: %s\n expression: %s\n" 
@@ -2109,7 +2123,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
         | _ -> typ_error l ("Expected a register with fields, given " ^ (t_to_string reg_t)))
     | AL_bit(reg_a,bit) -> 
       let (reg,reg_a,reg_t,t) = check_reg reg_a in
-      let (E_aux(bit,(le,eannot)),_,_,_,_,_) = check_exp envs None true (new_t ()) bit in
+      let (E_aux(bit,(le,eannot)),_,_,_,_,_) = check_exp envs None true true (new_t ()) (new_t ()) bit in
       (match t.t with
         | Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord order;TA_typ item_t]) ->
           (match (base.nexp,len.nexp,order.order, bit) with
@@ -2124,8 +2138,8 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
         | _ -> typ_error l ("Alias bit lookup must refer to a register with type vector, found " ^ (t_to_string t)))
     | AL_slice(reg_a,sl1,sl2) -> 
       let (reg,reg_a,reg_t,t) = check_reg reg_a in 
-      let (E_aux(sl1,(le1,eannot1)),_,_,_,_,_) = check_exp envs None false (new_t ()) sl1 in
-      let (E_aux(sl2,(le2,eannot2)),_,_,_,_,_) = check_exp envs None false (new_t ()) sl2 in
+      let (E_aux(sl1,(le1,eannot1)),_,_,_,_,_) = check_exp envs None true true (new_t ()) (new_t ()) sl1 in
+      let (E_aux(sl2,(le2,eannot2)),_,_,_,_,_) = check_exp envs None true true (new_t ()) (new_t ()) sl2 in
       (match t.t with
         | Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord order;TA_typ item_t]) ->
           (match (base.nexp,len.nexp,order.order, sl1,sl2) with
@@ -2178,7 +2192,7 @@ let check_def envs def =
     (DEF_fundef fd,envs)
   | DEF_val letdef -> 
     (*let _ = Printf.eprintf "checking letdef\n" in*)
-    let (letbind,t_env_let,_,b_env_let,eft) = check_lbind envs None true Emp_global letdef in
+    let (letbind,t_env_let,_,b_env_let,eft) = check_lbind envs None true None Emp_global letdef in
     (*let _ = Printf.eprintf "checked letdef\n" in*)
     (DEF_val letbind,Env(d_env,Envmap.union t_env t_env_let, merge_bounds b_env b_env_let, tp_env))
   | DEF_spec spec ->