chore: request update stage0

This PR adds the attribute `@[univ_out_params]` for specifying which
universe levels should be treated as output parameters. By default,
any universe level that does not occur in any input parameter is
considered an output parameter.

src/Init/Notation.lean

@@ -651,6 +651,17 @@ in the same module where the actual identifier was defined.
 -/
 syntax (name := suggest_for) "suggest_for" (ppSpace ident)+ : attr
 
+/--
+The attribute `@[univ_out_params ..]` on a class specifies the universe output parameters.
+
+* `@[univ_out_params]` means the class does not have universe output parameters.
+* `@[univ_out_params u v]` means the universes `u` and `v` are output parameters.
+
+If the type declaration does not contain this attribute, then Lean assumes that universe
+parameter that does not occur in any input parameter is an output one.
+-/
+syntax (name := univ_out_params) "univ_out_params" (ppSpace ident)* : attr
+
 /--
 The `@[coe]` attribute on a function (which should also appear in a
 `instance : Coe A B := ⟨myFn⟩` declaration) allows the delaborator to show

src/Lean/Class.lean

@@ -228,4 +228,30 @@ private def init :=
       setEnv env
   }
 
+builtin_initialize
+  registerBuiltinAttribute {
+    name  := `univ_out_params
+    descr := "universe output parameters for a type class"
+    add   := fun decl stx kind => do
+      unless kind == AttributeKind.global do throwAttrMustBeGlobal `univ_out_params kind
+      let env ← getEnv
+      unless isClass env decl do
+        throwError "invalid `univ_out_params`, `{decl}` is not a class"
+      let info ← getConstInfo decl
+      let us := info.levelParams
+      let args := stx[1].getArgs
+      args.forM fun arg => do
+        unless us.contains arg.getId do
+          throwErrorAt arg "`{arg}` is not a universe parameter of `{decl}`"
+      let args := args.map (·.getId)
+      let mut outLevelParams : Array Nat := #[]
+      let mut i := 0
+      for u in us do
+        if args.contains u then
+          outLevelParams := outLevelParams.push i
+        i := i + 1
+      let outParams := getOutParamPositions? env decl |>.getD #[]
+      modifyEnv fun env => classExtension.addEntry env { name := decl, outParams, outLevelParams }
+  }
+
 end Lean

src/Lean/Elab/Inductive.lean

@@ -24,7 +24,8 @@ def Lean.Parser.Command.classInductive :=
 -/
 private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (isCoinductive : Bool) : TermElabM InductiveView := do
   let isClass := decl.isOfKind ``Parser.Command.classInductive
-  let modifiers := if isClass then modifiers.addAttr { name := `class } else modifiers
+  -- **Note**: We use `addFirstAttr` to make sure the `[class]` attribute is processed **before** `[univ_out_params]
+  let modifiers := if isClass then modifiers.addFirstAttr { name := `class } else modifiers
   let (binders, type?) := expandOptDeclSig decl[2]
   let declId           := decl[1]
   let ⟨name, declName, levelNames, docString?⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers

src/Lean/Elab/Structure.lean

@@ -412,7 +412,8 @@ def structCtor           := leading_parser try (declModifiers >> ident >> " :: "
 def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM StructView := do
   checkValidInductiveModifier modifiers
   let isClass   := stx[0].getKind == ``Parser.Command.classTk
-  let modifiers := if isClass then modifiers.addAttr { name := `class } else modifiers
+  -- **Note**: We use `addFirstAttr` to make sure the `[class]` attribute is processed **before** `[univ_out_params]`
+  let modifiers := if isClass then modifiers.addFirstAttr { name := `class } else modifiers
   let declId    := stx[1]
   let ⟨name, declName, levelNames, docString?⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
   if modifiers.isMeta then

stage0/src/stdlib_flags.h

@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {

tests/lean/run/univ_out_params.lean

@@ -0,0 +1,39 @@
+import Lean
+
+open Lean Meta
+
+@[univ_out_params v]
+class ToLvl₁.{u, v} : Type where
+  dummy : ∀ (_ : Sort u) (_ : Sort v), True := fun _ _ => trivial
+
+/-- info: (some #[1]) -/
+#guard_msgs in
+run_meta do IO.println <| getOutLevelParamPositions? (← getEnv) ``ToLvl₁
+
+@[univ_out_params]
+class ToLvl₂.{u, v} : Type where
+  dummy : ∀ (_ : Sort u) (_ : Sort v), True := fun _ _ => trivial
+
+/-- info: (some #[]) -/
+#guard_msgs in
+run_meta do IO.println <| getOutLevelParamPositions? (← getEnv) ``ToLvl₂
+
+@[univ_out_params v u]
+class ToLvl₃.{u, v} : Type where
+  dummy : ∀ (_ : Sort u) (_ : Sort v), True := fun _ _ => trivial
+
+/-- info: (some #[0, 1]) -/
+#guard_msgs in
+run_meta do IO.println <| getOutLevelParamPositions? (← getEnv) ``ToLvl₃
+
+/-- error: `v` is not a universe parameter of `Foo` -/
+#guard_msgs in
+@[univ_out_params v]
+class Foo (α : Type u) where
+  a : α
+
+/-- error: invalid `univ_out_params`, `Bla` is not a class -/
+#guard_msgs in
+@[univ_out_params u]
+structure Bla (α : Type u) where
+  a : α