anchor.diff:      | Some k' ->
         if not (continue_fast_path k')
         then slow_path "k' has uvars" (Some k')
  -      else if (not must_tot) || N.non_info_norm env k
  -      then TcUtil.check_has_type env t k' k
         else
           let eff_opt = effect_of_well_typed_tot_or_gtot_term env t in
           match eff_opt with
           | None -> slow_path "could not compute the effect" None
           | Some eff ->
  -          if lid_equals eff Const.effect_GTot_lid
  -          then raise_error (Errors.Fatal_UnexpectedImplictArgument,
  +          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
  +          else raise_error (Errors.Fatal_UnexpectedImplictArgument,
                    (BU.format1 "Implicit argument %s is GTot, expected a Tot" (Print.term_to_string t)))
                    t.pos
  -          else TcUtil.check_has_type env t k' k
  -
  +        
   let check_type_and_effect_of_well_typed_tot_or_gtot_term env t k must_total = check_well_typed_term_is_tot_or_gtot_at_type env t k must_total false
  
positive.code:   | Tm_refine _ -> Const.effect_Tot_lid |> Some
    | Tm_app (hd, args) ->
      let join_effects eff1_opt eff2_opt =
        if eff1_opt |> is_none || eff2_opt |> is_none then None
        else
          let Some eff1, Some eff2 = eff1_opt, eff2_opt in
          let tot, gtot = Const.effect_Tot_lid, Const.effect_GTot_lid in
  
          if lid_equals eff1 tot && lid_equals eff2 tot then Some tot
          else if (lid_equals eff1 gtot ||
                   lid_equals eff1 tot)
               && (lid_equals eff2 gtot ||
                   lid_equals eff2 gtot) then Some gtot
          else None in
  
      let eff_hd = effect_of_well_typed_term env hd in
  
negative.code: let type_of_well_typed_tot_or_gtot_term env t = type_of_well_typed_term env t
  
  let rec effect_of_well_typed_term (env:env) (t:term) : option<lident> =
    // if Env.debug env <| Options.Other "FastImplicits"
    // then BU.print1 "Computing effect of well-typed term: %s\n" (Print.term_to_string t);
  
    match (SS.compress t).n with
    | Tm_delayed _ | Tm_bvar _ -> failwith "Impossible!"
    | Tm_name _ -> Const.effect_Tot_lid |> Some
  