From cf313d210194acdfdece0089734118a78b9b6a7b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Oct 2022 16:42:27 -0700 Subject: [PATCH] chore: improve `eqvTypes` --- src/Lean/Compiler/LCNF/InferType.lean | 3 +++ src/Lean/Compiler/LCNF/Passes.lean | 1 + src/Lean/Compiler/LCNF/Simp/InlineProj.lean | 2 +- 3 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/InferType.lean b/src/Lean/Compiler/LCNF/InferType.lean index d79281fdec..4af5b59892 100644 --- a/src/Lean/Compiler/LCNF/InferType.lean +++ b/src/Lean/Compiler/LCNF/InferType.lean @@ -416,6 +416,9 @@ We have that `List Nat` and `List ◾` are compatible types, but they are not eq partial def eqvTypes (a b : Expr) : Bool := if a == b then true + else if a.isErased && b.isErased then + -- `◾ α` is equivalent to `◾` + true else let a' := a.headBeta let b' := b.headBeta diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean index a2bee15035..e054637d6b 100644 --- a/src/Lean/Compiler/LCNF/Passes.lean +++ b/src/Lean/Compiler/LCNF/Passes.lean @@ -113,5 +113,6 @@ builtin_initialize builtin_initialize registerTraceClass `Compiler.saveBase (inherited := true) + registerTraceClass `Compiler.trace (inherited := true) end Lean.Compiler.LCNF diff --git a/src/Lean/Compiler/LCNF/Simp/InlineProj.lean b/src/Lean/Compiler/LCNF/Simp/InlineProj.lean index 5426b31423..1a91747209 100644 --- a/src/Lean/Compiler/LCNF/Simp/InlineProj.lean +++ b/src/Lean/Compiler/LCNF/Simp/InlineProj.lean @@ -43,7 +43,7 @@ partial def inlineProjInst? (e : Expr) (expectedType : Expr) : SimpM (Option (Ar let (fvarId?, decls) ← visit s [i] |>.run |>.run #[] if let some fvarId := fvarId? then let type ← getType fvarId - if type.isErased || eqvTypes expectedType type then + if expectedType.isErased || type.isErased || eqvTypes expectedType type then return some (decls, fvarId) else let cast ← mkLcCast (.fvar fvarId) expectedType