anchor.diff:          | Some (e1, c1) -> e1, c1
           | None -> e1, c1 in
   
  -    //ret_or_res_typ has type either<either<typ, comp>, typ>
  -    let env_branches, ret_or_res_typ, ret_opt, g1 =
  +    let env_branches, ret_opt, g1 =
         match ret_opt with
  -      | None ->  //no return annotation, set an expected type either from env or a new uvar
  +      | None ->
           (match Env.expected_typ env with
  -         | Some t -> env, Inr t, None, g1
  +         | Some _ -> env, None, 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, Inr res_t, None, Env.conj_guard g1 g)
  -      | Some (t_or_c, None) ->
  -        //typecheck the return annotation and unset expected type in the env if exists,
  -        //  (we will check the expected type at the end)
  -        //the branch typechecking (tc_eqn) will typecheck the branch with an ascription
  +           Env.set_expected_typ env res_t,
  +           None,
  +           Env.conj_guard g1 g)
  +      | Some (b, asc) ->
  +        //We have a returns annotation,
  +        //  clear the expected type in the environment for the branches
  +        //  we will check the expected type for the whole match at the end
           let env, _ = Env.clear_expected_typ env in
  -        let t_or_c, g =
  -          match t_or_c with
  -           | Inl t -> let k, _ = U.type_u () in
  -                     let t, _, g = tc_check_tot_or_gtot_term env t k "" in
  -                     Inl t, g
  -           | Inr c -> let c, _, g = tc_comp env c in
  -                     Inr c, g in
  -        env, Inl t_or_c, Some (t_or_c, None), Env.conj_guard g1 g
  -      | _ ->
  -        raise_error (Errors.Fatal_UnexpectedTerm,
  -          "Tactic is not yet supported with match return") (Env.get_range env) in
  -
  -    let guard_x, t_eqns =
  -      let guard_x =
  -        match ret_opt with
  -        | None -> S.new_bv (Some e1.pos) c1.res_typ
  -        | Some _ ->
  -          (match (e1 |> U.unascribe |> SS.compress).n with
  -           | Tm_name scrutinee_bv -> scrutinee_bv
  -           | _ ->
  -             raise_error (Errors.Fatal_UnexpectedTerm,
  -               "The scrutinee must be a variable when a return annotation is supplied with a match") e1.pos) in
  -      guard_x,
  -      eqns |> List.map (tc_eqn guard_x env_branches ret_opt) in
  +        let b, asc =
  +          let bs, asc = SS.open_ascription [b] asc in
  +          let b = List.hd bs in
  +          //we set the sort of the binder to be the type of e1
  +          {b with binder_bv={b.binder_bv with sort=c1.res_typ}}, asc in
  +        //b is in scope for asc
  +        let env_asc = Env.push_binders env [b] in
  +        let asc, g_asc =
  +          match asc with
  +          | Inl t, None ->
  +            let k, _ = U.type_u () in
  +            let t, _, g = tc_check_tot_or_gtot_term env_asc t k "" in
  +            (Inl t, None), g
  +          | Inr c, None ->
  +            let c, _, g = tc_comp env_asc c in
  +            (Inr c, None), g
  +          | _ -> 
  +            raise_error (Errors.Fatal_UnexpectedTerm,
  +              "Tactic is not yet supported with match returns") (Env.get_range env) in
  +
  +        //we need to close g_asc with the binder b
  +        env,
  +        Some (b, asc),
  +        Env.conj_guard g1 (Env.close_guard env_asc [b] g_asc) in
  +
  +    //g1 is now the guard for the scrutinee and the ascription
  +    //  and it is well-formed in env
  +
  +    //the logical variable for the scrutinee
  +    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 ret_opt) in
   
       let c_branches, g_branches, erasable =
  -      let cases, g, erasable =
  -          List.fold_right
  -                (fun (branch, f, eff_label, cflags, c, g, erasable_branch) (caccum, gaccum, erasable) ->
  -                     (f, eff_label, cflags, c)::caccum,
  -                     Env.conj_guard g gaccum,
  -                     erasable || erasable_branch)
  -                t_eqns
  -                ([], Env.trivial_guard, false) in
  -
  -      (* note that bind_cases adds an exhaustiveness check *)
  -      match ret_or_res_typ with
  -      | Inr res_t ->
  -        //no return annotation, just bind_cases
  -        TcUtil.bind_cases env res_t cases guard_x, g, erasable
  -
  -      | Inl (Inl t) ->  //a return annotation, with type
  -        //set the type in the lcomp of the branches, and then bind_cases
  -
  -        let cases = List.map
  -          (fun (f, eff_label, cflags, c) ->
  -             (f, eff_label, cflags, (fun b -> TcComm.set_result_typ_lc (c b) t))) cases in
  -
  -        TcUtil.bind_cases env t cases guard_x, g, erasable
  -
  -      | Inl (Inr c) ->  //a return annotation, with computation type
  +      match ret_opt with
  +      | Some (b, (Inr c, _)) ->  //a return annotation, with computation type
  +
  +        //c has b free, so substitute it with the scrutinee
  +        let c = SS.subst_comp [NT (b.binder_bv, e1)] c in
  +
           //we don't need to bind the cases
  -        //but we still need to weaken the guards for the branches with the
  -        //negation of the branch conditions that come before this branch
  -        let fmls, gs =  //branch conditions, branch guards
  +        //but we still need to
  +        //  (a) weaken the guards for the branches with the
  +        //      negation of the branch conditions that come before this branch
  +        //  (b) add exhaustiveness check
  +        //  (c) close guard_x
  +
  +        let fmls, gs, erasables =  //branch conditions, branch guards, erasable bits
             t_eqns
  -          |> List.map (fun (_, f, _, _, _, g, _) -> (f, g))
  -          |> List.unzip in
  +          |> List.map (fun (_, f, _, _, _, g, b) -> (f, g, b))
  +          |> List.unzip3 in
           let neg_conds, exhaustiveness_cond = TcUtil.get_neg_branch_conds fmls in
           let g =
             List.map2 TcComm.weaken_guard_formula gs neg_conds
  -          |> List.fold_left Env.conj_guard Env.trivial_guard in
  +          |> Env.conj_guards in
           let g_exhaustiveness =
             U.mk_imp exhaustiveness_cond U.t_false
             |> TcUtil.label Err.exhaustiveness_check (Env.get_range env)  //label
             |> NonTrivial
             |> Env.guard_of_guard_formula in
  -        TcComm.lcomp_of_comp c, Env.conj_guard g g_exhaustiveness, erasable in
  -
  -    //combine with e1's computation type
  +        let g = Env.conj_guard g g_exhaustiveness in
  +        //weaken with guard_x == scrutinee
  +        let g = TcComm.weaken_guard_formula g
  +          (U.mk_eq2 (env.universe_of env c1.res_typ) c1.res_typ (S.bv_to_name guard_x) e1) in
  +        //close guard_x
  +        let g = Env.close_guard env [S.mk_binder guard_x] g in 
  +        TcComm.lcomp_of_comp c,
  +        g,
  +        erasables |> List.fold_left (fun acc b -> acc || b) false
  +
  +      | _ ->
  +        let cases, g, erasable =
  +          List.fold_right
  +            (fun (branch, f, eff_label, cflags, c, g, erasable_branch) (caccum, gaccum, erasable) ->
  +               (f, eff_label, cflags |> must, c |> must)::caccum,
  +               Env.conj_guard g gaccum,
  +               erasable || erasable_branch) t_eqns ([], Env.trivial_guard, false) in
  +        match ret_opt with
  +        | None ->
  +          //no returns annotation, just bind_cases
  +          //when the returns annotation is absent, env_branches contains the expected type
  +          // (which may either be coming from top, or a new uvar)
  +          let res_t = Env.expected_typ env_branches |> must in
  +          TcUtil.bind_cases env res_t cases guard_x, g, erasable
  +
  +        | Some (b, (Inl t, _)) ->  //a returns annotation, with type
  +
  +          //t has b free, so substitute it with the scrutinee
  +          let t = SS.subst [NT (b.binder_bv, e1)] t in
  +
  +          //set the type in the lcomp of the branches, and then bind_cases
  +          //AR: is this step redundant? should check
  +          let cases = List.map
  +            (fun (f, eff_label, cflags, c) ->
  +               (f, eff_label, cflags, (fun b -> TcComm.set_result_typ_lc (c b) t))) cases in
  +
  +          TcUtil.bind_cases env t cases guard_x, g, erasable
  +    in
  +
  +    //bind with e1's computation type
       let cres = TcUtil.bind e1.pos env (Some e1) c1 (Some guard_x, c_branches) in
   
       let cres =
  
positive.code:     let e, cres, g_expected_type =
        match ret_opt with
        | None -> e, cres, Env.trivial_guard
        | Some _ -> comp_check_expected_typ env e cres in
  
      if debug env Options.Extreme
      then BU.print2 "(%s) Typechecked Tm_match, comp type = %s\n"
  
negative.code: 
  (********************************************************************************************************************)
  (* Type-checking a pattern-matching branch                                                                          *)
  (* scrutinee_expr is the scrutinee expression, used when we also have a returns annotation                          *)
  (* the pattern, when_clause and branch are closed                                                                   *)
  (* scrutinee is the logical name of the expression being matched; it is not in scope in the branch                  *)
  (*   but it is in scope for the VC of the branch                                                                    *)
  (* env does not contain scrutinee, or any of the pattern-bound variables                                            *)
  (* the returned terms are well-formed in an environment extended with the scrutinee only                            *)
  
  