Zulip Chat Archive

Stream: general

Topic: class instance resolution failure


Yury G. Kudryashov (Feb 09 2021 at 13:29):

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 (Feb 09 2021 at 13:37):

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

Eric Wieser (Feb 09 2021 at 13:44):

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 (Feb 09 2021 at 13:50):

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 (Feb 09 2021 at 13:53):

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

Violeta Hernández (Jun 07 2022 at 20:56):

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 (Jun 07 2022 at 21:18):

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

Eric Wieser (Jun 07 2022 at 21:23):

What does #lint have to say here?

Violeta Hernández (Jun 07 2022 at 22:31):

Oh yeah, that makes sense!

Violeta Hernández (Jun 07 2022 at 22:31):

I'll make this into a theorem instead then


Last updated: Dec 20 2023 at 11:08 UTC