Misc fixes

src/typechecker/FStar.TypeChecker.Cfg.fst

@@ -1559,7 +1559,7 @@ let config' psteps s e =
     {tcenv = e;
      debug = if dbg_flag || Options.debug_any () then
             { gen = Env.debug e (Options.Other "Norm") || dbg_flag
-             ; top = Env.debug e (Options.Other "NormTop")
+             ; top = Env.debug e (Options.Other "NormTop") || dbg_flag
              ; cfg = Env.debug e (Options.Other "NormCfg")
              ; primop = Env.debug e (Options.Other "Primops")
              ; unfolding = Env.debug e (Options.Other "Unfolding")

src/typechecker/FStar.TypeChecker.Cfg.fsti

@@ -113,6 +113,8 @@ type debug_switches = {
     erase_erasable_args: bool;
 }
 
+val no_debug_switches : debug_switches
+
 type cfg = {
      steps: fsteps;
      tcenv: Env.env;

src/typechecker/FStar.TypeChecker.Normalize.fst

@@ -100,7 +100,7 @@ type branches = list (pat * option term * term)
 
 type stack_elt =
  | Arg      of closure * aqual * Range.range
- | UnivArgs of list universe * Range.range
+ | UnivArgs of list universe * Range.range // NB: universes must be values already, no bvars allowed
  | MemoLazy of cfg_memo (env * term)
  | Match    of env * option match_returns_ascription * branches * option residual_comp * cfg * Range.range
  | Abs      of env * binders * env * option residual_comp * Range.range //the second env is the first one extended with the binders, for reducing the option lcomp

src/typechecker/FStar.TypeChecker.TcTerm.fst

@@ -298,7 +298,9 @@ let check_expected_effect env (use_eq:bool) (copt:option comp) (ec : term * comp
                             Some g)
              else None, c, None
   in
+  def_check_comp_closed_in_env c.pos "check_expected_effect.c.before_norm" env c;
   let c = norm_c env c in
+  def_check_comp_closed_in_env c.pos "check_expected_effect.c.after_norm" env c;
   match expected_c_opt with
     | None ->
       e, c, (match gopt with | None -> Env.trivial_guard | Some g -> g)
@@ -310,6 +312,7 @@ let check_expected_effect env (use_eq:bool) (copt:option comp) (ec : term * comp
 
        let c = TcUtil.maybe_assume_result_eq_pure_term env e (TcComm.lcomp_of_comp c) in
        let c, g_c = TcComm.lcomp_comp c in
+       def_check_comp_closed_in_env c.pos "check_expected_effect.c.after_assume" env c;
        if debug env <| Options.Medium then
        BU.print4 "In check_expected_effect, asking rel to solve the problem on e=(%s) and c=(%s), expected_c=(%s), and use_eq=%s\n"
                  (Print.term_to_string e)