fix: avoid "failed to evaluate" error when extension has sorry

See updated test output.

src/Lean/KeyedDeclsAttribute.lean

@@ -7,6 +7,7 @@ import Lean.Attributes
 import Lean.Compiler.InitAttr
 import Lean.ToExpr
 import Lean.ScopedEnvExtension
+import Lean.Compiler.IR.CompilerM
 
 /-!
 A builder for attributes that are applied to declarations of a common type and
@@ -129,8 +130,13 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDe
     descr           := df.descr
     add             := fun constName stx attrKind => do
       let key ← df.evalKey false stx
-      let val ← evalConstCheck γ df.valueTypeName constName
-      ext.add { key := key, decl := constName, value := val } attrKind
+      match IR.getSorryDep (← getEnv) constName with
+      | none =>
+        let val ← evalConstCheck γ df.valueTypeName constName
+        ext.add { key := key, decl := constName, value := val } attrKind
+      | _ =>
+        -- If the declaration contains `sorry`, we skip `evalConstCheck` to avoid unnecessary bizarre error message
+        pure ()
     applicationTime := AttributeApplicationTime.afterCompilation
   }
   pure { defn := df, tableRef := tableRef, ext := ext }

tests/lean/435.lean.expected.out

@@ -1,3 +1,2 @@
 435.lean:3:37-3:42: warning: declaration uses 'sorry'
 435.lean:5:21-5:23: error: unknown identifier 'op' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.
-435.lean:5:0-5:23: error: cannot evaluate code because it uses 'sorry' and/or contains errors

tests/lean/notationPrecheck.lean.expected.out

@@ -1,8 +1,6 @@
 notationPrecheck.lean:1:25-1:26: error: unknown identifier 'a' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.
-notationPrecheck.lean:1:0-1:26: error: cannot evaluate code because it uses 'sorry' and/or contains errors
 notationPrecheck.lean:4:16-4:19: error: no macro or `[quotPrecheck]` instance for syntax kind 'termB_' found
   b x
 This means we cannot eagerly check your notation/quotation for unbound identifiers; you can use `set_option quotPrecheck false` to disable this check.
-notationPrecheck.lean:4:0-4:19: error: cannot evaluate code because it uses 'sorry' and/or contains errors
 notationPrecheck.lean:8:7-8:8: error: elaboration function for 'termB_' has not been implemented
   b x✝