From 827ef9448650de1dbd48d6606fe82f7a22ee2733 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 9 Oct 2022 08:53:24 -0700
Subject: [PATCH] feat: add `eqvTypes`

---
 src/Lean/Compiler/LCNF/InferType.lean | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/src/Lean/Compiler/LCNF/InferType.lean b/src/Lean/Compiler/LCNF/InferType.lean
index 30d0221809..d79281fdec 100644
--- a/src/Lean/Compiler/LCNF/InferType.lean
+++ b/src/Lean/Compiler/LCNF/InferType.lean
@@ -407,4 +407,29 @@ def compatibleTypes (a b : Expr) : CompilerM Bool :=
   else
     InferType.compatibleTypesFull a b |>.run {}
 
+/--
+Return `true` if the given LCNF are equivalent.
+Remark: `eqvTypes a b` implies `compatibleTypes`, but the reverse direction is not true.
+We have that `List Nat` and `List ◾` are compatible types, but they are not equivalent.
+`List Nat` and `(fun x => List x) Nat` are both equivalent and compatible types.
+-/
+partial def eqvTypes (a b : Expr) : Bool :=
+  if a == b then
+    true
+  else
+    let a' := a.headBeta
+    let b' := b.headBeta
+    if a != a' || b != b' then
+      eqvTypes a' b'
+    else
+      match a, b with
+      | .mdata _ a, b => eqvTypes a b
+      | a, .mdata _ b => eqvTypes a b
+      | .app f a, .app g b => eqvTypes f g && eqvTypes a b
+      | .forallE _ d₁ b₁ _, .forallE _ d₂ b₂ _ => eqvTypes d₁ d₂ && eqvTypes b₁ b₂
+      | .lam _ d₁ b₁ _, .lam _ d₂ b₂ _ => eqvTypes d₁ d₂ && eqvTypes b₁ b₂
+      | .sort u, .sort v => Level.isEquiv u v
+      | .const n us, .const m vs => n == m && List.isEqv us vs Level.isEquiv
+      | _, _ => false
+
 end Lean.Compiler.LCNF