From 83775b08cbccb18b060d683d5297e8aff54048a8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 5 Feb 2021 15:14:12 -0800
Subject: [PATCH] fix: `whnfCore` not expanding delayed assignments

---
 src/Lean/Meta/WHNF.lean                  | 27 ++++++++++++++++++++++++
 tests/lean/run/whnfDelayedMVarIssue.lean | 10 +++++++++
 2 files changed, 37 insertions(+)
 create mode 100644 tests/lean/run/whnfDelayedMVarIssue.lean

diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 3f68279279..afbc36ed5c 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -307,6 +307,31 @@ def reduceProj? (e : Expr) : MetaM (Option Expr) := do
   | Expr.proj _ i c _ => project? c i
   | _                 => return none
 
+/-
+  Auxiliary method for reducing terms of the form `?m t_1 ... t_n` where `?m` is delayed assigned.
+  Recall that we can only expand a delayed assignment when all holes/metavariables in the assigned value have been "filled".
+-/
+private def whnfDelayedAssigned? (f' : Expr) (e : Expr) : MetaM (Option Expr) := do
+  if f'.isMVar then
+    match (← getDelayedAssignment? f'.mvarId!) with
+    | none => return none
+    | some { fvars := fvars, val := val, .. } =>
+      let args := e.getAppArgs
+      if fvars.size > args.size then
+        -- Insufficient number of argument to expand delayed assignment
+        return none
+      else
+        let newVal ← instantiateMVars val
+        if newVal.hasExprMVar then
+           -- Delayed assignment still contains metavariables
+           return none
+        else
+           let newVal := newVal.abstract fvars
+           let result := newVal.instantiateRevRange 0 fvars.size args
+           return mkAppRange result fvars.size args.size args
+  else
+    return none
+
 /--
   Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
   expand let-expressions, expand assigned meta-variables. -/
@@ -322,6 +347,8 @@ partial def whnfCore (e : Expr) : MetaM Expr :=
       if f'.isLambda then
         let revArgs := e.getAppRevArgs
         whnfCore <| f'.betaRev revArgs
+      else if let some eNew ← whnfDelayedAssigned? f' e then
+        whnfCore eNew
       else
         let e := if f == f' then e else e.updateFn f'
         match (← reduceMatcher? e) with
diff --git a/tests/lean/run/whnfDelayedMVarIssue.lean b/tests/lean/run/whnfDelayedMVarIssue.lean
new file mode 100644
index 0000000000..76efdb0389
--- /dev/null
+++ b/tests/lean/run/whnfDelayedMVarIssue.lean
@@ -0,0 +1,10 @@
+def Nat.isZero (n : Nat) :=
+  n == 0
+
+def test (preDefs : Array (Array Nat)) : IO Unit := do
+  for preDefs in preDefs do
+    let preDef := preDefs[0]
+    if preDef.isZero then
+      pure ()
+    else
+      IO.println "error"