From 6bf77488f572558a29dedf3c479fd351645ed738 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Thu, 24 Oct 2024 11:27:55 -0500
Subject: [PATCH 01/14] feat: Upstream derive handler for `ToExpr` from Mathlib

---
 src/Lean/Elab/Deriving.lean        |   1 +
 src/Lean/Elab/Deriving/ToExpr.lean | 232 +++++++++++++++++++++++++++++
 src/Lean/ToLevel.lean              |  41 +++++
 3 files changed, 274 insertions(+)
 create mode 100644 src/Lean/Elab/Deriving/ToExpr.lean
 create mode 100644 src/Lean/ToLevel.lean

diff --git a/src/Lean/Elab/Deriving.lean b/src/Lean/Elab/Deriving.lean
index d6b9aef0289a..c119ae627390 100644
--- a/src/Lean/Elab/Deriving.lean
+++ b/src/Lean/Elab/Deriving.lean
@@ -16,3 +16,4 @@ import Lean.Elab.Deriving.FromToJson
 import Lean.Elab.Deriving.SizeOf
 import Lean.Elab.Deriving.Hashable
 import Lean.Elab.Deriving.Ord
+import Lean.Elab.Deriving.ToExpr
diff --git a/src/Lean/Elab/Deriving/ToExpr.lean b/src/Lean/Elab/Deriving/ToExpr.lean
new file mode 100644
index 000000000000..b8382754ce2a
--- /dev/null
+++ b/src/Lean/Elab/Deriving/ToExpr.lean
@@ -0,0 +1,232 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Lean.Meta.Transform
+import Lean.Elab.Deriving.Basic
+import Lean.Elab.Deriving.Util
+import Lean.ToExpr
+import Lean.ToLevel
+
+
+/-!
+# A `ToExpr` derive handler
+
+This module defines a `ToExpr` derive handler for inductive types. It supports mutually inductive
+types as well.
+
+The `ToExpr` derive handlers support universe level polymorphism. This is implemented using the
+`Lean.ToLevel` class. To use `ToExpr` in places where there is universe polymorphism, make sure
+to have a `[ToLevel.{u}]` instance available.
+
+Implementation note: this derive handler was originally modeled after the `Repr` derive handler.
+-/
+
+namespace Lean.Deriving.ToExpr
+
+open Lean Elab Lean.Parser.Term
+open Meta Command Deriving
+
+/-- Specialization of `Lean.Elab.Deriving.mkHeader` for `ToExpr`. -/
+def mkToExprHeader (indVal : InductiveVal) : TermElabM Header := do
+  -- The auxiliary functions we produce are `indtype -> Expr`.
+  let header ← mkHeader ``ToExpr 1 indVal
+  return header
+
+/-- Give a term that is equivalent to `(term| mkAppN $f #[$args,*])`.
+As an optimization, `mkAppN` is pre-expanded out to use `Expr.app` directly. -/
+def mkAppNTerm (f : Term) (args : Array Term) : MetaM Term :=
+  args.foldlM (fun a b => `(Expr.app $a $b)) f
+
+/-- Create the body of the `toExpr` function
+for the `ToExpr` instance, which is a `match` expression
+that calls `toExpr` and `toTypeExpr` to assemble an expression for a given term.
+For recursive inductive types, `auxFunName` refers to the `ToExpr` instance
+for the current type.
+For mutually recursive types, we rely on the local instances set up by `mkLocalInstanceLetDecls`. -/
+def mkToExprBody (header : Header) (indVal : InductiveVal) (auxFunName : Name) :
+    TermElabM Term := do
+  let discrs ← mkDiscrs header indVal
+  let alts ← mkAlts
+  `(match $[$discrs],* with $alts:matchAlt*)
+where
+  /-- Create the `match` cases, one per constructor. -/
+  mkAlts : TermElabM (Array (TSyntax ``matchAlt)) := do
+    let mut alts := #[]
+    for ctorName in indVal.ctors do
+      let ctorInfo ← getConstInfoCtor ctorName
+      let alt ← forallTelescopeReducing ctorInfo.type fun xs _ => do
+        let mut patterns := #[]
+        -- add `_` pattern for indices
+        for _ in [:indVal.numIndices] do
+          patterns := patterns.push (← `(_))
+        let mut ctorArgs := #[]
+        let mut rhsArgs : Array Term := #[]
+        let mkArg (x : Expr) (a : Term) : TermElabM Term := do
+          if (← inferType x).isAppOf indVal.name then
+            `($(mkIdent auxFunName) $a)
+          else if ← Meta.isType x then
+            `(toTypeExpr $a)
+          else
+            `(toExpr $a)
+        -- add `_` pattern for inductive parameters, which are inaccessible
+        for i in [:ctorInfo.numParams] do
+          let a := mkIdent header.argNames[i]!
+          ctorArgs := ctorArgs.push (← `(_))
+          rhsArgs := rhsArgs.push <| ← mkArg xs[i]! a
+        for i in [:ctorInfo.numFields] do
+          let a := mkIdent (← mkFreshUserName `a)
+          ctorArgs := ctorArgs.push a
+          rhsArgs := rhsArgs.push <| ← mkArg xs[ctorInfo.numParams + i]! a
+        patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs:term*))
+        let levels ← indVal.levelParams.toArray.mapM (fun u => `(toLevel.{$(mkIdent u)}))
+        let rhs : Term ←
+          mkAppNTerm (← `(Expr.const $(quote ctorInfo.name) [$levels,*])) rhsArgs
+        `(matchAltExpr| | $[$patterns:term],* => $rhs)
+      alts := alts.push alt
+    return alts
+
+/-- Create the body of the `toTypeExpr` function for the `ToExpr` instance.
+Calls `toExpr` and `toTypeExpr` to the arguments to the type constructor. -/
+def mkToTypeExpr (argNames : Array Name) (indVal : InductiveVal) : TermElabM Term := do
+  let levels ← indVal.levelParams.toArray.mapM (fun u => `(toLevel.{$(mkIdent u)}))
+  forallTelescopeReducing indVal.type fun xs _ => do
+    let mut args : Array Term := #[]
+    for i in [:xs.size] do
+      let x := xs[i]!
+      let a := mkIdent argNames[i]!
+      if ← Meta.isType x then
+        args := args.push <| ← `(toTypeExpr $a)
+      else
+        args := args.push <| ← `(toExpr $a)
+    mkAppNTerm (← `((Expr.const $(quote indVal.name) [$levels,*]))) args
+
+/--
+For mutually recursive inductive types, the strategy is to have local `ToExpr` instances in scope
+for each of the inductives when defining each instance.
+This way, each instance can freely use `toExpr` and `toTypeExpr` for each of the other types.
+
+Note that each instance gets its own definition of each of the others' `toTypeExpr` fields.
+(This is working around the fact that the `Deriving.Context` API assumes
+that each instance in mutual recursion only has a single auxiliary definition.
+There are other ways to work around it, but `toTypeExpr` implementations
+are very simple, so duplicating them seemed to be OK.) -/
+def mkLocalInstanceLetDecls (ctx : Deriving.Context) (argNames : Array Name) :
+    TermElabM (Array (TSyntax ``Parser.Term.letDecl)) := do
+  let mut letDecls := #[]
+  for i in [:ctx.typeInfos.size] do
+    let indVal       := ctx.typeInfos[i]!
+    let auxFunName   := ctx.auxFunNames[i]!
+    let currArgNames ← mkInductArgNames indVal
+    let numParams    := indVal.numParams
+    let currIndices  := currArgNames[numParams:]
+    let binders      ← mkImplicitBinders currIndices
+    let argNamesNew  := argNames[:numParams] ++ currIndices
+    let indType      ← mkInductiveApp indVal argNamesNew
+    let instName     ← mkFreshUserName `localinst
+    let toTypeExpr   ← mkToTypeExpr argNames indVal
+    let letDecl      ← `(Parser.Term.letDecl| $(mkIdent instName):ident $binders:implicitBinder* :
+                            ToExpr $indType :=
+                          { toExpr := $(mkIdent auxFunName), toTypeExpr := $toTypeExpr })
+    letDecls := letDecls.push letDecl
+  return letDecls
+
+/-- Fix the output of `mkInductiveApp` to explicitly reference universe levels. -/
+def fixIndType (indVal : InductiveVal) (t : Term) : TermElabM Term :=
+  match t with
+  | `(@$f $args*) =>
+    let levels := indVal.levelParams.toArray.map mkIdent
+    `(@$f.{$levels,*} $args*)
+  | _ => throwError "(internal error) expecting output of `mkInductiveApp`"
+
+/-- Make `ToLevel` instance binders for all the level variables. -/
+def mkToLevelBinders (indVal : InductiveVal) : TermElabM (TSyntaxArray ``instBinderF) := do
+  indVal.levelParams.toArray.mapM (fun u => `(instBinderF| [ToLevel.{$(mkIdent u)}]))
+
+open TSyntax.Compat in
+/-- Make a `toExpr` function for the given inductive type.
+The implementations of each `toExpr` function for a (mutual) inductive type
+are given as top-level private definitions.
+These end up being assembled into `ToExpr` instances in `mkInstanceCmds`.
+For mutual inductive types,
+then each of the other types' `ToExpr` instances are provided as local instances,
+to wire together the recursion (this necessitates these auxiliary definitions being `partial`). -/
+def mkAuxFunction (ctx : Deriving.Context) (i : Nat) : TermElabM Command := do
+  let auxFunName := ctx.auxFunNames[i]!
+  let indVal     := ctx.typeInfos[i]!
+  let header     ← mkToExprHeader indVal
+  let mut body   ← mkToExprBody header indVal auxFunName
+  if ctx.usePartial then
+    let letDecls ← mkLocalInstanceLetDecls ctx header.argNames
+    body ← mkLet letDecls body
+  -- We need to alter the last binder (the one for the "target") to have explicit universe levels
+  -- so that the `ToLevel` instance arguments can use them.
+  let addLevels binder :=
+    match binder with
+    | `(bracketedBinderF| ($a : $ty)) => do `(bracketedBinderF| ($a : $(← fixIndType indVal ty)))
+    | _ => throwError "(internal error) expecting inst binder"
+  let binders := header.binders.pop
+    ++ (← mkToLevelBinders indVal)
+    ++ #[← addLevels header.binders.back]
+  let levels := indVal.levelParams.toArray.map mkIdent
+  if ctx.usePartial then
+    `(private partial def $(mkIdent auxFunName):ident.{$levels,*} $binders:bracketedBinder* :
+        Expr := $body:term)
+  else
+    `(private def $(mkIdent auxFunName):ident.{$levels,*} $binders:bracketedBinder* :
+        Expr := $body:term)
+
+/-- Create all the auxiliary functions using `mkAuxFunction` for the (mutual) inductive type(s).
+Wraps the resulting definition commands in `mutual ... end`. -/
+def mkMutualBlock (ctx : Deriving.Context) : TermElabM Syntax := do
+  let mut auxDefs := #[]
+  for i in [:ctx.typeInfos.size] do
+    auxDefs := auxDefs.push (← mkAuxFunction ctx i)
+  `(mutual $auxDefs:command* end)
+
+open TSyntax.Compat in
+/-- Assuming all of the auxiliary definitions exist, create all the `instance` commands
+for the `ToExpr` instances for the (mutual) inductive type(s). -/
+def mkInstanceCmds (ctx : Deriving.Context) (typeNames : Array Name) :
+    TermElabM (Array Command) := do
+  let mut instances := #[]
+  for i in [:ctx.typeInfos.size] do
+    let indVal       := ctx.typeInfos[i]!
+    if typeNames.contains indVal.name then
+      let auxFunName   := ctx.auxFunNames[i]!
+      let argNames     ← mkInductArgNames indVal
+      let binders      ← mkImplicitBinders argNames
+      let binders      := binders ++ (← mkInstImplicitBinders ``ToExpr indVal argNames)
+      let binders      := binders ++ (← mkToLevelBinders indVal)
+      let indType      ← fixIndType indVal (← mkInductiveApp indVal argNames)
+      let toTypeExpr   ← mkToTypeExpr argNames indVal
+      let levels       := indVal.levelParams.toArray.map mkIdent
+      let instCmd ← `(instance $binders:implicitBinder* : ToExpr $indType where
+                        toExpr := $(mkIdent auxFunName).{$levels,*}
+                        toTypeExpr := $toTypeExpr)
+      instances := instances.push instCmd
+  return instances
+
+/-- Returns all the commands generated by `mkMutualBlock` and `mkInstanceCmds`. -/
+def mkToExprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
+  let ctx ← mkContext "toExpr" declNames[0]!
+  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx declNames)
+  trace[Elab.Deriving.toExpr] "\n{cmds}"
+  return cmds
+
+/-- The main entry point to the `ToExpr` derive handler. -/
+def mkToExprInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
+  if (← declNames.allM isInductive) && declNames.size > 0 then
+    let cmds ← liftTermElabM <| mkToExprInstanceCmds declNames
+    cmds.forM elabCommand
+    return true
+  else
+    return false
+
+builtin_initialize
+  registerDerivingHandler ``Lean.ToExpr mkToExprInstanceHandler
+  registerTraceClass `Elab.Deriving.toExpr
+
+end Lean.Deriving.ToExpr
diff --git a/src/Lean/ToLevel.lean b/src/Lean/ToLevel.lean
new file mode 100644
index 000000000000..e8cab6c6d451
--- /dev/null
+++ b/src/Lean/ToLevel.lean
@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+import Lean
+
+/-! # `ToLevel` class
+
+This module defines `Lean.ToLevel`, which is the `Lean.Level` analogue to `Lean.ToExpr`.
+
+-/
+
+namespace Lean
+
+/-- 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} 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. -/
+  univ : Type u := Sort u
+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

From 92b4402e8c9a182d260b9135c2418aa9bb3a621a Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Thu, 31 Oct 2024 14:28:43 -0500
Subject: [PATCH 02/14] fix: use prelude in `ToLevel`

---
 src/Lean/ToLevel.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/ToLevel.lean b/src/Lean/ToLevel.lean
index e8cab6c6d451..11b264803a41 100644
--- a/src/Lean/ToLevel.lean
+++ b/src/Lean/ToLevel.lean
@@ -3,7 +3,8 @@ Copyright (c) 2023 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
-import Lean
+prelude
+import Lean.Expr
 
 /-! # `ToLevel` class
 

From 0970d1a1a057136a940367802889575b4a5b234d Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Thu, 31 Oct 2024 15:21:43 -0500
Subject: [PATCH 03/14] fix: ensure `ToLevel.{u}` lives in `Type u` (rather
 than `Type (u+1)`)

---
 src/Lean/ToLevel.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/ToLevel.lean b/src/Lean/ToLevel.lean
index 11b264803a41..7a7f364ab0de 100644
--- a/src/Lean/ToLevel.lean
+++ b/src/Lean/ToLevel.lean
@@ -20,7 +20,7 @@ class ToLevel.{u} 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. -/
-  univ : Type u := Sort u
+  univ : Sort u := PUnit.{u}
 export ToLevel (toLevel)
 
 instance : ToLevel.{0} where

From 659894034214fa4dbf1b1a18b9c5656acf6679e5 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Thu, 31 Oct 2024 17:06:15 -0500
Subject: [PATCH 04/14] fix: ensure that `ToLevel.{u} : Type`, for all
 universes `u`

---
 src/Lean/ToLevel.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/Lean/ToLevel.lean b/src/Lean/ToLevel.lean
index 7a7f364ab0de..d6476a7fd771 100644
--- a/src/Lean/ToLevel.lean
+++ b/src/Lean/ToLevel.lean
@@ -14,13 +14,17 @@ This module defines `Lean.ToLevel`, which is the `Lean.Level` analogue to `Lean.
 
 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} 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. -/
