diff --git a/src/Lean/Compiler/LCNF/Specialize.lean b/src/Lean/Compiler/LCNF/Specialize.lean
index 00404b92c5..30ea5a4127 100644
--- a/src/Lean/Compiler/LCNF/Specialize.lean
+++ b/src/Lean/Compiler/LCNF/Specialize.lean
@@ -261,6 +261,9 @@ def getRemainingArgs (paramsInfo : Array SpecParamInfo) (args : Array Arg) : Arr
       result := result.push arg
   return result ++ args[paramsInfo.size:]
 
+def paramsToVarSet (params : Array Param) : FVarIdSet :=
+  params.foldl (fun r p => r.insert p.fvarId) {}
+
 mutual
   /--
   Try to specialize the function application in the given let-declaration.
@@ -295,7 +298,8 @@ mutual
       specDecl.saveBase
       let specDecl ← specDecl.simp {}
       let specDecl ← specDecl.simp { etaPoly := true, inlinePartial := true, implementedBy := true }
-      let value ← withReader (fun _ => { declName := specDecl.name }) do
+      let ground := paramsToVarSet specDecl.params
+      let value ← withReader (fun _ => { declName := specDecl.name, ground }) do
          withParams specDecl.params <| specDecl.value.mapCodeM visitCode
       let specDecl := { specDecl with value }
       modify fun s => { s with decls := s.decls.push specDecl }
@@ -337,7 +341,8 @@ def main (decl : Decl) : SpecializeM Decl := do
 end Specialize
 
 partial def Decl.specialize (decl : Decl) : CompilerM (Array Decl) := do
-  let (decl, s) ← Specialize.main decl |>.run { declName := decl.name } |>.run {}
+  let ground := Specialize.paramsToVarSet decl.params
+  let (decl, s) ← Specialize.main decl |>.run { declName := decl.name, ground } |>.run {}
   return s.decls.push decl
 
 def specialize : Pass where