From 796e9e3bdd1e4d09efce2d105d201165ec33ae80 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 18 Sep 2022 13:21:55 -0700
Subject: [PATCH] feat: eta expand at `specializeApp?`

---
 src/Lean/Compiler/LCNF/Specialize.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Compiler/LCNF/Specialize.lean b/src/Lean/Compiler/LCNF/Specialize.lean
index 8227df00db..e584cf6c70 100644
--- a/src/Lean/Compiler/LCNF/Specialize.lean
+++ b/src/Lean/Compiler/LCNF/Specialize.lean
@@ -318,6 +318,7 @@ mutual
     trace[Compiler.specialize.candidate] "params: {params.map fun p => p.binderName}"
     -- TODO: create cache and check cached results, apply `visitCode` to `specDecl`, return new application
     let specDecl ← mkSpecDecl decl us paramsInfo params decls args
+    let specDecl ← specDecl.etaExpand
     let specDecl ← specDecl.simp {} -- TODO: `simp` config
     modify fun s => { s with decls := s.decls.push specDecl }
     return none