From 0bbaf161be552e1efe0cb2064f05e74e93e7d490 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 24 Jul 2020 11:37:03 -0700
Subject: [PATCH] fix: metavariable assignments were being ignored

---
 src/Lean/Util/Closure.lean | 29 ++++++++++++++++++-----------
 1 file changed, 18 insertions(+), 11 deletions(-)

diff --git a/src/Lean/Util/Closure.lean b/src/Lean/Util/Closure.lean
index 9fc003aa2c..70d4dcb6f6 100644
--- a/src/Lean/Util/Closure.lean
+++ b/src/Lean/Util/Closure.lean
@@ -48,12 +48,16 @@ modify $ fun s => { s with levelParams := s.levelParams.push p, nextLevelIdx :=
 pure $ mkLevelParam p
 
 partial def collectLevelAux : Level → ClosureM Level
-| u@(Level.succ v _)   => do v ← visitLevel collectLevelAux v; pure $ u.updateSucc! v
-| u@(Level.max v w _)  => do v ← visitLevel collectLevelAux v; w ← visitLevel collectLevelAux w; pure $ u.updateMax! v w
-| u@(Level.imax v w _) => do v ← visitLevel collectLevelAux v; w ← visitLevel collectLevelAux w; pure $ u.updateIMax! v w
-| u@(Level.mvar _ _)   => mkNewLevelParam u
-| u@(Level.param _ _)  => mkNewLevelParam u
-| u@(Level.zero _)     => pure u
+| u@(Level.succ v _)      => do v ← visitLevel collectLevelAux v; pure $ u.updateSucc! v
+| u@(Level.max v w _)     => do v ← visitLevel collectLevelAux v; w ← visitLevel collectLevelAux w; pure $ u.updateMax! v w
+| u@(Level.imax v w _)    => do v ← visitLevel collectLevelAux v; w ← visitLevel collectLevelAux w; pure $ u.updateIMax! v w
+| u@(Level.mvar mvarId _) => do
+  ctx ← read;
+  match ctx.mctx.getLevelAssignment? mvarId with
+  | none   => mkNewLevelParam u
+  | some v => visitLevel collectLevelAux v
+| u@(Level.param _ _)     => mkNewLevelParam u
+| u@(Level.zero _)        => pure u
 
 def collectLevel (u : Level) : ClosureM Level :=
 visitLevel collectLevelAux u
@@ -117,11 +121,14 @@ partial def collectExprAux : Expr → ClosureM Expr
     ctx ← read;
     match ctx.mctx.findDecl? mvarId with
     | none          => throw "unknown metavariable"
-    | some mvarDecl => do
-      type ← collect mvarDecl.type;
-      x    ← mkLocalDecl none type;
-      modify $ fun s => { s with exprClosure := s.exprClosure.push e };
-      pure x
+    | some mvarDecl =>
+      match ctx.mctx.getExprAssignment? mvarId with
+      | some v => collect v
+      | none   => do
+        type ← collect mvarDecl.type;
+        x    ← mkLocalDecl none type;
+        modify $ fun s => { s with exprClosure := s.exprClosure.push e };
+        pure x
   | Expr.fvar fvarId _ => do
     ctx ← read;
     match ctx.lctxInput.find? fvarId with