change from Lean3 in dealing with open namespaces

Stream: lean4

[Damiano Testa]

Deal All,

I found the change below somewhat surprising. I can see why one of the two definitions could go either way, but the other feels like it should work.

In Lean3, either one of these two definitions works:

-- Lean3
namespace myName

def fn := 0

end myName

open myName

-- separately, they both work
def fn := fn

def fn : int := (fn : int)  -- in fact, the type ascription is unnecessary

However, in Lean4, they both fail:

namespace myName

def fn := 0

end myName

open myName

-- this fails, although it works in Lean3
def fn := fn -- failed to infer definition type, fair enough

--  I find the failure of this a little less justified, though :)
def fn : Int := Int.ofNat fn
/-
application type mismatch
  Int.ofNat fn
argument
  fn
has type
  Int : Type
but is expected to have type
  Nat : Type
-/

[James Gallicchio]

I think if you mark the definitions nonrec it has the behavior you expect. This is the behavior I'd expect as a programmer, since I'd expect recursive function names to shadow opened namespaces in scope.

[James Gallicchio]

I can't speak to the Lean3 behavior though... I find it confusing :)

[Damiano Testa]

You are completely right! In Lean4, these work (separately, of course):

nonrec def fn := fn

nonrec def fn : Int := Int.ofNat fn

Ok, I learned something, thanks!

[Damiano Testa]

Moreover, I like the possibility of controlling which behaviour to obtain: really cool!

[James Gallicchio]

It's quite clean. I end up using nonrec more often in local definitions, if I want to shadow a function with a new one that puts in some arguments or something :)

[James Gallicchio]

(Should nonrec be more prominent in docs? It's very useful but I'm not sure if the common use case is mentioned in the manual)

[Damiano Testa]

Honestly, I have yet to really dive into reading the manual: I am faking it, trying to get Lean3 syntax to work with Lean4... :upside_down:

[James Gallicchio]

hey, it works for the most part

[Damiano Testa]

Yes, not only it works, I find that when there is a change, I am usually happier with the newer version! Yay Lean4!

[Damiano Testa]

This case was one of the first where I thought that I was not so happy, and now I like it better!

[James Gallicchio]

fully agreed, Lean4 is "new and improved" with an emphasis on improved