From 9ea099827fd380a10f5dbbba81809ef9b7141ebf Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 29 Mar 2025 14:39:42 -0700
Subject: [PATCH] fix(env): Adding declarations with universe levels

---
 Pantograph/Environment.lean |  8 +++++---
 Test/Integration.lean       | 19 ++++++++++++++++++-
 2 files changed, 23 insertions(+), 4 deletions(-)

diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index e18da61..d7bac21 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -148,7 +148,9 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.
 def addDecl (name: String) (levels: Array String := #[]) (type: String) (value: String) (isTheorem: Bool)
     : Protocol.FallibleT CoreM Protocol.EnvAddResult := do
   let env ← Lean.MonadEnv.getEnv
-  let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
+  let levelParams := levels.toList.map (·.toName)
+  let tvM: Elab.TermElabM (Except String (Expr × Expr)) :=
+    Elab.Term.withLevelNames levelParams do do
     let type ← match parseTerm env type with
       | .ok syn => do
         match ← elabTerm syn with
@@ -164,11 +166,11 @@ def addDecl (name: String) (levels: Array String := #[]) (type: String) (value:
           pure $ expr
         catch ex => return .error (← ex.toMessageData.toString)
       | .error e => return .error e
-    pure $ .ok (type, value)
+    Elab.Term.synthesizeSyntheticMVarsNoPostponing
+    pure $ .ok (← instantiateMVars type, ← instantiateMVars value)
   let (type, value) ← match ← tvM.run' (ctx := {}) |>.run' with
     | .ok t => pure t
     | .error e => Protocol.throw $ Protocol.errorExpr e
-  let levelParams := levels.toList.map (·.toName)
   let decl := if isTheorem then
     Lean.Declaration.thmDecl <| Lean.mkTheoremValEx
       (name := name.toName)
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 013554b..4778f0a 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -162,6 +162,7 @@ def test_automatic_mode (automatic: Bool): Test :=
 def test_env_add_inspect : Test :=
   let name1 := "Pantograph.mystery"
   let name2 := "Pantograph.mystery2"
+  let name3 := "Pantograph.mystery3"
   [
     step "env.add"
       ({
@@ -190,9 +191,25 @@ def test_env_add_inspect : Test :=
        value? := .some { pp? := .some "fun a => ↑a + 1" },
        type := { pp? := .some "Nat → Int" },
      }:
-      Protocol.EnvInspectResult)
+      Protocol.EnvInspectResult),
+    step "env.add"
+      ({
+        name := name3,
+        levels := #["u"]
+        type := "(α : Type u) → α → (α × α)",
+        value := "λ (α : Type u) (x : α) => (x, x)",
+        isTheorem := false
+      }: Protocol.EnvAdd)
+     ({}: Protocol.EnvAddResult),
+    step "env.inspect" ({name := name3} : Protocol.EnvInspect)
+     ({
+       type := { pp? := .some "(α : Type u) → α → α × α" },
+     }:
+      Protocol.EnvInspectResult),
   ]
 
+def f.{u} : (α : Type u) → α → (α × α) := λ (α : Type u) (x : α) => (x, x)
+
 example : ∀ (p: Prop), p → p := by
   intro p h
   exact h