fix: avoid "unknown constant" error message for auxiliary declarations

src/Lean/Compiler/LCNF/Simp.lean

@@ -855,7 +855,7 @@ simplification opportunities by eta-expanding them.
 def etaPolyApp? (letDecl : LetDecl) : OptionT SimpM FunDecl := do
   guard <| (← read).config.etaPoly
   let .const declName _ := letDecl.value.getAppFn | failure
-  let info ← getConstInfo declName
+  let some info := (← getEnv).find? declName | failure
   guard <| hasLocalInst info.type
   guard <| !(← Meta.isInstance declName)
   let some decl ← getStage1Decl? declName | failure

src/Lean/Compiler/LCNF/Stage1.lean

@@ -37,7 +37,7 @@ def getStage1Decl? (declName : Name) : CoreM (Option Decl) := do
   match stage1Ext.getState (← getEnv) |>.decls.find? declName with
   | some decl => return decl
   | none =>
-    let info ← getConstInfo declName
+    let some info := (← getEnv).find? declName | return none
     if info.hasValue then
       let decls ← compileStage1 info.all.toArray
       return decls.find? fun decl => declName == decl.name