fix: make invalid use of 'partial' error more robust

src/Lean/Elab/PreDefinition/Main.lean

@@ -329,7 +329,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
         else if preDefs.any (·.modifiers.isPartial) then
           for preDef in preDefs do
             if preDef.modifiers.isPartial && !(← whnfD preDef.type).isForall then
-              withRef preDef.ref <| throwError "invalid use of 'partial', '{preDef.declName}' is not a function{indentExpr preDef.type}"
+              withRef preDef.ref <| throwError "invalid use of 'partial', '{preDef.declName}' is not a function"
           addAndCompilePartial preDefs
           preDefs.forM (·.termination.ensureNone "partial")
         else

tests/lean/697.lean.expected.out

@@ -1,2 +1 @@
 697.lean:24:12-24:19: error: invalid use of 'partial', 'pregion' is not a function
-  P Unit

tests/lean/sanitychecks.lean.expected.out

@@ -12,7 +12,6 @@ sanitychecks.lean:10:0-10:23: error: failed to synthesize
 
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 sanitychecks.lean:18:12-18:20: error: invalid use of 'partial', 'Foo.unsound3' is not a function
-  False
 sanitychecks.lean:20:0-20:54: error: failed to compile 'partial' definition 'Foo.unsound4', could not prove that the type
   ∀ (x : Unit), False
 is nonempty.

tests/lean/silent_failure.lean

@@ -0,0 +1,6 @@
+-- This was previously failing silently (but not adding `g` to the environment).
+
+#guard_msgs (drop info) in
+partial def g :
+  have : False := by apply?
+  False := g

tests/lean/silent_failure.lean.expected.out

@@ -0,0 +1 @@
+silent_failure.lean:4:12-4:13: error: invalid use of 'partial', 'g' is not a function