anchor.diff:        let signature_ts = let us, t, _ = signature in (us, t) in
         TcUtil.layered_effect_indices_as_binders signature_ts u (a |> fst |> S.bv_to_name) in
       let bs = a::rest_bs in
  -    let k = U.arrow bs (U.type_u () |> (fun (t, u) -> S.mk_Total' t (Some u))) in
  +    let k = U.arrow bs (U.type_u () |> (fun (t, u) -> S.mk_Total' t (Some (new_u_univ ())))) in  //note the universe of Tot need not be u
       let g = Rel.teq env ty k in
       Rel.force_trivial_guard env g;
  -    repr_us, repr_t, SS.close_univ_vars us (N.normalize [Env.Beta] env k) in
  +    repr_us, repr_t, SS.close_univ_vars us (k |> N.remove_uvar_solutions env) in
   
     log_combinator "repr" repr;
   
  +  //helper function that creates an application node (repr<u> a_tm ?u1 ... ?un)
  +  //returns the application term and the guard for the introduced uvars (see TcUtil.fresh_layered_effect_repr)
     let fresh_repr r env u a_tm =
       let signature_ts = let us, t, _ = signature in (us, t) in
       let repr_ts = let us, t, _ = repr in (us, t) in
       TcUtil.fresh_layered_effect_repr env r ed.mname signature_ts repr_ts u a_tm in
   
  +  let not_an_arrow_error comb n t r =
  +    raise_error (Errors.Fatal_UnexpectedEffect,
  +      BU.format4 "Type of %s:%s is not an arrow with >= %s binders (%s)" ed.mname.str comb (string_of_int n) (Print.term_to_string t)
  +    ) r in
  +
  +  (*
  +   * return_repr
  +   *
  +   * return_repr must have type:
  +   *   a:Type -> <some binders> -> x:a -> repr a i_1 ... i_n  //polymorphic in one universe (that of a)
  +   *   where i_1 ... i_n are terms of effect indices types (as in the signature)
  +   *
  +   * The binders have arbitrary sorts
  +   *)
     let return_repr =
       let r = (snd ed.return_repr).pos in
  -    let ret_us, ret_t, ret_ty = check_and_gen' "return_repr" 1 None ed.return_repr in
  +    let ret_us, ret_t, ret_ty = check_and_gen "return_repr" 1 ed.return_repr in
   
       let us, ty = SS.open_univ_vars ret_us ret_ty in
       let env = Env.push_univ_vars env0 us in
  
positive.code:     let a, u = fresh_a_and_u_a "a" in
      let rest_bs = TcUtil.layered_effect_indices_as_binders (sig_us, sig_t) u (a |> fst |> S.bv_to_name) in
      let bs = a::rest_bs in
      let k = U.arrow bs (S.mk_Total S.teff) in
      let g_eq = Rel.teq env t k in
      Rel.force_trivial_guard env g_eq;
      sig_us, SS.close_univ_vars us (N.normalize [Env.Beta] env k), sig_ty in
  
    log_combinator "signature" signature;
  
    //AR: TODO: FIXME: check that repr has the type a:Type -> ...is... -> Type
    let repr =
      let r = (snd ed.repr).pos in
      let repr_us, repr_t, repr_ty = check_and_gen' "repr" 1 None ed.repr in
      
      let us, ty = SS.open_univ_vars repr_us repr_ty in
      let env = Env.push_univ_vars env0 us in
  
negative.code:           effect_args = is;
            flags = [] } in
          U.arrow bs (S.mk_Comp ct)
        | _ -> raise_error (Errors.Fatal_ActionMustHaveFunctionType, err_msg k) r in
  
      if Env.debug env <| Options.Other "LayeredEffects" then
        BU.print1 "Action type after injecting it into the monad: %s\n" (Print.term_to_string act_typ);
  