From 5fbe63cca409bdff2a98a1eed60f9a2f548853ed Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 18 Sep 2022 15:29:41 -0700
Subject: [PATCH] fix: process remaining params

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

diff --git a/src/Lean/Compiler/LCNF/Specialize.lean b/src/Lean/Compiler/LCNF/Specialize.lean
index ea4e22feb5..98d67b665c 100644
--- a/src/Lean/Compiler/LCNF/Specialize.lean
+++ b/src/Lean/Compiler/LCNF/Specialize.lean
@@ -307,6 +307,9 @@ where
         -- Keep the parameter
         let param := { param with type := param.type.instantiateLevelParams decl.levelParams us }
         params := params.push (← internalizeParam param)
+    for param in decl.params[argMask.size:] do
+      let param := { param with type := param.type.instantiateLevelParams decl.levelParams us }
+      params := params.push (← internalizeParam param)
     let value := decl.instantiateValueLevelParams us
     let value ← internalizeCode value
     let value := attachCodeDecls decls value