anchor.diff:    | Sig_new_effect_for_free _ -> env
     | Sig_new_effect (ne) ->
       let env = Env.push_sigelt env se in
  +
       ne.actions |> List.fold_left (fun env a -> Env.push_sigelt env (U.action_as_lb ne.mname a)) env
     | Sig_declare_typ (_, _, _)
     | Sig_let (_, _, _) when se.sigquals |> BU.for_some (function OnlyName -> true | _ -> false) -> env
  
positive.code:     end
    | _ -> fail()
  
  let rec tc_eff_decl env0 (ed:Syntax.eff_decl) =
    assert (ed.univs = []); //no explicit universe variables in the source; Q: But what about re-type-checking a program?
    let effect_params_un, signature_un, opening = SS.open_term' ed.binders ed.signature in
    let effect_params, env, _ = tc_tparams env0 effect_params_un in
  
negative.code:   List.rev !sigelts @ sigelts', ed, lift_from_pure_opt
  
  
  let tc_lex_t env ses quals lids =
      (* We specifically type lex_t as:
  
            type lex_t<u> : Type(u) =
  