anchor.diff:    | 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 _
  
positive.code:   | Tm_delayed _
    | Tm_bvar _ -> failwith ("Impossible: " ^ Print.term_to_string t)
  
    | Tm_name x ->
      Some x.sort
  
    | Tm_lazy i ->
      typeof_tot_or_gtot_term_fastpath env (U.unfold_lazy i) must_tot
  
    | Tm_fvar fv ->
      bind_opt (Env.try_lookup_and_inst_lid env [] fv.fv_name.v) (fun (t, _) ->
        Some t)
  
    | Tm_uinst({n=Tm_fvar fv}, us) ->
      bind_opt (Env.try_lookup_and_inst_lid env us fv.fv_name.v) (fun (t, _) ->
        Some t)
  
    (* Can't (easily) do this one efficiently, just return None *)
    | Tm_constant Const_reify
    | Tm_constant (Const_reflect _) -> None
  
    | Tm_constant sc ->
      Some (tc_constant env t.pos sc)
  
    | Tm_type u ->
      Some (mk_tm_type (U_succ u))
  
    | Tm_abs(bs, body, Some ({residual_effect=eff; residual_typ=tbody})) ->  //AR: maybe keep residual univ too?
      let mk_comp =
  
negative.code:           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
          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, _) -> 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) ->
  