Type constructors in sections

Stream: new members

[oggy]

Hi folks, as suggested to introduce myself briefly: my former academic life revolved around formal methods, mostly using Isabelle/HOL - I haven't really used dependent types before. I'm currently playing around with Lean for a toy project proving properties of a particular algorithm we use at work.
Onto the question: I'm using Lean 4, and I'm trying to create a section with definitions parameterized on some types. I've run into the following issue though (probably because I have only skimmed the books so far). Lean complains about my definition below:

section
  variable (T : Type)

  structure Struct :=
    val : T

  structure Struct2 :=
    val2: Option Struct

end

The error message being:

application type mismatch
  Option Struct
argument
  Struct
has type
  Type → Type : Type 1
but is expected to have type
  Type ?u.250 : Type (?u.250 + 1)

I think I understand roughly what's going on (Struct being what I'd call a type constructor rather than a concrete type), but I'm a bit surprised that Struct isn't "completed" to a concrete type inside of the section. Is it possible to get this automatic "completion" somehow? I'm planning to perform this development gradually, adding more (possibly parameterized) fields to Struct, and I'd like to avoid doing this manually.

A mostly unrelated question: I also didn't expect State (or type constructors in general) to be Type 1, but I think mostly because I'm not used to thinking in terms of type universes. A couple of questions there: theoretically, what's the best (and ideally concise) explanation of Lean's meta theory, and, very practically, which command can I use to see the universe of a term's type?

[David Renshaw]

#check Struct
-- Struct (T : Type) : Type

#check Type
-- Type : Type 1

[David Renshaw]

I don't know of a way to avoid needing to explicitly provide the T, like this:

  structure Struct2 :=
    val2: Option (Struct T)

[oggy]

Thanks - if there's no way around it, I can live with something like def Struct_Instantiated := Struct T.

[Eric Wieser]

That won't work though

[Eric Wieser]

You'll still have to write Struct_Instantiated T

[oggy]

Indeed, I thought I'd tried it out but I had mistyped something. But I'm now confused why Struct2 below typechecks :)

section
  variable (T : Type)

  structure Struct :=
    val : T

 structure Struct2 :=
    val2: Option Struct_Mistyped

end

[Eric Wieser]

See #lean4 > Undefined variables silently accepted

[Eric Wieser]

This is shorthand for

 structure Struct2 (Struct_Mistyped : _) :=
    val2: Option Struct_Mistyped

which is elaborated as

 structure Struct2 (Struct_Mistyped : Type u) :=
    val2: Option Struct_Mistyped

[Matthew Ballard]

Try set_option autoImplicit false in before Struct2

[Eric Wieser]

Or just set_option autoImplicit false at the top of the file

[Matthew Ballard]

Eric Wieser said:

Or just set_option autoImplicit false at the top of the file

This is probably safer until you get a hang of the behavior

[Matthew Ballard]

More info