-  univ : Sort u := PUnit.{u}
+  /-- 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

From 0e357ae29860dab3da7cb6975aef1c225f6349be Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Thu, 5 Dec 2024 13:03:05 +0000
Subject: [PATCH 05/14] remove old ToLevel pre-merge

---
 src/Lean/ToLevel.lean | 46 -------------------------------------------
 1 file changed, 46 deletions(-)
 delete mode 100644 src/Lean/ToLevel.lean

diff --git a/src/Lean/ToLevel.lean b/src/Lean/ToLevel.lean
deleted file mode 100644
index d6476a7fd771..000000000000
--- a/src/Lean/ToLevel.lean
+++ /dev/null
@@ -1,46 +0,0 @@
-/-
-Copyright (c) 2023 Kyle Miller. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kyle Miller
--/
-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} 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

From c04f9e72a67380309d4513b564b2113992aace94 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 11 Dec 2024 14:31:59 +0000
Subject: [PATCH 06/14] use Array.back!

---
 src/Lean/Elab/Deriving/ToExpr.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Deriving/ToExpr.lean b/src/Lean/Elab/Deriving/ToExpr.lean
index b8382754ce2a..4234504fd392 100644
--- a/src/Lean/Elab/Deriving/ToExpr.lean
+++ b/src/Lean/Elab/Deriving/ToExpr.lean
@@ -169,7 +169,7 @@ def mkAuxFunction (ctx : Deriving.Context) (i : Nat) : TermElabM Command := do
     | _ => throwError "(internal error) expecting inst binder"
   let binders := header.binders.pop
     ++ (← mkToLevelBinders indVal)
