anchor.diff:                  t_eqns
                   ([], Env.trivial_guard, false) in
         (* bind_cases adds an exhaustiveness check *)
  -      TcUtil.bind_cases env res_t cases guard_x,
  -      g,
  -      erasable
  -    in
  +      match asc_opt with
  +      | None -> TcUtil.bind_cases env (res_t_opt |> must) cases guard_x, g, erasable
  +      | Some (Inl t, _) ->
  +        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
  +      | Some (Inr c, _) ->
  +        let g_exhaustiveness =
  +          List.fold_right
  +            (fun (f, _, _, _) g -> U.mk_disj (U.b2t f) g)
  +            cases U.t_false
  +          |> TcUtil.label Err.exhaustiveness_check (Env.get_range env)
  +          |> (fun f -> Env.guard_of_guard_formula (NonTrivial f)) in
  +        TcComm.lcomp_of_comp c, Env.conj_guard g g_exhaustiveness, erasable in
   
       let cres = TcUtil.bind e1.pos env (Some e1) c1 (Some guard_x, c_branches) in
       let cres =
  
positive.code: 
  and tc_match (env : Env.env) (top : term) : term * lcomp * guard_t =
    match (SS.compress top).n with
    | Tm_match(e1, asc_opt, eqns) ->
      let env1, topt = Env.clear_expected_typ env in
      let env1 = instantiate_both env1 in
      let e1, c1, g1 = tc_term env1 e1 in
      // GM: for some reason, without this annotation on eqns,
      //     F* fails to do inference. A uvar at type Type gets
      //     solved to `list u#0`, which is ill-typed.
      let e1, c1, (eqns : list<S.branch>) =
          match TcUtil.coerce_views env e1 c1 with
          | Some (e1, c1) -> (e1, c1, eqns)
          | None -> (e1, c1, eqns)
      in
      let env_branches, return_comp_opt, res_t, g1 =
        match check_match_return_annotation e1 asc_opt (Env.get_range env) with
        | None ->
          (match topt with
           | Some t -> env, None, 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, None, res_t, Env.conj_guard g1 g)
        | Some c ->
          let c, u_c, g_c = tc_comp env c in
          Env.clear_expected_typ env |> fst,
          Some c,
          U.comp_result c,
          Env.conj_guard g1 g_c in
  
      if Env.debug env Options.Extreme
      then BU.print1 "Tm_match: expected type of branches is %s\n" (Print.term_to_string res_t);
  
      let guard_x = S.new_bv (Some e1.pos) c1.res_typ in
      let t_eqns =
        let return_comp_opt = BU.map_opt return_comp_opt (fun c ->
          match (e1 |> U.unascribe |> SS.compress).n with
          | Tm_name e1 -> SS.subst_comp [NT (e1, S.bv_to_name guard_x)] c
          | _ -> failwith "Impossible!") in        
        eqns |> List.map (tc_eqn guard_x env_branches return_comp_opt) in
  
      let c_branches, g_branches, erasable =
        let cases, g, erasable =
  
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"
  