When instance synthesis fails due to a missing metavariable, other paths are not tried

[sgouezel]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When instance synthesis fails due to a missing metavariable, other paths are not tried.

Context

This example came from my investigations of why set_option backward.synthInstance.canonInstances false is needed a lot in mathlib in probability theory files.

Steps to Reproduce

Run the following code in the last nightly.

class FooClass (α : Type _) : Prop where

-- set_option backward.synthInstance.canonInstances false in -- the instance is found if you uncomment this line
theorem bar (α ι : Type _) [FooClass α] (f : ι → FooClass α) : FooClass α := by infer_instance

Expected behavior: [Clear and concise description of what you expect to happen]

The instance should be found. First, f should be tried to provide the instance, but since there is no way to find the metavariable in f ?m.36, instance search should go on, and find the instance coming from [FooClass α].

Actual behavior: [Clear and concise description of what actually happens]

The instance is not found, because instance search stops after trying (and failing) f ?m.36. Note that the instance is found if one uncomments the line set_option backward.synthInstance.canonInstances false in, but I don't see why this should be relevant.

Versions

4.9.0-nightly-2024-05-17

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.