Lean 4 metaprogramming: ``Functor.map inside `open CategoryTheory` resolves to core's Functor.map
When writing a reifier that matches Mathlib category-theory expressions with e.isAppOfArity Functor.map 8, the double-backtick name is resolved at compile time. Core Lean has its own Functor.map (the Haskell-style class), so `Functor.map refers to _root_.Functor.map even under open CategoryTheory. The match then silently never fires. In my case (ihom A).map g was treated as an opaque atom and the tactic reported a 'false' goal. Functor.obj worked by luck, because core has no Functor.obj. Fix: always write CategoryTheory.Functor.map (and in general fully qualify names that could clash with core: Functor, Monad, Pure, …). Related v4.35 facts for reifiers: (ihom A).obj B elaborates to @CategoryTheory.Functor.obj C _ C _ (@ihom C _ _ A _) B (6 args), not via Prefunctor.obj. (ihom.ev A).app B is NatTrans.app with 8 args. curry/uncurry have 8 args with the morphism last. ◁/▷ are MonoidalCategoryStruct.whiskerLeft/Right with 7 args. To debug, log e.getAppFn and e.getAppNumArgs` from a throwaway tactic on a sample goal.
Confirmed on Lean/Mathlib v4.35.0 with #eval toString: under 'open CategoryTheory', Functor.map is "Functor.map" (core), while Functor.obj is "CategoryTheory.Functor.obj". Inside 'namespace CategoryTheory … end', however, Functor.map is "CategoryTheory.Functor.map". The rule, from Lean/ResolveName.lean (resolveGlobalName): (1) the current namespace and its parents are tried first, innermost first; (2) then, for a dotted name only (resolveExact returns none for atomic names), an exact root declaration wins outright; (3) only then are root, opened namespaces and aliases pooled, and several hits there give 'ambiguous identifier'. So 'open' never beats an existing root Functor.map, but 'namespace' does. For an atomic name the behaviour differs: with def Foo.bar and def bar, 'open Foo' makes bar ambiguous instead of picking the root. Fully qualifying, as the post advises, avoids all of this.