Typeclass resolution under binders

Stream: general

[Eric Wieser]

What's going on here?

import analysis.normed_space.basic

variables (𝕜 ι : Type*) (E : ι → Type*)

-- ok
example
  [nondiscrete_normed_field 𝕜] [Π i, normed_group (E i)] [Π i, semi_normed_space 𝕜 (E i)] :
  Π i, module 𝕜 (E i) := λ i, by apply_instance

-- fails
example
  [nondiscrete_normed_field 𝕜] [Π i, normed_group (E i)] [Π i, semi_normed_space 𝕜 (E i)] :
  Π i, module 𝕜 (E i) := by apply_instance

/-- This is `semi_normed_space.to_module` with stronger assumptions -/
instance semi_normed_space.to_module'
  [normed_field 𝕜] (F : Type*) [normed_group F] [semi_normed_space 𝕜 F] :
  module 𝕜 F := by apply_instance

-- now works
example
  [nondiscrete_normed_field 𝕜] [Π i, normed_group (E i)] [Π i, semi_normed_space 𝕜 (E i)] :
  Π i, module 𝕜 (E i) := by apply_instance

[Sebastien Gouezel]

It's probably an instance of https://github.com/leanprover/lean4/issues/509 . This has been fixed in Lean 4, but backporting the fix is out of my league.

[Eric Wieser]

I realized I ran into this before in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/decidable_pred.20instance.20not.20found.20by.20typeclass.20search/near/219962294

[Eric Wieser]

Adding this new semi_normed_space.to_module' instance seems to remove the need for a handful of @ symbols, so seems to me like a good idea.

[Oliver Nash]

I just bumped into the following, which I'm guessing is related:

import analysis.normed_space.basic

noncomputable theory

example (𝕜 M X : Type*) [normed_field 𝕜]
  [normed_group M] [normed_space 𝕜 M] : module 𝕜 (X → M) :=
by apply_instance -- Works

example (M X : Type*)
  [normed_group M] [normed_space ℝ M] : module ℝ (X → M) :=
by apply_instance -- Fails :-(

[Oliver Nash]

Knowing (vaguely) that there are issues (fixed in Lean 4) with typeclass inference and pi types, I'm not so surprised that my second example fails. However conditioning on my first example succeeding, I am.

[Oliver Nash]

FWIW, this is a proof:

example (M X : Type*)
  [normed_group M] [normed_space ℝ M] : module ℝ (X → M) :=
begin
  haveI : module ℝ M := by apply_instance,
  apply_instance,
end

[Oliver Nash]

I wonder is this somehow connected with noncomputability weirdness: we need to use real.normed_field for this to work.

[Kevin Buzzard]

So should this

instance foo (M : Type*)
  [normed_group M] [normed_space ℝ M] : module ℝ M :=
by apply_instance

be an explicit instance? (this fixes the problem in this instance, unsurprisingly). Sometimes you see this sort of stuff in mathlib (e.g. at one point data.rat.basic had a ton of this stuff) with comments such as "short cutting type class inference".

[Oliver Nash]

Right, this is really my question. I think your foo should be an instance but I'll wait a few hours before I take any action to see if there are other remarks.

[Kevin Buzzard]

oh those rat instances are still there! What's that all about?

[Eric Wieser]

I think I ran into this over and over again in my matrix exponential PR (#13520)

[Eric Wieser]

https://github.com/leanprover-community/mathlib/blob/53b1437ed8455a51cf10af033e299a8101b2f6b4/src/analysis/normed_space/matrix_exponential.lean#L64-L103

[Oliver Nash]

#14013

[Eric Wieser]

Repeating my comment from the PR, this instance also works:

instance function.module
  (R β X : Type*) [semiring R] [add_comm_monoid β] [module R β] : module R (X → β) :=
by apply_instance

[Eric Wieser]

Note we already have docs#function.algebra in the same style