feat: allow structures to have non-bracketed binders (#8671)

This PR allow structures to have non-bracketed binders, making it
consistent with `inductive`.

The change allows the following to be written instead of having to write
`S (n)`:
```lean
structure S n where
  field : Fin n
```

Author: cppio

src/Lean/Elab/Structure.lean

@@ -30,7 +30,7 @@ namespace Structure
 
 /-! Recall that the `structure command syntax is
 ```
-leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> Term.optType >> optional «extends» >> optional (" := " >> optional structCtor >> structFields)
+leading_parser (structureTk <|> classTk) >> declId >> optDeclSig >> optional «extends» >> optional (" := " >> optional structCtor >> structFields)
 ```
 -/
 
@@ -206,10 +206,10 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
     let ref := structStx[1].mkSynthetic
     addDeclarationRangesFromSyntax declName ref
     pure { ref, declId := ref, modifiers := default, declName }
-  if structStx[5].isNone then
+  if structStx[4].isNone then
     useDefault
   else
-    let optCtor := structStx[5][1]
+    let optCtor := structStx[4][1]
     if optCtor.isNone then
       useDefault
     else
@@ -278,12 +278,12 @@ def structFields         := leading_parser many (structExplicitBinder <|> struct
 ```
 -/
 private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM (Array StructFieldView) := do
-  if structStx[5][0].isToken ":=" then
+  if structStx[4][0].isToken ":=" then
     -- https://github.com/leanprover/lean4/issues/5236
     let cmd := if structStx[0].getKind == ``Parser.Command.classTk then "class" else "structure"
-    withRef structStx[0] <| Linter.logLintIf Linter.linter.deprecated structStx[5][0]
+    withRef structStx[0] <| Linter.logLintIf Linter.linter.deprecated structStx[4][0]
       s!"{cmd} ... :=' has been deprecated in favor of '{cmd} ... where'."
-  let fieldBinders := if structStx[5].isNone then #[] else structStx[5][2][0].getArgs
+  let fieldBinders := if structStx[4].isNone then #[] else structStx[4][2][0].getArgs
   fieldBinders.foldlM (init := #[]) fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do
     let mut fieldBinder := fieldBinder
     if fieldBinder.getKind == ``Parser.Command.structSimpleBinder then
@@ -342,43 +342,45 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
       }
 
 /-
-leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> Term.optType >> optional «extends» >>
+leading_parser (structureTk <|> classTk) >> declId >> optDeclSig >> optional «extends» >>
   optional (("where" <|> ":=") >> optional structCtor >> structFields) >> optDeriving
 
 where
 def structParent := leading_parser optional (atomic (ident >> " : ")) >> termParser
-def «extends» := leading_parser " extends " >> sepBy1 structParent ", "
-def typeSpec := leading_parser " : " >> termParser
-def optType : Parser := optional typeSpec
+def «extends» := leading_parser " extends " >> sepBy1 structParent ", " >> optType
 
 def structFields         := leading_parser many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
 def structCtor           := leading_parser try (declModifiers >> ident >> " :: ")
 -/
 def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM StructView := do
+  let stx := -- for bootstrap compatibility, remove this after stage0 update
+    if stx.getNumArgs == 7
+    then stx.setArgs #[stx[0], stx[1], .node .none ``Parser.Command.optDeclSig #[stx[2], stx[3]], stx[4], stx[5], stx[6]]
+    else stx
   checkValidInductiveModifier modifiers
   let isClass   := stx[0].getKind == ``Parser.Command.classTk
   let modifiers := if isClass then modifiers.addAttr { name := `class } else modifiers
   let declId    := stx[1]
   let ⟨name, declName, levelNames⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
   addDeclarationRangesForBuiltin declName modifiers.stx stx
-  let binders   := stx[2]
-  let (optType, exts) ←
+  let (binders, type?) := expandOptDeclSig stx[2]
+  let exts := stx[3]
+  let type? ←
     -- Compatibility mode for `structure S extends P : Type` syntax
-    if stx[3].isNone && !stx[4].isNone && !stx[4][0][2].isNone then
-      logWarningAt stx[4][0][2][0] "\
+    if type?.isNone && !exts.isNone && !exts[0][2].isNone then
+      logWarningAt exts[0][2][0] "\
         The syntax is now 'structure S : Type extends P' rather than 'structure S extends P : Type'.\n\n\
         The purpose of this change is to accommodate 'structure S extends toP : P' syntax for naming parent projections."
-      pure (stx[4][0][2], stx[4])
+      pure (some exts[0][2][0][1])
     else
-      if !stx[4].isNone && !stx[4][0][2].isNone then
-        logErrorAt stx[4][0][2][0] "\
+      if !exts.isNone && !exts[0][2].isNone then
+        logErrorAt exts[0][2][0] "\
           Unexpected additional resulting type. \
           The syntax is now 'structure S : Type extends P' rather than 'structure S extends P : Type'.\n\n\
           The purpose of this change is to accommodate 'structure S extends toP : P' syntax for naming parent projections."
-      pure (stx[3], stx[4])
-  let parents   ← expandParents exts
-  let derivingClasses ← getOptDerivingClasses stx[6]
-  let type?     := if optType.isNone then none else some optType[0][1]
+      pure type?
+  let parents ← expandParents exts
+  let derivingClasses ← getOptDerivingClasses stx[5]
   let ctor ← expandCtor stx modifiers declName
   let fields ← expandFields stx modifiers declName
   fields.forM fun field => do

src/Lean/Linter/MissingDocs.lean

@@ -149,7 +149,7 @@ def checkDecl : SimpleHandler := fun stx => do
         if declModifiersPubNoDoc head then -- no doc string
           lintField rest[1][0] stx[1] "computed field"
   else if rest.getKind == ``«structure» then
-    unless rest[5][2].isNone do
+    unless rest[4][2].isNone do
       let redecls : Std.HashSet String.Pos :=
         (← get).infoState.trees.foldl (init := {}) fun s tree =>
           tree.foldInfo (init := s) fun _ info s =>
@@ -163,7 +163,7 @@ def checkDecl : SimpleHandler := fun stx => do
         if let some range := stx.getRange? then
           if redecls.contains range.start then return
         lintField parent stx "public field"
-      for stx in rest[5][2][0].getArgs do
+      for stx in rest[4][2][0].getArgs do
         let head := stx[0]
         if declModifiersPubNoDoc head then
           if stx.getKind == ``structSimpleBinder then

src/Lean/Linter/UnusedVariables.lean

@@ -189,16 +189,14 @@ builtin_initialize
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
     stack.matches [`null, none, `null, ``Lean.Parser.Command.variable])
 
-/-- `structure Foo where unused : Nat` -/
-builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
-  stack.matches [`null, none, `null, ``Lean.Parser.Command.structure])
-
-/-- `inductive Foo where | unused : Foo` -/
+/--
+* `structure Foo (unused : Nat)`
+* `inductive Foo (unused : Foo)`
+-/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
-  stack.matches [`null, none, `null, none, ``Lean.Parser.Command.inductive] &&
-  (stack[3]? |>.any fun (stx, pos) =>
-    pos == 0 &&
-    [``Lean.Parser.Command.optDeclSig, ``Lean.Parser.Command.declSig].any (stx.isOfKind ·)))
+  stack.matches [`null, none, `null, ``Lean.Parser.Command.optDeclSig, none] &&
+  (stack[4]? |>.any fun (stx, _) =>
+    [``Lean.Parser.Command.structure, ``Lean.Parser.Command.inductive].any (stx.isOfKind ·)))
 
 /--
 * `structure Foo where foo (unused : Nat) : Nat`

src/Lean/Parser/Command.lean

@@ -236,7 +236,7 @@ def «structure»          := leading_parser
     (structureTk <|> classTk) >>
     -- Note: no error recovery here due to clashing with the `class abbrev` syntax
     declId >>
-    ppIndent (many (ppSpace >> Term.bracketedBinder) >> Term.optType >> optional «extends») >>
+    ppIndent (optDeclSig >> optional «extends») >>
     optional ((symbol " := " <|> " where ") >> optional structCtor >> structFields) >>
     optDeriving
 @[builtin_command_parser] def declaration := leading_parser

tests/lean/1705.lean.expected.out

@@ -1,5 +1,2 @@
-1705.lean:1:13-1:16: error: function expected at
-  T
-term has type
-  ?m
-1705.lean:1:18-1:19: error: unexpected identifier; expected command
+1705.lean:1:22-1:23: error: type expected, got
+  (R : ?m)

tests/lean/run/structBinderIdent.lean

@@ -0,0 +1,104 @@
+/-!
+# Testing structure declarations, including unbracketed parameters
+-/
+
+/-!
+Structure with no parameters, no type, named constructor, and derived instance
+-/
+structure NatPair where
+  mkPair ::
+  fst : Nat
+  snd : Nat
+  deriving Inhabited
+
+/-- info: NatPair : Type -/
+#guard_msgs in
+#check NatPair
+
+/-- info: NatPair.mkPair (fst snd : Nat) : NatPair -/
+#guard_msgs in
+#check NatPair.mkPair
+
+/-- info: instInhabitedNatPair -/
+#guard_msgs in
+#synth Inhabited NatPair
+
+/-!
+Structure with type and no parameters
+-/
+structure Pointed : Type u where
+  α : Sort u
+  x : α
+
+/-- info: Pointed.{u} : Type u -/
+#guard_msgs in
+#check Pointed
+
+/-- info: Pointed.mk.{u} (α : Sort u) (x : α) : Pointed -/
+#guard_msgs in
+#check Pointed.mk
+
+/-!
+Structure with unbracketed parameter, no type, and derived instance
+-/
+structure Δ n where
+  val : Fin (n + 1)
+  deriving Inhabited
+
+/-- info: Δ (n : Nat) : Type -/
+#guard_msgs in
+#check Δ
+
+/-- info: Δ.mk {n : Nat} (val : Fin (n + 1)) : Δ n -/
+#guard_msgs in
+#check Δ.mk
+
+/-- info: @instInhabitedΔ -/
+#guard_msgs in
+#synth ∀ n, Inhabited (Δ n)
+
+/-!
+Structure with unbracketed parameters, type, and extends
+-/
+structure Prod₃ α β γ : Type u extends toProd : α × β where
+  trd : (γ : Type u)
+
+/-- info: Prod₃.{u} (α β γ : Type u) : Type u -/
+#guard_msgs in
+#check Prod₃
+
+/-- info: Prod₃.mk.{u} {α β γ : Type u} (toProd : α × β) (trd : γ) : Prod₃ α β γ -/
+#guard_msgs in
+#check Prod₃.mk
+
+/-- info: Prod₃.toProd.{u} {α β γ : Type u} (self : Prod₃ α β γ) : α × β -/
+#guard_msgs in
+#check Prod₃.toProd
+
+/-!
+Structure with no type and mixture of bracketed and unbracketed parameters
+-/
+structure IsLt {n} (i : Fin n) j where
+  pf : i < j
+
+/-- info: IsLt {n : Nat} (i j : Fin n) : Prop -/
+#guard_msgs in
+#check IsLt
+
+/-- info: IsLt.mk {n : Nat} {i j : Fin n} (pf : i < j) : IsLt i j -/
+#guard_msgs in
+#check IsLt.mk
+
+/-!
+Structure with type and mixture of bracketed and unbracketed parameters
+-/
+structure Eval {n} (F : Fin n → Sort u) i : Sort (max 1 u) where
+  value : F i
+
+/-- info: Eval.{u} {n : Nat} (F : Fin n → Sort u) (i : Fin n) : Sort (max 1 u) -/
+#guard_msgs in
+#check Eval
+
+/-- info: Eval.mk.{u} {n : Nat} {F : Fin n → Sort u} {i : Fin n} (value : F i) : Eval F i -/
+#guard_msgs in
+#check Eval.mk