From c33b5b6588bf00aa75c8981efcbc7d4c8fad41f5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 13 Oct 2022 06:08:51 -0700
Subject: [PATCH] chore: remove unnecessary `eqvTypes`

---
 src/Lean/Compiler/LCNF/Simp/Main.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/Simp/Main.lean b/src/Lean/Compiler/LCNF/Simp/Main.lean
index c9753b4154..322e9c7c18 100644
--- a/src/Lean/Compiler/LCNF/Simp/Main.lean
+++ b/src/Lean/Compiler/LCNF/Simp/Main.lean
@@ -96,10 +96,8 @@ def isReturnOf (c : Code) (fvarId : FVarId) : SimpM Bool := do
   | .return fvarId' => return (← normFVar fvarId') == fvarId
   | _ => return false
 
-def elimVar? (value : Expr) (expectedType : Expr) : SimpM (Option FVarId) := do
+def elimVar? (value : Expr) : SimpM (Option FVarId) := do
   let .fvar fvarId := value | return none
-  let type ← getType fvarId
-  unless type.isErased || eqvTypes type expectedType do return none
   return fvarId
 
 mutual
@@ -225,7 +223,7 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
       attachCodeDecls decls k
     else if let some funDecl ← etaPolyApp? decl then
       simp (.fun funDecl k)
-    else if let some fvarId ← elimVar? decl.value decl.type then
+    else if let some fvarId ← elimVar? decl.value then
       /- Eliminate `let _x_i := _x_j;` -/
       addFVarSubst decl.fvarId fvarId
       eraseLetDecl decl