-    ++ #[← addLevels header.binders.back]
+    ++ #[← addLevels header.binders.back!]
   let levels := indVal.levelParams.toArray.map mkIdent
   if ctx.usePartial then
     `(private partial def $(mkIdent auxFunName):ident.{$levels,*} $binders:bracketedBinder* :

From 39e065a59e79c99c57c222ba6cc57a3075b282f0 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 11 Dec 2024 14:35:48 +0000
Subject: [PATCH 07/14] move namespace to Lean.Elab.Deriving.ToExpr

This also ensures that `mkLet` is resolved to `Lean.Elab.Deriving.mkLet` (as intended) instead of `Lean.mkLet`
---
 src/Lean/Elab/Deriving/ToExpr.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Deriving/ToExpr.lean b/src/Lean/Elab/Deriving/ToExpr.lean
index 4234504fd392..f7ab0181c3c1 100644
--- a/src/Lean/Elab/Deriving/ToExpr.lean
+++ b/src/Lean/Elab/Deriving/ToExpr.lean
@@ -24,7 +24,7 @@ to have a `[ToLevel.{u}]` instance available.
 Implementation note: this derive handler was originally modeled after the `Repr` derive handler.
 -/
 
-namespace Lean.Deriving.ToExpr
+namespace Lean.Elab.Deriving.ToExpr
 
 open Lean Elab Lean.Parser.Term
 open Meta Command Deriving
@@ -229,4 +229,4 @@ builtin_initialize
   registerDerivingHandler ``Lean.ToExpr mkToExprInstanceHandler
   registerTraceClass `Elab.Deriving.toExpr
 
