anchor.diff:          let e = mk (Tm_let((false, [lb]), SS.close [S.mk_binder guard_x] e_match)) top.pos in
           TcUtil.maybe_monadic env e cres.eff_name cres.res_typ
       in
  +
  +    let e, cres, g_expected_type =
  +      match return_comp_opt with
  +      | None -> e, cres, Env.trivial_guard
  +      | Some c -> comp_check_expected_typ env e (TcComm.lcomp_of_comp c) 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_guard g1 g_branches
  +    e, cres, Env.conj_guards [g1; g_branches; g_expected_type]
   
     | _ ->
       failwith (BU.format1 "tc_match called on %s\n" (Print.tag_of_term top))
  
positive.code:             check_no_smt_theory_symbols env pats
          | _ -> failwith "Impossible"
  
  (************************************************************************************************************)
  (* Building the environment for the body of a let rec;                                                      *)
  (* guards the recursively bound names with a termination check                                              *)
  
negative.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 *)
  