anchor.diff:    (* 3. Check the branch *)
     let branch_exp, c, g_branch =
       let branch_exp =
  -      match return_comp_opt with
  +      match asc_opt with
         | None -> branch_exp
  -      | Some c ->  //AR: TODO: check that expected type in env is None?
  -        let c = SS.subst_comp [NT (scrutinee, norm_pat_exp)] c in
  -        U.ascribe branch_exp (Inr c, None) in
  +      | Some asc ->
  +        asc
  +        |> SS.subst_ascription [NT (scrutinee, norm_pat_exp)]
  +        |> U.ascribe branch_exp in
       let branch_exp, c, g_branch = tc_term pat_env branch_exp in
       let branch_exp =
  -      match return_comp_opt with
  +      match asc_opt with
         | None -> branch_exp
         | Some _ ->
           match (SS.compress branch_exp).n with
  
positive.code: (* 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                            *)
  (********************************************************************************************************************)
  and tc_eqn scrutinee env return_comp_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 *)
  
negative.code:     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"
  