feat: upstream ToLevel from mathlib

src/Lean/ToExpr.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Expr
+import Lean.ToLevel
 import Init.Data.BitVec.Basic
 universe u
 
@@ -138,34 +139,35 @@ instance : ToExpr Name where
   toExpr     := Name.toExprAux
   toTypeExpr := mkConst ``Name
 
-instance [ToExpr α] : ToExpr (Option α) :=
+instance {α : Type u} [l : ToLevel.{u}] [ToExpr α] : ToExpr (Option α) :=
   let type := toTypeExpr α
   { toExpr     := fun o => match o with
-      | none   => mkApp (mkConst ``Option.none [levelZero]) type
-      | some a => mkApp2 (mkConst ``Option.some [levelZero]) type (toExpr a),
-    toTypeExpr := mkApp (mkConst ``Option [levelZero]) type }
+      | none   => mkApp (mkConst ``Option.none [l.toLevel]) type
+      | some a => mkApp2 (mkConst ``Option.some [l.toLevel]) type (toExpr a),
+    toTypeExpr := mkApp (mkConst ``Option [l.toLevel]) type }
 
 private def List.toExprAux [ToExpr α] (nilFn : Expr) (consFn : Expr) : List α → Expr
   | []    => nilFn
   | a::as => mkApp2 consFn (toExpr a) (toExprAux nilFn consFn as)
 
-instance [ToExpr α] : ToExpr (List α) :=
+instance {α : Type u} [l : ToLevel.{u}] [ToExpr α] : ToExpr (List α) :=
   let type := toTypeExpr α
-  let nil  := mkApp (mkConst ``List.nil [levelZero]) type
-  let cons := mkApp (mkConst ``List.cons [levelZero]) type
+  let nil  := mkApp (mkConst ``List.nil [l.toLevel]) type
+  let cons := mkApp (mkConst ``List.cons [l.toLevel]) type
   { toExpr     := List.toExprAux nil cons,
-    toTypeExpr := mkApp (mkConst ``List [levelZero]) type }
+    toTypeExpr := mkApp (mkConst ``List [l.toLevel]) type }
 
-instance [ToExpr α] : ToExpr (Array α) :=
+instance {α : Type u} [l : ToLevel.{u}] [ToExpr α] : ToExpr (Array α) :=
   let type := toTypeExpr α
-  { toExpr     := fun as => mkApp2 (mkConst ``List.toArray [levelZero]) type (toExpr as.toList),
-    toTypeExpr := mkApp (mkConst ``Array [levelZero]) type }
+  { toExpr     := fun as => mkApp2 (mkConst ``List.toArray [l.toLevel]) type (toExpr as.toList),
+    toTypeExpr := mkApp (mkConst ``Array [l.toLevel]) type }
 
-instance [ToExpr α] [ToExpr β] : ToExpr (α × β) :=
+instance {α : Type u} {β : Type v} [lu : ToLevel.{u}] [lv : ToLevel.{v}]
+    [ToExpr α] [ToExpr β] : ToExpr (α × β) :=
   let αType := toTypeExpr α
   let βType := toTypeExpr β
-  { toExpr     := fun ⟨a, b⟩ => mkApp4 (mkConst ``Prod.mk [levelZero, levelZero]) αType βType (toExpr a) (toExpr b),
-    toTypeExpr := mkApp2 (mkConst ``Prod [levelZero, levelZero]) αType βType }
+  { toExpr     := fun ⟨a, b⟩ => mkApp4 (mkConst ``Prod.mk [lu.toLevel, lv.toLevel]) αType βType (toExpr a) (toExpr b),
+    toTypeExpr := mkApp2 (mkConst ``Prod [lu.toLevel, lv.toLevel]) αType βType }
 
 instance : ToExpr Literal where
   toTypeExpr := mkConst ``Literal

