wird instance search

Stream: general

[Sebastien Gouezel]

It's been a long time, but I don't understand what is going on with a typeclass search. Unfortunately, I haven't a mwe. In the file topology/uniform_space/pi, we have an instance

instance Pi.complete [∀ i, complete_space (α i)] : complete_space (Π i, α i) := ...

Since this instance fails to fire in non-dependent situations, I have added just below a new instance

instance Pi.complete_nondep (β : Type u) [uniform_space β] [complete_space β] :
  complete_space (ι → β) :=
Pi.complete _

Then, let's open a new file, and paste

import topology.metric_space.basic
universes u
set_option trace.class_instances true
lemma foo (α : Type u) [metric_space α] [complete_space α] :
  complete_space (ℕ → α) := by apply_instance

The instance search fails because it reaches the maximum recursion level. The trace starts with

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : @complete_space (ℕ → α)
  (@Pi.uniform_space ℕ (λ (ᾰ : ℕ), α)
     (λ (i : ℕ), @metric_space.to_uniform_space' α (@metric_space.to_pseudo_metric_space α _inst_1))) := _inst_2
failed is_def_eq
[class_instances] (0) ?x_0 : @complete_space (ℕ → α)
  (@Pi.uniform_space ℕ (λ (ᾰ : ℕ), α)
     (λ (i : ℕ), @metric_space.to_uniform_space' α (@metric_space.to_pseudo_metric_space α _inst_1))) := @Pi.complete_nondep ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6
[class_instances] (1) ?x_6 : @complete_space α (@metric_space.to_uniform_space' α (@metric_space.to_pseudo_metric_space α _inst_1)) := _inst_2
[class_instances] caching instance for @complete_space α (@metric_space.to_uniform_space' α (@metric_space.to_pseudo_metric_space α _inst_1))
_inst_2
[class_instances] (1) ?x_3 i : uniform_space (?x_2 i) := @Pi.uniform_space (?x_7 i) (?x_8 i) (?x_9 i)
failed is_def_eq
[class_instances] (1) ?x_3 i : uniform_space (?x_2 i) := @uniform_space.separation_quotient.uniform_space (?x_10 i) (?x_11 i)
[class_instances] (2) ?x_11 i : uniform_space (?x_10 i) := @Pi.uniform_space (?x_12 i) (?x_13 i) (?x_14 i)
failed is_def_eq
[class_instances] (2) ?x_11 i : uniform_space (?x_10 i) := @uniform_space.separation_quotient.uniform_space (?x_15 i) (?x_16 i)

and then starts repeating itself.

Am I doing something wrong here? My new instance seems perfectly reasonable to me...

[Sebastien Gouezel]

Sorry, please ignore.