anchor.diff:      let unary_op, _ = U.head_and_args t in
       let head = mk (Tm_app(unary_op, [a1; a2])) (Range.union_ranges unary_op.pos (fst a1).pos) in
       let t = mk (Tm_app(head, rest)) t.pos in
  -    type_of_well_typed_term env t
  +    typeof_tot_or_gtot_term_fastpath env t
   
     | Tm_app({n=Tm_constant Const_range_of}, [_]) ->
       Some (t_range)
   
     | Tm_app({n=Tm_constant Const_set_range_of}, [(t, _); _]) ->
  -    type_of_well_typed_term env t
  +    typeof_tot_or_gtot_term_fastpath env t
   
     | Tm_app(hd, args) ->
  -    let t_hd = type_of_well_typed_term env hd in
  +    let t_hd = typeof_tot_or_gtot_term_fastpath env hd in
       let rec aux args t_hd =
         match (N.unfold_whnf env t_hd).n with
         | Tm_arrow(bs, c) ->
  
positive.code: 
      Returns (Some k), if it can find k quickly
  *)
  let rec type_of_well_typed_term (env:env) (t:term) : option<typ> =
    let mk_tm_type u = S.mk (Tm_type u) t.pos in
    let t = SS.compress t in
    match t.n with
    | Tm_delayed _
    | Tm_bvar _ -> failwith "Impossible"
  
    | Tm_name x ->
      Some x.sort
  
    | Tm_lazy i ->
      type_of_well_typed_term env (U.unfold_lazy i)
  
    | Tm_fvar fv ->
      bind_opt (Env.try_lookup_and_inst_lid env [] fv.fv_name.v) (fun (t, _) ->
  
negative.code:     if eff_hd_and_args |> is_none then
        (* let _ = BU.print_string "eff_hd_and_args turned out to be None\n" in *) None
      else
        let t_hd = typeof_tot_or_gtot_term_fastpath env hd in
        // if Env.debug env <| Options.Other "FastImplicits"
        // then BU.print2 "Computing type of hd %s to be %s\n" (Print.term_to_string hd)
        //        (match t_hd with | None -> "None" | Some k -> Print.term_to_string k);
  