anchor.diff:             TcUtil.bind e.pos env (Some e) (TcComm.lcomp_of_comp c) (None, cres)
         else cres
       in
  +
       let e =
  +      let return_annotation = match ret_or_res_typ with
  +                              | Inl asc -> Some asc
  +                              | Inr _ -> None in
         let mk_match scrutinee =
           (* TODO (KM) : I have the impression that lifting here is useless/wrong : the scrutinee should always be pure... *)
           (* let scrutinee = TypeChecker.Util.maybe_lift env scrutinee c1.eff_name cres.eff_name c1.res_typ in *)
           let branches = t_eqns |> List.map (fun ((pat, wopt, br), _, eff_label, _, _, _, _) ->
  -              (pat, wopt, TcUtil.maybe_lift env br eff_label cres.eff_name cres.res_typ)) in
  -        let e = mk (Tm_match(scrutinee, asc_opt, branches)) top.pos in
  +          pat, wopt, TcUtil.maybe_lift env br eff_label cres.eff_name cres.res_typ
  +        ) in
  +        let e = mk (Tm_match(scrutinee, return_annotation, branches)) top.pos in
           let e = TcUtil.maybe_monadic env e cres.eff_name cres.res_typ in
           //The ascription with the result type is useful for re-checking a term, translating it to Lean etc.
  -        match asc_opt with
  -        | None -> mk (Tm_ascribed(e, (Inl cres.res_typ, None), Some cres.eff_name)) e.pos
  -        | Some _ -> e
  +        //AR: TODO: revisit, for now doing only if return annotation is not provided
  +        match ret_or_res_typ with
  +        | Inr _ -> mk (Tm_ascribed(e, (Inl cres.res_typ, None), Some cres.eff_name)) e.pos
  +        | Inl _ -> e
         in
  +
         //see issue #594: if the scrutinee is impure, then explicitly sequence it with an impure let binding
         //                to protect it from the normalizer optimizing it away
         if TcUtil.is_pure_or_ghost_effect env c1.eff_name
  
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:                      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 -> 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
          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
          let g_exhaustiveness =
            List.fold_right
              (fun (f, _, _, _) g ->  //first substitute guard_x with scrutinee bv in f
               U.mk_disj (f |> SS.subst [NT (guard_x, e1)] |> U.b2t) g)
              cases U.t_false
            |> TcUtil.label Err.exhaustiveness_check (Env.get_range env)  //label
            |> (fun f -> Env.guard_of_guard_formula (NonTrivial f)) in
          TcComm.lcomp_of_comp c, Env.conj_guard g g_exhaustiveness, erasable in
  
      //combine with e1's computation type
      let cres = TcUtil.bind e1.pos env (Some e1) c1 (Some guard_x, c_branches) in
  
      let cres =
        if erasable
        then (* promote cres to ghost *)
  