weird unification issue

Stream: general

[Sebastien Gouezel]

I have encountered a weird unification issue. Sometimes, when there is an instance for dependent types, Lean 3 has difficulties inferring this instance in a non-dependent situation, and we need to add the corresponding non-dependent instance to help it. That's what I had done for an instance on complete product spaces, but it broke a proof in a later file. I have reduced the issue to the following mwe:

import analysis.calculus.inverse

lemma Pi.complete_nondep {ι : Type*} (α : Type*) [uniform_space α]
[complete_space α] : complete_space (ι → α) :=
Pi.complete _

lemma foo (ι : Type*) [h : fintype ι] :
@complete_space (ι → ℝ)
  (@metric_space.to_uniform_space' (ι → ℝ)
     (@semi_normed_group.to_pseudo_metric_space (ι → ℝ)
        (@normed_group.to_semi_normed_group (ι → ℝ)
           (@pi.normed_group ι (λ (ᾰ : ι), ℝ) h (λ (i : ι), real.normed_group))))) :=
begin
  apply Pi.complete_nondep ℝ,
end

Here, Pi.complete_nondep is the new instance I would like to add (registered here only as a lemma), and foo is the issue this instance creates. The proof apply Pi.complete_nondep ℝ works fine, but apply Pi.complete_nondep _ does not, and neither does exact Pi.complete_nondep ℝ, for reasons I don't understand.

[Floris van Doorn]

FWIW exact @Pi.complete_nondep _ ℝ _ _ does work. I forgot the details about how adding @ changes the elaborator.
My guess is that when the elaborator is lost, it's first trying to unify the last (type-class) argument, and somehow running in circles when doing that.