From e8246e026dc39b4b99be011379a852e61fdc729e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Sep 2022 15:57:12 -0700 Subject: [PATCH] fix: bug at `compatibleTypes` Many thanks to @hargoniX --- src/Lean/Compiler/LCNF/Types.lean | 8 +++++--- tests/lean/run/compatibleTypesBugAtLCNF.lean | 3 +++ 2 files changed, 8 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/compatibleTypesBugAtLCNF.lean diff --git a/src/Lean/Compiler/LCNF/Types.lean b/src/Lean/Compiler/LCNF/Types.lean index 97e51bca5e..3593967f6b 100644 --- a/src/Lean/Compiler/LCNF/Types.lean +++ b/src/Lean/Compiler/LCNF/Types.lean @@ -201,9 +201,11 @@ partial def compatibleTypes (a b : Expr) : Bool := if a.isAnyType || b.isAnyType then true else - let a := a.headBeta - let b := b.headBeta - if a == b then + let a' := a.headBeta + let b' := b.headBeta + if a != a' || b != b' then + compatibleTypes a' b' + else if a == b then true else match a, b with diff --git a/tests/lean/run/compatibleTypesBugAtLCNF.lean b/tests/lean/run/compatibleTypesBugAtLCNF.lean new file mode 100644 index 0000000000..203c01b569 --- /dev/null +++ b/tests/lean/run/compatibleTypesBugAtLCNF.lean @@ -0,0 +1,3 @@ +import Lean + +#eval Lean.Compiler.compile #[``Lean.Compiler.LCNF.Simp.etaPolyApp?]