Order of definitions strange interaction with universes

Stream: lean4

[Andrés Goens]

It's not news that Lean is sensitive to the order in which things get declared, but I found a very strange interaction between this and an error about type universes in the delaborator. Here's a MWE:

This works perfectly fine:

inductive Foo
| foo : Foo

inductive Bar
| foobar : Foo → Bar
| somelist : List Bar → Bar

Whereas if we reverse the order of declaration, i.e.:

inductive Bar
| foobar : Foo → Bar
| somelist : List Bar → Bar

inductive Foo
| foo : Foo

It will give the error: "failed to compute resulting universe level of inductive datatype, provide universe explicitly"

It seems to also need both the mutually inductive construction (here with List Bar) *and * the unresolved type of Foo. Does someone know what's happening here? Why does it behave differently than, say, def, where something like

def Bar := Foo
def Foo := Nat

Lean will complain that it doesn't know the identifier Foo, but

inductive Bar
| foo : Foo → Bar
def Foo := Nat

works perfectly fine. Is this a fundamental difference or just part of the WIP nature of Lean4?

[Kevin Buzzard]

In Lean 3,

inductive Bar
| foobar : Foo → Bar
| somelist : list Bar → Bar

inductive Foo
| foo : Foo

just gives an error unknown identifier 'Foo' in the obvious place. Is Lean 4 different in this regard?

[Henrik Böving]

It is probably declaring Foo in the Bar definition as an auto implicit type. If you put mutual above and end in the end of your code block it will actually do the mutual definition.

[Andrés Goens]

Kevin Buzzard said:

In Lean 3,

inductive Bar
| foobar : Foo → Bar
| somelist : list Bar → Bar

inductive Foo
| foo : Foo

just gives an error unknown identifier 'Foo' in the obvious place. Is Lean 4 different in this regard?

yep, Lean4 will complain about universes there. Maybe it's just a bug then?

[Andrés Goens]

Henrik Böving said:

It is probably declaring Foo in the Bar definition as an auto implicit type. If you put mutual above and end in the end of your code block it will actually do the mutual definition.

That makes sense. The mutual thing does actually also get it to work as well. Might be better (more explicit) than changing the order. I guess the whole auto implicit types thing might just be more brittle for now. Thanks for the pointer!

[Henrik Böving]

I don't think the feature itself is brittle, the conclusion that it can't determine the desired universe of the auto implicit type is true since you do not give it any information at all about what that universe should be, though you can maybe argue it should indicate that something is wrong with Bar.

[Marcus Rossel]

Kevin Buzzard said:

Is Lean 4 different in this regard?

Yes, it is.
Just to make explicit what @Henrik Böving wrote about auto-implicit behavior above:
If Foo isn't a known type, then Lean 4 interprets the following definition of Bar as:

inductive Bar
| foobar : Foo → Bar

#print Bar.foobar -- constructor Bar.foobar.{u_1} : {Foo : Sort u_1} → Foo → Bar

That is, the Foo automatically becomes an implicit parameter (of type Sort u_1) to the foobar constructor.
If Foo is a known type, it has the "regular" behavior:

inductive Foo

inductive Bar
| foobar : Foo → Bar

#print Bar.foobar -- constructor Bar.foobar: Foo → Bar

[Arthur Paulino]

This prevents Lean from creating implicit parameters automatically:

set_option autoImplicit false

inductive Bar
| foobar : Foo → Bar -- unknown identifier 'Foo'

Or if you don't want that behavior in a particular declaration:

set_option autoImplicit false in
inductive Bar
| foobar : Foo → Bar -- unknown identifier 'Foo'

[Leonardo de Moura]

We will try to improve the error message.
BTW, in most color themes, variables and constants are highlighted using different colors.
image.png
image.png
Note that in the second picture, Foo is blue because it has not been interpreted as a constant.