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