Weird namespace hygiene issue

[PatrickMassot]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

When elaborating a definition in a namespace that is not opened, constants appearing in that namespace take precedence over their root version.

Context

This appeared while porting the sphere eversion project. There was a long Zulip discussion but I don't think it brings anything more that the example below.

Steps to Reproduce

def Foo.Bar : Nat → Nat := id

def Bar : Nat := 3

def Foo.Baz : Nat := Bar + 2

Expected behavior: [Clear and concise description of what you expect to happen]

No error, Foo.Baz is 5.

Actual behavior: [Clear and concise description of what actually happens]

The Bar in the body definition is interpreted as Foo.Bar and leads to the error message: failed to synthesize instance HAdd (Nat → Nat) Nat Nat.

Versions

Lean (version 4.3.0-rc1, commit baa4b68a7192, Release) Ubuntu

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[digama0]

I think this is intended behavior, inside the body of def Foo.Baz it is as though it was namespace Foo def Baz, and so you are in the Foo namespace and hence it is not an ambiguous reference, the Foo.Bar definition trumps the global Bar definition. (The example that came up in the Zulip discussion which is more questionable is where the reference to Bar is in a variable but it is still interpreted as Foo.Bar.)

[PatrickMassot]

Ok, here is a new example showing the interaction with variable.

def Foo.Bar (s : String) := s ++ "."

def Bar (n : Nat) := Fin n

def succ (x : Bar n) := Fin.succ x

variable (x : Bar 2)

def Foo.Baz := succ x

Everything is fine if you comment out the last def. With the last def you get an error message on the variable line: failed to synthesize instance OfNat String 2. So I guess this is one more request to bring back the Lean 3 behavior of variable.

[kim-em]

@PatrickMassot, might be worth closing this one and starting a fresh issue in that case.

[Kha]

Same as https://github.com/leanprover/lean4/issues/1876?

[PatrickMassot]

Yes, I think this is mostly duplicate of #1876.