fix: bug at reduceRec

src/Lean/Meta/WHNF.lean

@@ -49,9 +49,9 @@ private def getFirstCtor (d : Name) : MetaM (Option Name) := do
   let some (ConstantInfo.inductInfo { ctors := ctor::_, ..}) ← getConstNoEx? d | pure none
   return some ctor
 
-private def mkNullaryCtor (type : Expr) (nparams : Nat) : MetaM (Option Expr) :=
+private def mkNullaryCtor (type : Expr) (nparams : Nat) : MetaM (Option Expr) := do
   match type.getAppFn with
-  | Expr.const d lvls _ => do
+  | Expr.const d lvls _ =>
     let (some ctor) ← getFirstCtor d | pure none
     return mkAppN (mkConst ctor lvls) (type.getAppArgs.shrink nparams)
   | _ =>
@@ -72,7 +72,7 @@ private def getRecRuleFor (recVal : RecursorVal) (major : Expr) : Option Recurso
 
 private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM (Option Expr) := do
   let majorType ← inferType major
-  let majorType ← whnf majorType
+  let majorType ← instantiateMVars (← whnf majorType)
   let majorTypeI := majorType.getAppFn
   if !majorTypeI.isConstOf recVal.getInduct then
     return none

tests/lean/run/reductionBug.lean

@@ -0,0 +1,19 @@
+abbrev VName := String
+
+inductive Ty where
+  | Bool
+  | Int
+
+def Ctxt := VName → Option Ty
+
+variable (Γ : Ctxt) in
+inductive Expr : Ty → Type where
+  | var (h : Γ x = some τ) : Expr τ
+
+def Expr.constFold : Expr Γ τ → Option Unit
+  | var n   => none
+
+theorem Expr.constFold_sound {e : Expr Γ τ} : constFold e = some v → True := by
+  intro h
+  induction e with
+  | var   => simp only [constFold] at h