anchor.diff:          let z = List.zip qi.antiquotes newbvs in
   
           let lbs = List.map (fun ((bv, t), bv') ->
  -                                U.close_univs_and_mk_letbinding None (BU.Inl bv') []
  +                                U.close_univs_and_mk_letbinding None (Inl bv') []
                                                                   S.t_term Const.effect_Tot_lid
                                                                   t [] t.pos)
                              z in
  
positive.code:   (*          to the scrutinee                                                                                 *)
  
    let effect_label, cflags, maybe_return_c, g_when, g_branch =
  
      (* (a) eqs are equalities between the scrutinee and the pattern *)
      let eqs =
          if not (Env.should_verify env)
          then None
          else let e = SS.compress pat_exp in
               Some (U.mk_eq2 (env.universe_of env pat_t) pat_t scrutinee_tm e) in
  
      let c, g_branch = TcUtil.strengthen_precondition None env branch_exp c g_branch in
  
      //g_branch is trivial, its logical content is now incorporated within c
          
      let branch_has_layered_effect = c.eff_name |> Env.norm_eff_name env |> Env.is_layered_effect env in
  
      (* (b) *)
      let c_weak, g_when_weak =
       let env = Env.push_binders scrutinee_env (pat_bvs |> List.map S.mk_binder) in
       if branch_has_layered_effect
       then
         //branch_guard is a boolean, so b2t it
         let c = TcUtil.weaken_precondition env c (NonTrivial (U.b2t branch_guard)) in
         c, Env.trivial_guard  //use branch guard for weakening
       else
         match eqs, when_condition with
          | _ when not (Env.should_verify env) ->
            c, g_when
  
          | None, None ->
            c, g_when
  
          | Some f, None ->
            let gf = NonTrivial f in
            let g = Env.guard_of_guard_formula gf in
            TcUtil.weaken_precondition env c gf,
            Env.imp_guard g g_when
  
          | Some f, Some w ->
            let g_f = NonTrivial f in
            let g_fw = NonTrivial (U.mk_conj f w) in
            TcUtil.weaken_precondition env c g_fw,
            Env.imp_guard (Env.guard_of_guard_formula g_f) g_when
  
          | None, Some w ->
            let g_w = NonTrivial w in
            let g = Env.guard_of_guard_formula g_w in
            TcUtil.weaken_precondition env c g_w,
            g_when in
  
      (* (c) *)
      let binders = List.map S.mk_binder pat_bvs in
      let maybe_return_c_weak should_return =
          let c_weak =
            if should_return
            && TcComm.is_pure_or_ghost_lcomp c_weak
            then TcUtil.maybe_assume_result_eq_pure_term env branch_exp c_weak
            else c_weak
          in
          if branch_has_layered_effect
          then
            let _ = if Env.debug env <| Options.Other "LayeredEffects" then
              BU.print_string "Typechecking pat_bv_tms ...\n" in
  
            (*
             * AR: typecheck the pat_bv_tms, to resolve implicits etc.
             * 
             * recall that pat_bv_tms are terms that are definitionally equal to the pat_bvs
             *   but are in terms of projectors on the scrutinee term
             * these will be used to substitute pat bvs in the computation type
             * of the corresponding branch
             *
             * a pat_bv_tm's expected type is the sort of the corresponding pat bv
             * however, we need to be careful about dependent pat bvs of the like (a:Type) (x:a)
             *
             * so when we typecheck a pat_bv_tm with expected type as corresponding pat_bv.sort,
             *   we substitute the already seen pat bvs with their pat bv tms in the sort
             *)
  
            //first apply the pat_bv_tms to the scrutinee term
            let pat_bv_tms = pat_bv_tms |> List.map (fun pat_bv_tm ->
              mk_Tm_app pat_bv_tm [scrutinee_tm |> S.as_arg] Range.dummyRange
            ) in
  
            let pat_bv_tms =
              //note, we are explicitly setting lax = true, since these terms apply projectors
              //which we know are sound as per the branch guard, but hard to convince the typechecker
              //AR: TODO: should we instead do the non-lax typechecking but drop the logical payload in the guard?
              let env = { (Env.push_bv env scrutinee) with lax = true } in
              List.fold_left2 (fun (substs, acc) pat_bv_tm bv ->
                let expected_t = SS.subst substs bv.sort in
                //we also substitute in the pat_bv_tm, since in the case of nested patterns,
                //  there are cases when sorts of the bound scrutinee variable for the inner pattern vars
                //  contains some outer patterns vars
                let pat_bv_tm =
                  pat_bv_tm
                  |> SS.subst substs
                  |> tc_trivial_guard (Env.set_expected_typ env expected_t)
                  |> fst in
                substs@[NT (bv, pat_bv_tm)], acc@[pat_bv_tm]
              ) ([], []) pat_bv_tms pat_bvs
  
              |> snd
              |> List.map (N.normalize [Env.Beta] env) in
  
            let _ =
              if Env.debug env <| Options.Other "LayeredEffects" then
                BU.print2 "tc_eqn: typechecked pat_bv_tms %s (pat_bvs : %s)\n"
                  (List.fold_left (fun s t -> s ^ ";" ^ (Print.term_to_string t)) "" pat_bv_tms)
                  (List.fold_left (fun s t -> s ^ ";" ^ (Print.bv_to_string t)) "" pat_bvs)
              else () in
   
            c_weak
              |> TcComm.apply_lcomp (fun c -> c) (fun g ->
                  match eqs with
                  | None -> g
                  | Some eqs -> TcComm.weaken_guard_formula g eqs)
              |> TcUtil.close_layered_lcomp (Env.push_bv env scrutinee) pat_bvs pat_bv_tms
  
          else TcUtil.close_wp_lcomp env pat_bvs c_weak
      in
  
      c_weak.eff_name,
      c_weak.cflags,
      maybe_return_c_weak,
      Env.close_guard env binders g_when_weak,
      Env.conj_guard guard_pat g_branch
    in
  
    let guard = Env.conj_guard g_when g_branch in
  
  
negative.code: 
    | Tm_quoted (qt, qi)  ->
      let projl = function
        | Inl x -> x
        | Inr _ -> failwith "projl fail"
      in
      let non_trivial_antiquotes qi =
          let is_name t =
  