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.
Prerequisites
Please put an X between the brackets as you perform the following steps:
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.
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 inf ?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 lineset_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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.