anchor.diff:  (*           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                            *)
  +
  +(*
  + * ret_opt is the optional return annotation on the match
  + * if this is set, then ascribe it on the branches for typechecking
  + * but unascribe it before returning to the caller
  + *)
   (********************************************************************************************************************)
  -and tc_eqn scrutinee env asc_opt branch
  +and tc_eqn scrutinee env ret_opt branch
           : (pat * option<term> * term)                                                             (* checked branch *)
           * term       (* the guard condition for taking this branch, used by the caller for the exhaustiveness check *)
           * lident                                                                 (* effect label of the lcomp below *)
  
positive.code:         TcUtil.maybe_monadic env e cres.eff_name cres.res_typ
      in
  
      let e, cres, g_expected_type =
        match asc_opt with
        | None -> e, cres, Env.trivial_guard
        | _ -> comp_check_expected_typ env e cres in
  
      if debug env Options.Extreme
      then BU.print2 "(%s) Typechecked Tm_match, comp type = %s\n"
                        (Range.string_of_range top.pos) (TcComm.lcomp_to_string cres);
      e, cres, Env.conj_guards [g1; g_branches; g_expected_type]
  
    | _ ->
  
negative.code:     check_inner_let_rec env top
  
  and tc_match (env : Env.env) (top : term) : term * lcomp * guard_t =
  
    (*
     * AR: Typechecking of match expression:
     *
     * match expressions may be optionally annotated with a `return` annotation
     *   for dependent pattern matching
     *
     * When the return annotation is not supplied, we:
     *   -- typecheck the scrutinee
     *   -- typecheck the branches with
     *      -- if the expected type is not set in the env, then create a new uvar for it
     *      -- a new bv, guard_x below, as the scrutinee expression
     *   -- combine the computation types of the branches (TcUtil.bind_cases)
     *      -- with the if_the_else combinator, also adding pattern exhaustiveness checks
     *   -- bind the scrutinee computation type with the combined branches (using guard_x as the bv in bind)
     *
     * When the return annotation is supplied:
     *   -- typecheck the scrutinee
     *   -- typecheck the return annotation
     *   -- typecheck the branches with
     *      -- env with expected type unset
     *      -- a new bv, guard_x, as the scrutinee expression
     *      -- substituting scrutinee bv by guard_x in the return annotation
     *      -- in tc_eqn: substituting guard_x with the pattern expression, and ascribing it on the branch exp
     *   -- if the return annotation was a type:
     *      -- TcUtil.bind_cases as before
     *   -- if the return annotation was a computation type:
     *      -- no need to bind cases, take the comp annotation as is
     *      -- but add the pattern exhaustiveness check in the guard
     *      -- need to substitute guard_x by scrutinee bv back
     *   -- bind the scrutinee computation type with the combined branches (using guard_x as the bv in bind)
     *)
  
    match (SS.compress top).n with
    | Tm_match(e1, ret_opt, eqns) ->  //ret_opt is the return annotation
      let e1, c1, g1 = tc_term
        ({(env |> Env.clear_expected_typ |> fst) with instantiate_imp = true})
        e1 in
  
      let e1, c1 =
          match TcUtil.coerce_views env e1 c1 with
          | Some (e1, c1) -> e1, c1
          | None -> e1, c1 in
  
      let env_branches, ret_or_res_typ, g1 =  //ret_or_res_typ has type either<ascription, typ>
        match ret_opt with
        | None ->  //no return annotation, set an expected type either from env or a new uvar
          (match Env.expected_typ env with
           | Some t -> env, Inr 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, Inr res_t, Env.conj_guard g1 g)
        | Some (t_or_c, None) ->
          //typecheck the return annotation and unset expected type in the env if exists
          //the branch typechecking (tc_eqn) will typecheck the branch with an ascription
          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, 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 = S.new_bv (Some e1.pos) c1.res_typ in
      let t_eqns =
        let ret_opt = match ret_or_res_typ with
                      | Inl ret ->
                        (match (e1 |> U.unascribe |> SS.compress).n with
                         | Tm_name scrutinee_bv ->
                           //substitute scrutinee_bv with guard_x in the return annotation, if exists
                           SS.subst_ascription [NT (scrutinee_bv, S.bv_to_name guard_x)] ret |> Some
                         | _ ->
                           raise_error (Errors.Fatal_UnexpectedTerm,
                           "The scrutinee must be a variable when a return annotation is supplied with a match") e1.pos)
                      | Inr _ -> None in
        eqns |> List.map (tc_eqn guard_x env_branches ret_opt) in
  
      let c_branches, g_branches, erasable =
        let cases, g, erasable =
  