anchor.diff:            if not must_tot ||
                lid_equals eff Const.effect_Tot_lid ||
                N.non_info_norm env k
  -          then TcUtil.check_has_type env t k' k
  +          then (* let _ = BU.print_string "Finishing on fast path!\n" in *) TcUtil.check_has_type env t k' k
             else raise_error (Errors.Fatal_UnexpectedImplictArgument,
                    (BU.format1 "Implicit argument %s is GTot, expected a Tot" (Print.term_to_string t)))
                    t.pos
  
positive.code:       else None
      in
      BU.bind_opt mk_comp (fun f ->
      BU.bind_opt (universe_of_well_typed_term env tbody) (fun u ->
      Some (S.mk (Tm_arrow(bs, f tbody (Some u))) t.pos)))
  
    | Tm_arrow(bs, c) ->
      let bs, c = SS.open_comp bs c in
  
negative.code:   let continue_fast_path t = uvars_ok || (t |> Free.uvars |> set_is_empty && t |> Free.univs |> set_is_empty) in
  
    if not (continue_fast_path t)
    then slow_path "" (Some t)
    else if not (continue_fast_path k)
    then slow_path "" (Some k)
    else
      match type_of_well_typed_tot_or_gtot_term env t with
      | None -> slow_path "could not compute the type" None
      | Some k' ->
        if not (continue_fast_path k')
        then slow_path "" (Some k')
        else
          let eff_opt = effect_of_well_typed_tot_or_gtot_term env t in
          match eff_opt with
  