anchor.diff:      let repr, g_repr = TcUtil.fresh_effect_repr_en
         (Env.push_binders env bs)
         r sub.target u_a (a |> fst |> S.bv_to_name) in
  -    
  -    U.arrow bs (mk_Total' repr (new_u_univ () |> Some)), Env.conj_guard g_f_b g_repr in
  +
  +    let pure_wp_uvar, guard_wp = pure_wp_uvar (Env.push_binders env bs) repr
  +      (BU.format2 "implicit for pure_wp in typechecking lift %s~>%s"
  +         (Ident.string_of_lid sub.source) (Ident.string_of_lid sub.target)) r in
  +
  +    let c = S.mk_Comp ({
  +      comp_univs = [ u_a ];
  +      effect_name = PC.effect_PURE_lid;
  +      result_typ = repr;
  +      effect_args = [ pure_wp_uvar |> S.as_arg ];
  +      flags = [] }) in
  +
  +    U.arrow bs c, Env.conj_guard (Env.conj_guard g_f_b g_repr) guard_wp in
   
      if Env.debug env <| Options.Other "LayeredEffects" then
       BU.print1 "tc_layered_lift: before unification k: %s\n" (Print.term_to_string k);
  
positive.code:   g_us, t, ty
  
  (*
   * Typechecking of layered effects
   *)
  let tc_layered_eff_decl env0 (ed : S.eff_decl) (quals : list<qualifier>) =
  
negative.code:       S.gen_bv "f" None repr |> S.mk_binder, g in
      let ret_t, guard_ret_t = fresh_repr r (Env.push_binders env bs) u (fst a |> S.bv_to_name) in
  
      let pure_wp_uvar, guard_wp = pure_wp_uvar (Env.push_binders env bs) ret_t 
        (BU.format1 "implicit for pure_wp in checking stronger for %s" ed.mname.str)
        r in
      let c = S.mk_Comp ({
        comp_univs = [ Env.new_u_univ () ];
        effect_name = PC.effect_PURE_lid;
  