-end Lean.Deriving.ToExpr
+end Lean.Elab.Deriving.ToExpr

From 182775aa4f00514719ffb815881e44b9d02f868a Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 11 Dec 2024 14:43:30 +0000
Subject: [PATCH 08/14] deriving test cases

The final test case currently fails, exposing a bug when auto implicits are disabled
---
 tests/lean/run/derivingToExpr.lean | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 tests/lean/run/derivingToExpr.lean

diff --git a/tests/lean/run/derivingToExpr.lean b/tests/lean/run/derivingToExpr.lean
new file mode 100644
index 000000000000..c3504075ccb1
--- /dev/null
+++ b/tests/lean/run/derivingToExpr.lean
@@ -0,0 +1,22 @@
+import Lean.Elab.Deriving.ToExpr
+
+open Lean (ToExpr)
+
+-- Test with a universe polymporphic type parameter
+inductive Option' (α : Type u)
+  | some (a : α)
+  | none
+  deriving ToExpr
+
+-- Test with recursive type
+inductive List' (α : Type u)
+  | cons (a : α) (as : List' α)
+  | nil
+  deriving ToExpr
+
+-- Test without (universe) auto implicit
+set_option autoImplicit false in
+inductive ExplicitList'.{u} (α : Type u)
+  | cons (a : α) (as : List' α)
+  | nil
+  deriving ToExpr

From 20d4a2c6c6b275748f6eb32b5f31d9b248886749 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 11 Dec 2024 14:53:28 +0000
Subject: [PATCH 09/14] expand test to actually exercise generated instance

---
 tests/lean/run/derivingToExpr.lean     | 30 +++++++++++++++++++++++++-
 tests/lean/run/derivingToExpr.lean.out |  0
 2 files changed, 29 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/derivingToExpr.lean.out

diff --git a/tests/lean/run/derivingToExpr.lean b/tests/lean/run/derivingToExpr.lean
index c3504075ccb1..c0880309a0a1 100644
--- a/tests/lean/run/derivingToExpr.lean
+++ b/tests/lean/run/derivingToExpr.lean
@@ -1,6 +1,8 @@
 import Lean.Elab.Deriving.ToExpr
 
-open Lean (ToExpr)
+open Lean
+
+deriving instance ToExpr for ULift
 
 -- Test with a universe polymporphic type parameter
 inductive Option' (α : Type u)
@@ -8,6 +10,32 @@ inductive Option' (α : Type u)
   | none
   deriving ToExpr
 
+/-- info: instToExprOption'OfToLevel -/
+#guard_msgs in #synth ToExpr (Option' Nat)
+/-- info: instToExprOption'OfToLevel -/
+#guard_msgs in #synth ToExpr (Option' <| ULift.{20} Nat)
+
+/--
+info: Lean.Expr.app
+  (Lean.Expr.app
+    (Lean.Expr.const `Option'.some [Lean.Level.succ (Lean.Level.succ (Lean.Level.succ (Lean.Level.zero)))])
+    (Lean.Expr.app
+      (Lean.Expr.const `ULift [Lean.Level.succ (Lean.Level.succ (Lean.Level.succ (Lean.Level.zero))), Lean.Level.zero])
+      (Lean.Expr.const `Nat [])))
+  (Lean.Expr.app
+    (Lean.Expr.app
+      (Lean.Expr.const
+        `ULift.up
+        [Lean.Level.succ (Lean.Level.succ (Lean.Level.succ (Lean.Level.zero))), Lean.Level.zero])
+      (Lean.Expr.const `Nat []))
+    (Lean.Expr.app
+      (Lean.Expr.app
+        (Lean.Expr.app (Lean.Expr.const `OfNat.ofNat [Lean.Level.zero]) (Lean.Expr.const `Nat []))
+        (Lean.Expr.lit (Lean.Literal.natVal 42)))
+      (Lean.Expr.app (Lean.Expr.const `instOfNatNat []) (Lean.Expr.lit (Lean.Literal.natVal 42)))))
+-/
+#guard_msgs in #eval toExpr (Option'.some <| ULift.up.{3} 42)
+
 -- Test with recursive type
 inductive List' (α : Type u)
   | cons (a : α) (as : List' α)
diff --git a/tests/lean/run/derivingToExpr.lean.out b/tests/lean/run/derivingToExpr.lean.out
new file mode 100644
index 000000000000..e69de29bb2d1

From 76aec16ea06582d4c75d6f5648859670e4dc44c0 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 11 Dec 2024 15:27:46 +0000
Subject: [PATCH 10/14] expand tests to include ambient and directly specified
 universes

---
 tests/lean/run/derivingToExpr.lean | 33 ++++++++++++++++++++++++++++--
 1 file changed, 31 insertions(+), 2 deletions(-)

diff --git a/tests/lean/run/derivingToExpr.lean b/tests/lean/run/derivingToExpr.lean
index c0880309a0a1..6c75c2dd9262 100644
--- a/tests/lean/run/derivingToExpr.lean
+++ b/tests/lean/run/derivingToExpr.lean
@@ -4,6 +4,16 @@ open Lean
 
 deriving instance ToExpr for ULift
 
+-- Test with empty type
+inductive Empty'
+  deriving ToExpr
+
+-- Test without universes
+inductive MonoOption' (α : Type) : Type
+  | some (a : α)
+  | none
+  deriving ToExpr
+
 -- Test with a universe polymporphic type parameter
 inductive Option' (α : Type u)
   | some (a : α)
@@ -42,9 +52,28 @@ inductive List' (α : Type u)
   | nil
   deriving ToExpr
 
--- Test without (universe) auto implicit
-set_option autoImplicit false in
+-- Tests without (universe) auto implicits
+section NoAutoImplicit
+set_option autoImplicit false
+
+-- Test with universe specified directly on the type
 inductive ExplicitList'.{u} (α : Type u)
   | cons (a : α) (as : List' α)
   | nil
   deriving ToExpr
+
+-- Test with ambient (explicit) universe
+universe u in
+inductive AmbientList' (α : Type u)
+  | cons (a : α) (as : List' α)
+  | nil
+  deriving ToExpr
+
+-- Now, test both ambient and directly specified universes
+universe u in
+structure ExplicitAmbientPair.{v} (α : Type u) (β : Type v) where
+  a : α
+  b : β
+  deriving ToExpr
+
+end NoAutoImplicit

From 2b87f3eef91d4fa75a98b9fe273030d1cee65305 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 11 Dec 2024 15:34:14 +0000
Subject: [PATCH 11/14] expand tests to exercise explicitly provided universes,
 even when autoImplicits are enabled

---
 tests/lean/run/derivingToExpr.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/tests/lean/run/derivingToExpr.lean b/tests/lean/run/derivingToExpr.lean
index 6c75c2dd9262..56102952edca 100644
--- a/tests/lean/run/derivingToExpr.lean
+++ b/tests/lean/run/derivingToExpr.lean
@@ -52,6 +52,24 @@ inductive List' (α : Type u)
   | nil
   deriving ToExpr
 
+inductive WithUniverse.{u} (α : Type u)
+  | foo (a : α)
+  deriving ToExpr
+
+universe u in
+inductive WithAmbientUniverse (α : Type u)
+  | foo (a : α)
+  deriving ToExpr
+
+-- A test with: an ambient universe `u`, a directly specified universe `v`, and
+-- an implicit universe `w`
+universe u
+structure WithAmbientUniverseTriple.{v} (α : Type u) (β : Type v) (y : Type w) where
+  a : α
+  b : β
+  c : γ
+  deriving ToExpr
+
 -- Tests without (universe) auto implicits
 section NoAutoImplicit
 set_option autoImplicit false

From 0e6c925d617cb802e01c886f3c1ec913770aa62f Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 11 Dec 2024 15:55:17 +0000
Subject: [PATCH 12/14] fix test by correctly scoping universe

---
 tests/lean/run/derivingToExpr.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/run/derivingToExpr.lean b/tests/lean/run/derivingToExpr.lean
index 56102952edca..237b52ba5de7 100644
--- a/tests/lean/run/derivingToExpr.lean
+++ b/tests/lean/run/derivingToExpr.lean
@@ -63,7 +63,7 @@ inductive WithAmbientUniverse (α : Type u)
 
 -- A test with: an ambient universe `u`, a directly specified universe `v`, and
 -- an implicit universe `w`
-universe u
+universe u in
 structure WithAmbientUniverseTriple.{v} (α : Type u) (β : Type v) (y : Type w) where
   a : α
   b : β

From b9807eea70252ddfa10dff22a6d45cc5e7bb0b48 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 11 Dec 2024 15:55:59 +0000
Subject: [PATCH 13/14] fix: only explicitly declare universe levels that are
 *not* already present in the ambient context

---
 src/Lean/Elab/Deriving/ToExpr.lean | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Deriving/ToExpr.lean b/src/Lean/Elab/Deriving/ToExpr.lean
index f7ab0181c3c1..309077576ecc 100644
--- a/src/Lean/Elab/Deriving/ToExpr.lean
+++ b/src/Lean/Elab/Deriving/ToExpr.lean
@@ -170,7 +170,8 @@ def mkAuxFunction (ctx : Deriving.Context) (i : Nat) : TermElabM Command := do
   let binders := header.binders.pop
     ++ (← mkToLevelBinders indVal)
     ++ #[← addLevels header.binders.back!]
-  let levels := indVal.levelParams.toArray.map mkIdent
+  let ambient ← Term.getLevelNames
+  let levels := indVal.levelParams.filter (· ∉ ambient) |>.toArray.map mkIdent
   if ctx.usePartial then
     `(private partial def $(mkIdent auxFunName):ident.{$levels,*} $binders:bracketedBinder* :
         Expr := $body:term)
@@ -203,7 +204,15 @@ def mkInstanceCmds (ctx : Deriving.Context) (typeNames : Array Name) :
       let indType      ← fixIndType indVal (← mkInductiveApp indVal argNames)
       let toTypeExpr   ← mkToTypeExpr argNames indVal
       let levels       := indVal.levelParams.toArray.map mkIdent
-      let instCmd ← `(instance $binders:implicitBinder* : ToExpr $indType where
+      let ambientLevels ← Term.getLevelNames
+      /- `defLevels` are the universes which are *not* globally specified (via a `universe` command)
+          and need to be declared for the instance -/
+      let defLevels    := levels.filter (·.getId ∉ ambientLevels)
+      trace[Elab.Deriving.toExpr] "ambient levels: {← Term.getLevelNames}"
+      trace[Elab.Deriving.toExpr] "levels: {levels}"
+      trace[Elab.Deriving.toExpr] "defLevels: {defLevels}"
+      let instCmd ← `(universe $defLevels:ident* in
+                      instance $binders:implicitBinder* : ToExpr $indType where
                         toExpr := $(mkIdent auxFunName).{$levels,*}
                         toTypeExpr := $toTypeExpr)
       instances := instances.push instCmd

From 467d63dbb3c9605e700089e2c57e9fcb74c4c23c Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 11 Dec 2024 17:41:25 +0000
Subject: [PATCH 14/14] "fix" test

Turns out I had a typo in the argument list. The problem was not with implicit universes, rather it was with implicit parameters.
Also adds new testcases to expose this bug properly
---
 tests/lean/run/derivingToExpr.lean | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/tests/lean/run/derivingToExpr.lean b/tests/lean/run/derivingToExpr.lean
index 237b52ba5de7..f9b71309d4b3 100644
--- a/tests/lean/run/derivingToExpr.lean
+++ b/tests/lean/run/derivingToExpr.lean
@@ -61,10 +61,11 @@ inductive WithAmbientUniverse (α : Type u)
   | foo (a : α)
   deriving ToExpr
 
+set_option trace.Elab.Deriving.toExpr true in
 -- A test with: an ambient universe `u`, a directly specified universe `v`, and
 -- an implicit universe `w`
 universe u in
-structure WithAmbientUniverseTriple.{v} (α : Type u) (β : Type v) (y : Type w) where
+structure WithAmbientUniverseTriple.{v} (α : Type u) (β : Type v) (γ : Type w) where
   a : α
   b : β
   c : γ
@@ -95,3 +96,14 @@ structure ExplicitAmbientPair.{v} (α : Type u) (β : Type v) where
   deriving ToExpr
 
 end NoAutoImplicit
+
+-- Test with an implicit parameter to the inductive type
+inductive ImplicitParameter
+  | foo (a : α)
+  deriving ToExpr
+
+-- Test where the type parameter is a variable, with an implicit universe
+variable {α : Type u} in
+inductive VariableParameter : Type
+  | foo (a : α)
+  deriving ToExpr