class instance resolution failure

Stream: general

[Yury G. Kudryashov]

Hi, the following code works with mathlib before c6c7eaf and fails starting with c6c7eaf34:

import analysis.normed_space.multilinear

noncomputable theory
open_locale classical big_operators
open finset metric

universes u v wE wE₁ wG
variables {𝕜 : Type u} {ι : Type v}
  {E : ι → Type wE} {E₁ : ι → Type wE₁}
  {G : Type wG}
  [decidable_eq ι] [fintype ι] [nondiscrete_normed_field 𝕜]
  [Π i, normed_group (E i)] [Π i, normed_space 𝕜 (E i)]
  [Π i, normed_group (E₁ i)] [Π i, normed_space 𝕜 (E₁ i)]
  [normed_group G] [normed_space 𝕜 G]

local attribute [instance, priority 1001]
add_comm_group.to_add_comm_monoid normed_group.to_add_comm_group normed_space.to_semimodule smul_comm_class_self

example := Π i, semimodule 𝕜 (E i →L[𝕜] E₁ i) -- works

example := -- "failed to synthesize type class instance for (...) `Π (i : ι), semimodule 𝕜 (E i →L[𝕜] E₁ i)`
  continuous_multilinear_map 𝕜 (λ i, E i →L[𝕜] E₁ i) (continuous_multilinear_map 𝕜 E G)

How can I make it compile without using @continuous_multilinear_map?

[Eric Wieser]

I assume the relevant change from that PR is around here? https://github.com/leanprover-community/mathlib/commit/c6c7eaf34#diff-29a16c03884a7a902d4ae9eaed0b63eaf7cb329734950ecc58618a155fe80bc4R753

[Eric Wieser]

Some more hints:

-- fails
def e1 :=
  @continuous_multilinear_map 𝕜 _ (λ i, E i →L[𝕜] E₁ i) (continuous_multilinear_map 𝕜 E G)
    _ _ _ _ (infer_instance) _ _ _

-- ok
def e2 :=
  @continuous_multilinear_map 𝕜 _ (λ i, E i →L[𝕜] E₁ i) (continuous_multilinear_map 𝕜 E G)
    _ _ _ _ (λ i, infer_instance) _ _ _

I've seen this problem before, where type-class inference can't find pi-instances

[Eric Wieser]

Indeed, your works example is misleading, and what you actually wanted to check is

example : Π i, semimodule 𝕜 (E i →L[𝕜] E₁ i) := infer_instance

which fails

[Yury G. Kudryashov]

Another relevant part of the commit: https://github.com/leanprover-community/mathlib/commit/c6c7eaf34#diff-6eb2551e17f95d2b8d8985018d5587c8604357697034aba70a50128c08ff4545L375

[Violeta Hernández]

I PR'd #14601, which adds an instance

instance subsingleton.is_well_order [subsingleton α] (r : α → α → Prop) [hr : is_irrefl α r] :
  is_well_order α r :=
sorry

This single addition seems to lead to class instance resolution failing on docs#list.lex.is_strict_total_order. I have no idea why.

[Alex J. Best]

Couldn't this loop with docs#is_well_order.is_irrefl? Maybe that is the cause

[Eric Wieser]

What does #lint have to say here?

[Violeta Hernández]

Oh yeah, that makes sense!

[Violeta Hernández]

I'll make this into a theorem instead then