anchor.diff:            BU.map_opt (typeof_tot_or_gtot_term_fastpath (Env.push_binders env bs) body false) (SS.close bs) in
         bind_opt tbody (fun tbody ->
           let bs, tbody = SS.open_term bs tbody in
  -        bind_opt (universeof_fastpath (Env.push_binders env bs) tbody) (fun u ->
  -          Some (U.arrow bs (f tbody (Some u))))))
  -
  -  | Tm_arrow(bs, c) ->
  -    let bs, c = SS.open_comp bs c in
  -    let rec aux env us bs =
  -      match bs with
  -      | [] ->
  -        bind_opt
  -          (if c  //AR: if computation is non-total, make its universe Zero
  -              |> U.comp_effect_name
  -              |> Env.norm_eff_name env
  -              |> Env.lookup_effect_quals env
  -              |> List.existsb (fun q -> q = S.TotalEffect)
  -           then universeof_fastpath env (U.comp_result c)  //AR: Why not get comp univ here if available?
  -           else Some S.U_zero)
  -          (fun uc -> Some (mk_tm_type (S.U_max (uc::us))))
  -
  -      | ({binder_bv=x;binder_qual=imp})::bs ->
  -        bind_opt (universeof_fastpath env x.sort) (fun u_x ->
  -          let env = Env.push_bv env x in
  -          aux env (u_x::us) bs)
  -    in
  -    aux env [] bs
  +        let u = universe_of (Env.push_binders env bs) tbody in
  +        Some (U.arrow bs (f tbody (Some u)))))
   
     | Tm_abs _ -> None
   
  -  | Tm_refine(x, _) ->
  -    bind_opt (universeof_fastpath env x.sort) (fun u_x ->
  -      Some (mk_tm_type u_x))
  -
  -  (* Not doing anything smart with these, so we don't even associate
  -   * them appropriately. *)
  -  (* | Tm_app({n=Tm_constant Const_reify}, a::hd::rest) *)
  -  (* | Tm_app({n=Tm_constant (Const_reflect _)}, a::hd::rest) *)
  +  | Tm_refine(x, _) -> typeof_tot_or_gtot_term_fastpath env x.sort must_tot
   
     (* Unary operators. Explicitly curry extra arguments *)
     | Tm_app({n=Tm_constant Const_range_of}, a::hd::rest) ->
  
positive.code:   | Tm_unknown
    | Tm_uinst _ -> None
    | _ -> failwith ("Impossible! (" ^ (Print.tag_of_term t) ^ ")")
  
  and universeof_fastpath env t =
    bind_opt (typeof_tot_or_gtot_term_fastpath env t false) (fun k ->
      let rec aux (maybe_norm:bool) (k:typ) =
        match (SS.compress k).n with
        | Tm_type u -> Some u
        | Tm_meta (k, _) -> aux maybe_norm k
        | Tm_refine (x, _) -> aux maybe_norm x.sort
        | Tm_ascribed (k, _, _) -> aux maybe_norm k
        | _ ->
          if maybe_norm then aux false (N.unfold_whnf env k)
          else None in
      aux true k)
  
  (*
   * Precondition: G |- t : Tot _ or G |- t : GTot _
  
negative.code:     A possible restructuring would be to treat these two (type and effect) separately
        in the return type
  *)
  
  let rec typeof_tot_or_gtot_term_fastpath (env:env) (t:term) (must_tot:bool) : option<typ> =
    let mk_tm_type u = S.mk (Tm_type u) t.pos in
    let effect_ok k = (not must_tot) || (N.non_info_norm env k) in
  