Fix lens derivation with multiple universe levels

VCA-EPFL · Jun 14, 2024 · 2058b96 · 2058b96
1 parent cb0ae47
commit 2058b96
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 1 deletion.
diff --git 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
@@ -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