anchor.diff:    let torig = SS.compress t in
     if not env.instantiate_imp
     then e, torig, Env.trivial_guard
  -  else let number_of_implicits t =
  +  else begin
  +       if Env.debug env Options.High then
  +         BU.print2 "maybe_instantiate: starting check for (%s) of type (%s)\n"
  +                 (Print.term_to_string e) (Print.term_to_string t);
  +       let number_of_implicits t =
               let formals, _ = U.arrow_formals t in
               let n_implicits =
               match formals |> BU.prefix_until (fun (_, imp) -> imp=None || imp=Some Equality) with
  
positive.code:                   | _, (x, Some (Implicit dot))::rest ->
                        let t = SS.subst subst x.sort in
                        let v, _, g = new_implicit_var "Instantiation of implicit argument" e.pos env t in
                        let subst = NT(x, v)::subst in
                        let args, bs, subst, g' = aux subst (decr_inst inst_n) rest in
                        (v, Some (Implicit dot))::args, bs, subst, Env.conj_guard g g'
  
negative.code:                   | _, (x, Some (Meta tau))::rest ->
                        let t = SS.subst subst x.sort in
                        let v, _, g = new_implicit_var "Instantiation of meta argument" e.pos env t in
                        if Env.debug env Options.High then
                          BU.print1 "maybe_instantiate: Instantiating meta argument with %s\n"
                                  (Print.term_to_string v);
                        let mark_meta_implicits tau g =
                            { g with implicits =
                                List.map (fun imp -> { imp with imp_meta = Some (env, tau) }) g.implicits } in
  