From 993ec54db68217e6ef8be1eace2cdf509d36e7ad Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 15 Feb 2022 12:17:40 -0800
Subject: [PATCH] chore: avoid hack that may introduce unnecessary dependencies

---
 src/Lean/Elab/Match.lean          | 3 +--
 src/Lean/Meta/GeneralizeVars.lean | 8 ++++----
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 19ae5e1783..d7a3d757e7 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -600,9 +600,8 @@ private def generalize (discrs : Array Expr) (matchType : Expr) (altViews : Arra
   if !gen then
     return (discrs, matchType, altViews, false)
   else
-    let ysFVarIds ← getFVarsToGeneralize discrs
     /- let-decls are currently being ignored by the generalizer. -/
-    let ysFVarIds ← ysFVarIds.filterM fun fvarId => return !(← getLocalDecl fvarId).isLet
+    let ysFVarIds ← getFVarsToGeneralize discrs (ignoreLetDecls := true)
     if ysFVarIds.isEmpty then
       return (discrs, matchType, altViews, false)
     else
diff --git a/src/Lean/Meta/GeneralizeVars.lean b/src/Lean/Meta/GeneralizeVars.lean
index 4ee1322c6c..23e7b9d1b2 100644
--- a/src/Lean/Meta/GeneralizeVars.lean
+++ b/src/Lean/Meta/GeneralizeVars.lean
@@ -54,20 +54,20 @@ where
   Remark: we *not* collect instance implicit arguments nor auxiliary declarations for compiling
   recursive declarations.
 -/
-def getFVarSetToGeneralize (targets : Array Expr) (forbidden : FVarIdSet) : MetaM FVarIdSet := do
+def getFVarSetToGeneralize (targets : Array Expr) (forbidden : FVarIdSet) (ignoreLetDecls := false) : MetaM FVarIdSet := do
   let mut s : FVarIdSet := targets.foldl (init := {}) fun s target => if target.isFVar then s.insert target.fvarId! else s
   let mut r : FVarIdSet := {}
   for localDecl in (← getLCtx) do
     unless forbidden.contains localDecl.fvarId do
-      unless localDecl.isAuxDecl || localDecl.binderInfo.isInstImplicit do
+      unless localDecl.isAuxDecl || localDecl.binderInfo.isInstImplicit || (ignoreLetDecls && localDecl.isLet) do
       if (← getMCtx).findLocalDeclDependsOn localDecl fun fvarId => s.contains fvarId then
         r := r.insert localDecl.fvarId
         s := s.insert localDecl.fvarId
   return r
 
-def getFVarsToGeneralize (targets : Array Expr) (forbidden : FVarIdSet := {}) : MetaM (Array FVarId) := do
+def getFVarsToGeneralize (targets : Array Expr) (forbidden : FVarIdSet := {}) (ignoreLetDecls := false) : MetaM (Array FVarId) := do
   let forbidden ← mkGeneralizationForbiddenSet targets forbidden
-  let s ← getFVarSetToGeneralize targets forbidden
+  let s ← getFVarSetToGeneralize targets forbidden ignoreLetDecls
   sortFVarIds s.toArray
 
 end Lean.Meta