RFC: optionally disable automatic namespace

[madvorak]

I would like to have a project-wide setting to disable automatic opening of a namespace for the declaration's name prefix.
I would like everything inside a declaration to be evaluated the same way as if it was example instead.

theorem List.map_comp_comp {α β γ δ : Type}
    (l : List α) (f : α → β) (g : β → γ) (h : γ → δ) :
    l.map (h ∘ g ∘ f) = ((l.map f).map g).map h := by
  -- I want `map (g ∘ f) l` to be a syntax error
  have fg : map (g ∘ f) l = (l.map f).map g := by simp
  rw [←fg]
  simp

In the example above, with the new settings, I would be forced to write List.map (g ∘ f) l or l.map (g ∘ f) because map (g ∘ f) l would cause a syntax error. Currently map (g ∘ f) l is allowed and I don't like it.

Discussion:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Disable.20automatic.20namespace

[Command-Master]

Do you want to be able to use map_comp_comp without a namespace here, or even it only with the namespace?

[madvorak]

I want map_comp_comp to be error as well.

[Kha]

Please follow the RFC template if you want your RFC to be reviewed. I shouldn't have to mention that "I don't like it" is not sufficient motivation. However, I can also safely say that we would be likely to close even a comprehensive RFC for this proposal as changing such fundamental properties of the language's semantics needs to pass an extremely high justification barrier.