anchor.diff:      let k = U.arrow bs (S.mk_Total' repr (Some u_a)) in
       let g_eq = Rel.teq env ty k in
       Rel.force_trivial_guard env (Env.conj_guard g g_eq);
  -    ret_us, ret_t, k |> N.remove_uvar_solutions env |> SS.close_univ_vars us in
  +
  +    let k = k |> N.remove_uvar_solutions env in
  +
  +    let _check_valid_binders =
  +      match (SS.compress k).n with
  +      | Tm_arrow (bs, c) ->
  +        let bs, c = SS.open_comp bs c in
  +        let res_t = U.comp_result c in
  +        let bs = List.splitAt 2 bs |> snd in
  +        validate_layered_effect_binders env bs [res_t] r in
  +
  +    ret_us, ret_t, k |> SS.close_univ_vars us in
   
     log_combinator "return_repr" return_repr;
   
  
positive.code: 
      let guard_eq = Rel.teq env ty k in
      List.iter (Rel.force_trivial_guard env) [guard_f; guard_ret_t; guard_wp; guard_eq];
      stronger_us, stronger_t,
      k |> N.remove_uvar_solutions env
        |> N.normalize [Env.Beta; Env.Eager_unfolding] env
        |> SS.close_univ_vars stronger_us in
  
    log_combinator "stronger_repr" stronger_repr;
  
  
negative.code: 
    let guard_eq = Rel.teq env ty k in
    List.iter (Rel.force_trivial_guard env) [guard_f; guard_ret_t; guard_wp; guard_eq];
  
    let k = k
      |> N.remove_uvar_solutions env
      |> N.normalize [Env.Beta; Env.Eager_unfolding] env in
  
    if Env.debug env <| Options.Other "LayeredEffectsTc" then
      BU.print2 "Polymonadic subcomp %s type after unification : %s\n"
        combinator_name (Print.tscheme_to_string (us, k));
  
    let _check_valid_binders =
      match (SS.compress k).n with
      | Tm_arrow (bs, c) ->
        let bs,c = SS.open_comp bs c in
        let res_t = U.comp_result c in
        let bs, f_b =
          List.splitAt (List.length bs - 1) bs
          |> (fun (l1, l2) -> List.tl l1, List.hd l2) in
        validate_layered_effect_binders env bs [(fst f_b).sort; res_t] r in
  
  
    log_issue r (Errors.Warning_BleedingEdge_Feature,
      BU.format1 "Polymonadic subcomp (%s in this case) is an experimental feature;\
        it is subject to some redesign in the future. Please keep us informed (on github etc.) about how you are using it"
        combinator_name);
  
    (us, t), (us, k |> SS.close_univ_vars us)
  