fix: improve error message for partial inhabitation and add delta deriving (#5780)

Example new output:
```text
failed to compile 'partial' definition 'checkMyList', could not prove that the type
  ListNode → Bool × ListNode
is nonempty.

This process uses multiple strategies:
- It looks for a parameter that matches the return type.
- It tries synthesizing 'Inhabited' and 'Nonempty' instances for the return type.
- It tries unfolding the return type.

If the return type is defined using the 'structure' or 'inductive' command, you can try
adding a 'deriving Nonempty' clause to it.
```
The inhabitation prover now also unfolds definitions when trying to
prove inhabitation. For example,
```lean
def T (α : Type) := α × α

partial def f (n : Nat) : T Nat := f n
```

Motivated [by
Zulip](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Why.20return.20type.20of.20partial.20function.20MUST.20.60inhabited.60.3F/near/477905312)

src/Lean/Elab/PreDefinition/MkInhabitant.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.AppBuilder
+import Lean.PrettyPrinter
 namespace Lean.Elab
 open Meta
 
@@ -31,22 +32,41 @@ private def mkFnInhabitant? (xs : Array Expr) (type : Expr) (useOfNonempty : Boo
       | some val => return some (← mkLambdaFVars xs[0:i] val)
   loop xs.size type
 
+/--
+Find an inhabitant while doing delta unfolding.
+-/
+private partial def mkInhabitantForAux? (xs : Array Expr) (type : Expr) (useOfNonempty : Bool) : MetaM (Option Expr) := withIncRecDepth do
+  if let some val ← mkInhabitant? type useOfNonempty <||> findAssumption? xs type then
+    mkLambdaFVars xs val
+  else if let some val ← mkFnInhabitant? xs type useOfNonempty then
+    return val
+  else
+    let type ← whnfCore type
+    if type.isForall then
+      forallTelescope type fun xs' type' => do
+        mkInhabitantForAux? (xs ++ xs') type' useOfNonempty
+    else if let some type' ← unfoldDefinition? type then
+      mkInhabitantForAux? xs type' useOfNonempty
+    else
+      return none
+
 /- TODO: add a global IO.Ref to let users customize/extend this procedure -/
 def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr := do
-  let go? (useOfNonempty : Bool) : MetaM (Option Expr) := do
-    match (← mkInhabitant? type useOfNonempty) with
-    | some val => mkLambdaFVars xs val
-    | none     =>
-    match (← findAssumption? xs type) with
-    | some x => mkLambdaFVars xs x
-    | none   =>
-    match (← mkFnInhabitant? xs type useOfNonempty) with
-    | some val => return val
-    | none     => return none
-  match (← go? false) with
-  | some val => return val
-  | none     => match (← go? true) with
-    | some val => return val
-    | none     => throwError "failed to compile partial definition '{declName}', failed to show that type is inhabited and non empty"
+  if let some val ← mkInhabitantForAux? xs type false <||> mkInhabitantForAux? xs type true then
+    return val
+  else
+    throwError "\
+      failed to compile 'partial' definition '{declName}', could not prove that the type\
+      {indentExpr (← mkForallFVars xs type)}\n\
+      is nonempty.\n\
+      \n\
+      This process uses multiple strategies:\n\
+      - It looks for a parameter that matches the return type.\n\
+      - It tries synthesizing '{MessageData.ofConstName ``Inhabited}' and '{MessageData.ofConstName ``Nonempty}' \
+        instances for the return type.\n\
+      - It tries unfolding the return type.\n\
+      \n\
+      If the return type is defined using the 'structure' or 'inductive' command, \
+      you can try adding a 'deriving Nonempty' clause to it."
 
 end Lean.Elab

tests/lean/run/partialDelta.lean

@@ -0,0 +1,52 @@
+/-!
+# `partial` inhabitation with delta derivation
+-/
+set_option pp.mvars false
+
+/-!
+In the following, `partial` needs to unfold the return type to find an Inhabited instance.
+-/
+def MyGreatType (α : Type) := α × α
+
+partial def myLessGreatFunction (n : Nat) : MyGreatType Nat := myLessGreatFunction n
+
+
+/-!
+In the following, it needs to unfold underneath a forall.
+-/
+def MyGreaterType (α : Type) := α → MyGreatType α
+
+partial def myEvenLessGreatFunction (n : Nat) : MyGreaterType Nat := myEvenLessGreatFunction n
+
+
+/-!
+Regression test: can use existing parameter.
+-/
+partial def test1 (x : α) : α := test1 x
+
+/-!
+Regression test: can use Inhabited instance in parameter list.
+-/
+partial def test2 [Inhabited α] (n : Nat) : α := test2 n
+
+/-!
+Regression test: can use Nonempty instance in parameter list.
+-/
+partial def test3 [Nonempty α] (n : Nat) : α := test3 n
+
+/-!
+Error message.
+-/
+/--
+error: failed to compile 'partial' definition 'test4', could not prove that the type
+  {α : Sort u_1} → Nat → α
+is nonempty.
+
+This process uses multiple strategies:
+- It looks for a parameter that matches the return type.
+- It tries synthesizing 'Inhabited' and 'Nonempty' instances for the return type.
+- It tries unfolding the return type.
+
+If the return type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
+-/
+#guard_msgs in partial def test4 (n : Nat) : α := test4 n

tests/lean/sanitychecks.lean.expected.out

@@ -12,6 +12,15 @@ 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', failed to show that type is inhabited and non empty
+sanitychecks.lean:20:0-20:54: error: failed to compile 'partial' definition 'Foo.unsound4', could not prove that the type
+  Unit → False
+is nonempty.
+
+This process uses multiple strategies:
+- It looks for a parameter that matches the return type.
+- It tries synthesizing 'Inhabited' and 'Nonempty' instances for the return type.
+- It tries unfolding the return type.
+
+If the return type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
 sanitychecks.lean:22:12-22:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'
 sanitychecks.lean:25:12-25:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'