anchor.diff:            effect_args = is;
             flags = [] } in
           U.arrow bs (S.mk_Comp ct)
  -      | _ -> failwith "Impossible!" in
  +      | _ -> 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);
  
positive.code:       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 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
  
    log_combinator "repr" 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 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 us, ty = SS.open_univ_vars ret_us ret_ty in
      let env = Env.push_univ_vars env0 us in
  
negative.code:   // the rest of the job to [tc_decl].
    DMFF.cps_and_elaborate env ed
  
  (*
   * Typechecking of layered effects
   *)
  let tc_layered_eff_decl env0 (ed:S.eff_decl) : S.eff_decl =
    if Env.debug env0 <| Options.Other "LayeredEffects" then
      BU.print1 "Typechecking layered effect: \n\t%s\n" (Print.eff_decl_to_string false ed);
  
    //we don't support effect binders in layered effects yet
    if List.length ed.univs <> 0 || List.length ed.binders <> 0 then
      raise_error
        (Errors.Fatal_UnexpectedEffect, "Binders are not supported for layered effects (" ^ ed.mname.str ^")")
        (range_of_lid ed.mname);
  
    (*
     * Helper function used to typecheck and generalize various effect combinators
     *
     * comb is the name of the combinator (used for error messages)
     * n is the number of universes that the combinator should be polymorphic in
     * (us, t) is the tscheme to check and generalize (us will be [] in the first phase)
     *)
    let check_and_gen (comb:string) (n:int) (us, t) : (univ_names * term * typ) =
      let us, t = SS.open_univ_vars us t in
      let t, ty =
        let t, lc, g = tc_tot_or_gtot_term (Env.push_univ_vars env0 us) t in
        Rel.force_trivial_guard env0 g;
        t, lc.res_typ in
      let g_us, t = TcUtil.generalize_universes env0 t in
      let ty = SS.close_univ_vars g_us ty in
      //check that n = List.length g_us and that if us is set, it is same as g_us
      let univs_ok =
        if List.length g_us <> n then
          let error = BU.format5
            "Expected %s:%s to be universe-polymorphic in %s universes, but found %s (tscheme: %s)"
            ed.mname.str comb (string_of_int n) (g_us |> List.length |> string_of_int)
            (Print.tscheme_to_string (g_us, t)) in
          raise_error (Errors.Fatal_MismatchUniversePolymorphic, error) t.pos;
        match us with
        | [] -> ()
        | _ ->
         if List.length us = List.length g_us &&
            List.forall2 (fun u1 u2 -> S.order_univ_name u1 u2 = 0) us g_us
         then ()
         else raise_error (Errors.Fatal_UnexpectedNumberOfUniverse,
                (BU.format4 "Expected and generalized universes in the declaration for %s:%s are different, input: %s, but after gen: %s"
                   ed.mname.str comb (Print.univ_names_to_string us) (Print.univ_names_to_string g_us)))
              t.pos in
      g_us, t, ty in
  
    let log_combinator s (us, t, ty) =
      if Env.debug env0 <| Options.Other "LayeredEffects" then
        BU.print4 "Typechecked %s:%s = %s:%s\n"
          ed.mname.str s
          (Print.tscheme_to_string (us, t)) (Print.tscheme_to_string (us, ty)) in
  
    //helper function to get (a:Type ?u), returns the binder and ?u
    let fresh_a_and_u_a (a:string) : binder * universe = U.type_u () |> (fun (t, u) -> S.gen_bv a None t |> S.mk_binder, u) in
    //helper function to get (x:a)
    let fresh_x_a (x:string) (a:binder) : binder = S.gen_bv x None (a |> fst |> S.bv_to_name) |> S.mk_binder in
  
  
    (*
     * We now typecheck various combinators
     * In all the cases we take the following approach:
     *   - Typecheck the combinator (with no expected type)
     *   - Construct an expected type (k) using various uvars
     *   - Unify the type of the combinator (as typechecked) with k
     *   - Record k in the effect declaration (along with the combinator)
     *)
  
  
    (*
     * Effect signature
     *
     * The signature term must have the form:
     *   a:Type -> <some binders> -> Effect  //polymorphic in one universe (that of a)
     *
     * The binders become the effect indices
     *)
    let signature =
      let r = (snd ed.signature).pos in
      let sig_us, sig_t, sig_ty = check_and_gen "signature" 1 ed.signature in
  
      let us, t = SS.open_univ_vars sig_us sig_t in
      let env = Env.push_univ_vars env0 us in
  