From 2058b96ab1e9cfb214ba8cfd1a06f1ea9950c4df Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 14 Jun 2024 15:37:47 +0200
Subject: [PATCH] Fix lens derivation with multiple universe levels

---
 Leanses/Lens.lean     |  3 ++-
 LeansesTest/Lens.lean | 10 ++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/Leanses/Lens.lean b/Leanses/Lens.lean
index 589ce44..8be58fd 100644
--- a/Leanses/Lens.lean
+++ b/Leanses/Lens.lean
@@ -234,7 +234,8 @@ open Lean Meta PrettyPrinter Delaborator SubExpr Core in
 @[command_elab mkLens] def mkLensHandler : CommandElab
   | `(mklenses $i) => do
     let name ← resolveGlobalConstNoOverload i
-    let structureType ← liftTermElabM <| liftMetaM <| inferType (Expr.const name [])
+    let nameInst ← liftTermElabM <| liftMetaM <| mkConstWithFreshMVarLevels name
+    let structureType ← liftTermElabM <| liftMetaM <| inferType nameInst
     let names : TSyntaxArray `ident ← liftCoreM <| generateFreshNames structureType
     let numArgs := structureType.getForallBinderNames.length
     trace[debug] "{numArgs}"
diff --git a/LeansesTest/Lens.lean b/LeansesTest/Lens.lean
index ab4d0cf..4bd7756 100644
--- a/LeansesTest/Lens.lean
+++ b/LeansesTest/Lens.lean
@@ -76,3 +76,13 @@ namespace LeansesTest.Lens.Test2
 -- #eval ((gset set_Fin 1 (fun (x:Fin 5) => if x == 2 then 3 else 4))) ^.. traverse_Fin
 
 end LeansesTest.Lens.Test2
+
+namespace LeansesTest.Lens.Test3
+
+structure SubEx (α: Type _) where
+  c : List α
+  deriving Repr
+
+mklenses SubEx
+
+end LeansesTest.Lens.Test3