feat: partial inhabitation uses local Inhabited instances created…

… from parameters (leanprover#5821)

Rather than having a special pass where `mkInhabitantFor` uses the
`assumption` tactic, it creates `Inhabited` instances for each parameter
and just searches for an `Inhabited`/`Nonempty` instance for the return
type.

This makes examples like the following work:
```lean
partial def f (x : X) : Bool × X := ...
```

Removes the strategy where it looks for `Inhabited`/`Nonempty` instances
for every suffix of the signature.

This is a follow-up to leanprover#5780. 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

@@ -9,6 +9,20 @@ import Lean.PrettyPrinter
 namespace Lean.Elab
 open Meta
 
+private def withInhabitedInstances (xs : Array Expr) (k : Array Expr → MetaM α) : MetaM α := do
+  let rec go (i : Nat) (insts : Array Expr) : MetaM α := do
+    if h : i < xs.size then
+      let x := xs[i]
+      let xTy ← inferType x
+      let u ← getLevel xTy
+      let instTy := mkApp (.const ``Inhabited [u]) xTy
+      let instVal := mkApp2 (.const ``Inhabited.mk [u]) xTy x
+      withLetDecl `inst instTy instVal fun inst =>
+        go (i + 1) (insts.push inst)
+    else
+      k insts
+  go 0 #[]
+
 private def mkInhabitant? (type : Expr) (useOfNonempty : Bool) : MetaM (Option Expr) := do
   try
     if useOfNonempty then
@@ -18,55 +32,41 @@ private def mkInhabitant? (type : Expr) (useOfNonempty : Bool) : MetaM (Option E
   catch _ =>
     return none
 
-private def findAssumption? (xs : Array Expr) (type : Expr) : MetaM (Option Expr) := do
-  xs.findM? fun x => do isDefEq (← inferType x) type
-
-private def mkFnInhabitant? (xs : Array Expr) (type : Expr) (useOfNonempty : Bool) : MetaM (Option Expr) :=
-  let rec loop
-    | 0,   type => mkInhabitant? type useOfNonempty
-    | i+1, type => do
-      let x := xs[i]!
-      let type ← mkForallFVars #[x] type;
-      match (← mkInhabitant? type useOfNonempty) with
-      | none     => loop i type
-      | 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
+private partial def mkInhabitantForAux? (xs insts : Array Expr) (type : Expr) (useOfNonempty : Bool) : MetaM (Option Expr) := withIncRecDepth do
+  if let some val ← mkInhabitant? type useOfNonempty then
+    mkLambdaFVars xs (← mkLetFVars (usedLetOnly := true) insts val)
   else
     let type ← whnfCore type
     if type.isForall then
-      forallTelescope type fun xs' type' => do
-        mkInhabitantForAux? (xs ++ xs') type' useOfNonempty
+      forallTelescope type fun xs' type' =>
+        withInhabitedInstances xs' fun insts' =>
+          mkInhabitantForAux? (xs ++ xs') (insts ++ insts') type' useOfNonempty
     else if let some type' ← unfoldDefinition? type then
-      mkInhabitantForAux? xs type' useOfNonempty
+      mkInhabitantForAux? xs insts 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
-  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."
+def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr :=
+  withInhabitedInstances xs fun insts => do
+    if let some val ← mkInhabitantForAux? xs insts type false <||> mkInhabitantForAux? xs insts 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, while making every parameter into a local '{MessageData.ofConstName ``Inhabited}' instance.\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

@@ -44,9 +44,18 @@ 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 synthesizing 'Inhabited' and 'Nonempty' instances for the return type, while making every parameter into a local 'Inhabited' instance.
 - 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
+
+/-!
+Add arguments as inhabited instances.
+Example adapted from https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Why.20return.20type.20of.20partial.20function.20MUST.20.60inhabited.60.3F/near/477905312
+-/
+inductive ListNode where
+  | mk : Nat → Option ListNode → ListNode
+
+partial def checkMyList (head : ListNode) : Bool × ListNode := checkMyList head

tests/lean/sanitychecks.lean.expected.out

@@ -18,7 +18,7 @@ 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 synthesizing 'Inhabited' and 'Nonempty' instances for the return type, while making every parameter into a local 'Inhabited' instance.
 - 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.