conflicting namespaces in mutual declaration

Stream: lean4

[Andrés Goens]

Is there some fundamental reason why we can't mix namespaces in mutually-recursive functions?

As an example (MWE), if I have mutually recursive types:

mutual
inductive Foo
 | somefoo : Foo
 | bar : Bar → Foo

inductive Bar
 | somebar : Bar
 | foobar : Foo → Bar → Bar
end

and want to define some functions on them, say

mutual
def Foo.ToString : Foo → String
| Foo.somefoo => "foo"
| Foo.bar b => Bar.toString b

def Bar.ToString : Bar → String
| Bar.somebar => "bar"
| Bar.foobar f b => (Foo.toString f) ++ (Bar.toString b)
end

Then Lean complains: conflicting namespaces in mutual declaration, using namespace 'Bar', but used 'Foo' in previous declaration

I know that I could solve that easily for this example (and my real-use case), by splitting it up into two "phases":

mutual
def fooToString : Foo → String
  | Foo.somefoo => "foo"
  | Foo.bar b => barToString b

def barToString : Bar → String
  | Bar.somebar => "bar"
  | Bar.foobar f b => (fooToString f) ++ (barToString b)
end

def Foo.toString : Foo → String := fooToString
def Bar.toString : Bar → String := barToString

My question is wether there's any reason (e.g. type-theoretical) why this is difficult for the general case, i.e. why Lean won't support it, or is it "just" busywork to define e.g. a hygenic expansion that does something like this?

[Leonardo de Moura]

In Lean, def Foo.bla ... is expanded to namespace Foo def bla ... end Foo. When we defined mutual commands, we wanted to keep the same semantics. This is where the restriction came from. mutual is an atomic command in Lean. To correctly support your example, we would have to simulate the namespace command in the mutual. This is doable, and it will happen in the future.
In the meantime, one can use the new _root_ modifier as a workaround. It is not perfect since the namespace Bar will not be open at Bar.Foo.

mutual
inductive Foo
 | somefoo : Foo
 | bar : Bar → Foo

inductive Bar
 | somebar : Bar
 | foobar : Foo → Bar → Bar
end

mutual
  def Foo.toString : Foo → String
    | Foo.somefoo => "foo"
    | Foo.bar b => b.toString

  def _root_.Bar.toString : Bar → String
    | Bar.somebar => "bar"
    | Bar.foobar f b => f.toString ++ b.toString
end

[Leonardo de Moura]

BTW, the example above requires the following fix pushed today https://github.com/leanprover/lean4/commit/fce7697151475aef7d46ebba052952e2148e77a4