From 096a6fd4fb458ca16c66f17d096ebfedd921a640 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Sep 2022 13:57:14 -0700 Subject: [PATCH] fix: use `eta` at `compatibleTypes` --- src/Lean/Compiler/LCNF/Types.lean | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/Lean/Compiler/LCNF/Types.lean b/src/Lean/Compiler/LCNF/Types.lean index 3563d9eb1b..c9da2aec22 100644 --- a/src/Lean/Compiler/LCNF/Types.lean +++ b/src/Lean/Compiler/LCNF/Types.lean @@ -130,7 +130,7 @@ Convert a Lean type into a LCNF type used by the code generator. partial def toLCNFType (type : Expr) : MetaM Expr := do if (← isProp type) then return erasedExpr - let type ← whnf type + let type ← whnfEta type match type with | .sort u => return .sort u | .const .. => visitApp type #[] @@ -141,12 +141,20 @@ partial def toLCNFType (type : Expr) : MetaM Expr := do if b.isAnyType || b.isErased then return b else - return (Expr.lam n d (b.abstract #[x]) bi).eta + return Expr.lam n d (b.abstract #[x]) bi | .forallE .. => visitForall type #[] | .app .. => type.withApp visitApp | .fvar .. => visitApp type #[] | _ => return anyTypeExpr where + whnfEta (type : Expr) : MetaM Expr := do + let type ← whnf type + let type' := type.eta + if type' != type then + whnfEta type' + else + return type + visitForall (e : Expr) (xs : Array Expr) : MetaM Expr := do match e with | .forallE n d b bi =>