From 72d3840f0c3bcc3be83000307fe10d92abbd9443 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 9 Oct 2022 18:07:54 -0700
Subject: [PATCH] feat: add `simpCast?`

---
 src/Lean/Compiler/LCNF/Simp/Main.lean      |  2 +-
 src/Lean/Compiler/LCNF/Simp/SimpValue.lean | 20 ++++++++++++++++++--
 2 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/Simp/Main.lean b/src/Lean/Compiler/LCNF/Simp/Main.lean
index a7b401f4d2..ddad526813 100644
--- a/src/Lean/Compiler/LCNF/Simp/Main.lean
+++ b/src/Lean/Compiler/LCNF/Simp/Main.lean
@@ -265,7 +265,7 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
   match code with
   | .let decl k =>
     let mut decl ← normLetDecl decl
-    if let some value ← simpValue? decl.value then
+    if let some value ← simpValue? decl.value decl.type then
       markSimplified
       decl ← decl.updateValue value
     if let some decls ← ConstantFold.foldConstants decl then
diff --git a/src/Lean/Compiler/LCNF/Simp/SimpValue.lean b/src/Lean/Compiler/LCNF/Simp/SimpValue.lean
index cc632d1fb5..10e5a0db93 100644
--- a/src/Lean/Compiler/LCNF/Simp/SimpValue.lean
+++ b/src/Lean/Compiler/LCNF/Simp/SimpValue.lean
@@ -110,7 +110,23 @@ def applyImplementedBy? (e : Expr) : OptionT SimpM Expr := do
   let some declNameNew := getImplementedBy? (← getEnv) declName | failure
   return mkAppN (.const declNameNew us) e.getAppArgs
 
+/--
+```
+let _x : A := lcCast _ _ a
+```
+=> if `A` and type of `a` are equivalent
+```
+let _x : B := a
+```
+-/
+def simpCast? (e : Expr) (expectedType : Expr) : OptionT SimpM Expr := do
+  guard <| e.isAppOfArity ``lcCast 3
+  let a := e.appArg!
+  let type ← inferType a
+  guard <| type.isErased || eqvTypes expectedType type
+  return a
+
 /-- Try to apply simple simplifications. -/
-def simpValue? (e : Expr) : SimpM (Option Expr) :=
+def simpValue? (e : Expr) (expectedType : Expr) : SimpM (Option Expr) :=
   -- TODO: more simplifications
-  simpProj? e <|> simpAppApp? e <|> simpCtorDiscr? e <|> applyImplementedBy? e <|> simpCastCast? e
+  simpProj? e <|> simpAppApp? e <|> simpCtorDiscr? e <|> applyImplementedBy? e <|> simpCastCast? e <|> simpCast? e expectedType