anchor.diff:          | Some (e1, c1) -> (e1, c1, eqns)
           | None -> (e1, c1, eqns)
       in
  -    let env_branches, res_t, g1 =
  -      match topt with
  -      | Some t -> env, t, g1
  +    let env_branches, return_comp_opt, res_t, g1 =
  +      match check_match_return_annotation e1 asc_opt (Env.get_range env) with
         | None ->
  -        let k, _ = U.type_u() in
  -        let res_t, _, g = TcUtil.new_implicit_var "match result" e1.pos env k in
  -        Env.set_expected_typ env res_t, res_t, Env.conj_guard g1 g in
  +        (match topt with
  +         | Some t -> env, None, t, g1
  +         | None ->
  +           let k, _ = U.type_u() in
  +           let res_t, _, g = TcUtil.new_implicit_var "match result" e1.pos env k in
  +           Env.set_expected_typ env res_t, None, res_t, Env.conj_guard g1 g)
  +      | Some c ->
  +        let c, u_c, g_c = tc_comp env c in
  +        Env.clear_expected_typ env |> fst,
  +        Some c,
  +        U.comp_result c,
  +        Env.conj_guard g1 g_c in
   
       if Env.debug env Options.Extreme
       then BU.print1 "Tm_match: expected type of branches is %s\n" (Print.term_to_string res_t);
   
       let guard_x = S.new_bv (Some e1.pos) c1.res_typ in
  -    let t_eqns = eqns |> List.map (tc_eqn guard_x env_branches) in
  +    let t_eqns =
  +      let return_comp_opt = BU.map_opt return_comp_opt (fun c ->
  +        match (e1 |> U.unascribe |> SS.compress).n with
  +        | Tm_name e1 -> SS.subst_comp [NT (e1, S.bv_to_name guard_x)] c
  +        | _ -> failwith "Impossible!") in        
  +      eqns |> List.map (tc_eqn guard_x env_branches return_comp_opt) in
  +
       let c_branches, g_branches, erasable =
         let cases, g, erasable =
             List.fold_right
  
positive.code: 
  and tc_match (env : Env.env) (top : term) : term * lcomp * guard_t =
    match (SS.compress top).n with
    | Tm_match(e1, eqns) ->
      let env1, topt = Env.clear_expected_typ env in
      let env1 = instantiate_both env1 in
      let e1, c1, g1 = tc_term env1 e1 in
  
negative.code:             check_no_smt_theory_symbols env pats
          | _ -> failwith "Impossible"
  
  let check_match_return_annotation (scrutinee:term) (asc_opt:option<ascription>) (r:Range.range)
    : option<comp>
    = BU.map_opt asc_opt (fun asc ->
        let error msg = raise_error (Errors.Fatal_UnexpectedTerm, msg) r in
        match asc with
        | _, Some _ -> error "tactics are not yet supported with match-return"
        | Inl _, _  -> error "match-return annotation must be a comp"
        | Inr c, _  ->
          match (scrutinee |> U.unascribe |> SS.compress).n with
          | Tm_name _ -> c
          | _ -> error "the scrutinee must be a variable when a return annotation is supplied with a match")
  
  
  (************************************************************************************************************)
  (* Building the environment for the body of a let rec;                                                      *)
  (* guards the recursively bound names with a termination check                                              *)
  