src/Lean/ToLevel.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller, Alex Keizer
+-/
+prelude
+import Lean.Expr
+
+/-! # `ToLevel` class
+This module defines `Lean.ToLevel`, which is the `Lean.Level` analogue to `Lean.ToExpr`.
+-/
+
+namespace Lean
+
+universe w
+
+/-- A class to create `Level` expressions that denote particular universe levels in Lean.
+`Lean.ToLevel.toLevel.{u}` evaluates to a `Lean.Level` term representing `u` -/
+class ToLevel.{u} : Type where
+  /-- A `Level` that represents the universe level `u`. -/
+  toLevel : Level
+  /-- The universe itself. This is only here to avoid the "unused universe parameter" error.
+    We'll remove this field once https://github.com/leanprover/lean4/issues/2116 gets fixed.
+  -/
+  univ : ∃ x, x = PUnit.unit.{u} := ⟨_, rfl⟩
+export ToLevel (toLevel)
+
+instance : ToLevel.{0} where
+  toLevel := .zero
+
+universe u v
+
+instance [ToLevel.{u}] : ToLevel.{u+1} where
+  toLevel := .succ toLevel.{u}
+
+/-- `ToLevel` for `max u v`. This is not an instance since it causes divergence. -/
+def ToLevel.max [ToLevel.{u}] [ToLevel.{v}] : ToLevel.{max u v} where
+  toLevel := .max toLevel.{u} toLevel.{v}
+
+/-- `ToLevel` for `imax u v`. This is not an instance since it causes divergence. -/
+def ToLevel.imax [ToLevel.{u}] [ToLevel.{v}] : ToLevel.{imax u v} where
+  toLevel := .imax toLevel.{u} toLevel.{v}
+
+end Lean

tests/lean/run/2291.lean

@@ -13,7 +13,7 @@ let _x_21 := `Nat;
 let _x_22 := [];
 let _x_23 := Lean.Expr.const _x_21 _x_22;
 let _x_24 := `List.nil;
-let _x_25 := Lean.levelZero :: _x_22;
+let _x_25 := Lean.Level.zero :: _x_22;
 let _x_26 := Lean.Expr.const _x_24 _x_25;
 let _x_27 := _x_26.app _x_23;
 let _x_28 := `List.cons;
@@ -34,7 +34,7 @@ let _x_14 := Lean.Name.str._override Lean.Name.anonymous._impl "Nat";
 let _x_15 := List.nil _neutral;
 let _x_16 := Lean.Expr.const._override _x_14 _x_15;
 let _x_17 := `List.nil;
-let _x_18 := List.cons _neutral Lean.levelZero _x_15;
+let _x_18 := List.cons _neutral Lean.Level.zero._impl _x_15;
 let _x_19 := Lean.Expr.const._override _x_17 _x_18;
 let _x_20 := Lean.Expr.app._override _x_19 _x_16;
 let _x_21 := `List.cons;
@@ -54,7 +54,7 @@ let _x_1 := Lean.Name.str._override Lean.Name.anonymous._impl "Nat";
 let _x_2 := List.nil _neutral;
 let _x_3 := Lean.Expr.const._override _x_1 _x_2;
 let _x_4 := `List.nil;
-let _x_5 := List.cons _neutral Lean.levelZero _x_2;
+let _x_5 := List.cons _neutral Lean.Level.zero._impl _x_2;
 let _x_6 := Lean.Expr.const._override _x_4 _x_5;
 let _x_7 := Lean.Expr.app._override _x_6 _x_3;
 let _x_8 := `List.cons;
@@ -84,7 +84,7 @@ Lean.Expr.const._override _eval._closed_2 _x_1
 Lean.Name.mkStr2 _eval._closed_4 _eval._closed_5
 >> _eval._closed_7
 let _x_1 := List.nil _neutral;
-List.cons _neutral Lean.levelZero _x_1
+List.cons _neutral Lean.Level.zero._impl _x_1
 >> _eval._closed_8
 Lean.Expr.const._override _eval._closed_6 _eval._closed_7
 >> _eval._closed_9