various type-class loops

Stream: general

[Floris van Doorn]

I wrote a new linter that catches type-class loops (#8932), and I'm making some topics with some issues it found. I don't always know the best solution to fix these loops, so I'm hoping that someone who knows that part of mathlib better can fix these.

Here are some problematic instances in the library

• docs#nat.subtype.semilattice_sup_bot loops with the forgetful instances semilattice_sup_bot -> has_bot -> nonempty (I think this was originally written by @Chris Hughes, but it's very old). Here is an example (that is supposed to fail):

import data.nat.basic

example (s : set ℕ) [decidable_pred (∈ s)] : semilattice_sup_bot s :=
by apply_instance

• docs#sub_mul_action.has_zero loops with docs#has_zero.nonempty. (@Eric Wieser)
• The class docs#add_torsor is problematic. It comes with the instance docs#add_torsor.nonempty (a "dangerous" instance src#linter.dangerous_instance). This causes a loop with e.g. docs#affine_subspace.to_add_torsor (which would normally be a fine instance) (@Joseph Myers)

import linear_algebra.affine_space.affine_subspace

example (k V P : Type*) [ring k] [add_comm_group V] [module k V]
 [add_torsor V P] {s : set P} : nonempty (affine_span k s) :=
by apply_instance

[Floris van Doorn]

• The next problem I found has the least clear solution. It is an instance that doesn't loop, but takes a long time to fail. On yesterday's mathlib it takes 8.6 seconds on my laptop (#8933 should have reduced that a bit)

--after running scripts/mk_all.sh
import all

open topological_space measure_theory

set_option profiler true
example {α E : Type*} {m0 : measurable_space α} {p : ennreal} {μ : measure α}
  [measurable_space E] [normed_group E] [borel_space E]
  [second_countable_topology E] [hp : fact (1 ≤ p)] :
  complete_space (measure_theory.Lp E p μ) :=
by apply_instance

During the type-class search, a suprising amount of time is spent that some of these infinite-dimensional objects are instances of fintype, decidable_eq, unique, subsingleton, etc., which are classes with a lot of instances.

The following instances reduce the type-class inference type most.

local attribute [-instance] -- with all instances: 8.6s
  finite_dimensional.complex_to_real -- without this instance: 5.1s
  -- as of #8933 the next line should be insignificant
  is_simple_lattice.fintype -- without this and above instances: 2.7s
  ring.is_noetherian_of_fintype -- without this and above instances: 1.3s
  finite_dimensional.proper_is_R_or_C -- without this and above instances: 0.6s
  fintype.compact_space -- without this and above instances: 0.3s
  subsingleton.compact_space -- without this and above instances: 0.2s

I'm wondering if we can make some of these instances localized. For example, I expect that docs#ring.is_noetherian_of_fintype, docs#fintype.compact_space and docs#subsingleton.compact_space are rarely used (and the last one can probably be removed given that we have the fintype one). Maybe we could localize them in some locale? The remaining two instances (docs#finite_dimensional.complex_to_real and docs#finite_dimensional.proper_is_R_or_C) do seem useful often, so I'm not sure what to do with them.

[Floris van Doorn]

Removing/localizing these instances would also speed up other failures of type-class problems

import all

-- 6.3s with all instances -> 0.1s without the instances mentioned above
example {R K : Type*} [integral_domain R] [field K] [algebra R K]
  [is_fraction_ring R K] : fintype (class_group R K) :=
by apply_instance

-- 8.5s with all instances -> 1.6s without the instances mentioned above
-- (this one might be harder to get under <0.5s)
example {K V : Type*} [field K] [add_comm_group V] [module K V]
(S₁ S₂ : submodule K V) : finite_dimensional K (S₁ ⊓ S₂ : submodule K V) :=
by apply_instance

[Joseph Myers]

It looks like the add_torsor.nonempty instance was added by @Yury G. Kudryashov as part of the out_param changes (#3727). What breaks if you make it no longer an instance?

[Floris van Doorn]

Let's find out! branch#add_torsor_nonempty (I mistakenly looked at the field [nonempty : nonempty P] in Git blame for whom to "blame")

[Yury G. Kudryashov]

Note that the loop has nothing to do with the instance being "dangerous".

[Floris van Doorn]

Oh you're right, I missed that G is an out_param of the class.
In that case docs#affine_subspace.to_add_torsor seems like a bad instance

[Yury G. Kudryashov]

But we want to have an affine space structure on a nontrivial affine subspace. Should we introduce yet another ne_bot?

[Yury G. Kudryashov]

And use it instead of nonempty for affine_subspaces until we migrate to Lean 4?

[Johan Commelin]

@Floris van Doorn a generic question: do you think some of these problems are "worth" ignoring :see_no_evil: because Lean 4 is around the proverbial corner?

[Floris van Doorn]

If Lean 4 has no problem with all these loops, then I guess it's ok to ignore these in Lean 3 for the moment.
I'll test these loops in the binported version, and see if (and how well) it can deal with these.