instances that match unconditionally

Stream: mathlib4

[Matthew Ballard]

Using the following

code

import Mathlib

open Lean Meta DiscrTree

structure NaughtyInstance where
  name : Name
  type : Name
  priority : Nat
  isProjFn : Bool

instance : ToMessageData NaughtyInstance where
  toMessageData inst :=
  let isProj := if inst.isProjFn then "Projection" else "Not Projection"
  m!"{inst.name}, Type: {inst.type}, Priority: {inst.priority}, {isProj}"

def getNaughtyInstances : MetaM (List NaughtyInstance) := do
  let env ← getEnv
  let filtered ← env.constants.toList.filterM (fun (name, _) => isInstance name)
  let mut list := []
  for (name, info) in filtered do
    let prio ← getInstancePriority? name
    let isProj ← isProjectionFn name
    let (_, _, type) ← forallMetaTelescopeReducing info.type
    let keys ← mkPath type
    if keys.toList.drop 1 |>.all (· == .star) then
      if let .const type _ := keys[0]! then
      list := { name := name, type := type, priority := prio.get!, isProjFn := isProj } :: list
  return list

run_meta do
  let instances ← getNaughtyInstances
  logInfo m!"Total number universally application instances: {instances.length}"
  let defaultPrio := instances.filter (fun inst => inst.priority ≥ 1000)
  logInfo m!"Number with priority at or above default: {defaultPrio.length}"
  let projections := instances.filter (fun inst => inst.isProjFn)
  logInfo m!"Number of projection functions: {projections.length}"
  let mut msg := m!""
  for inst in instances do
    msg := msg ++ m!"{inst}\n"
  logInfo msg

gives the following list https://gist.github.com/mattrobball/8690f3a7bbb5ccb4c8e6cb632a495a34

These are instances that Lean will always attempt for the corresponding synthesis problem. Their current priority is listed

[Matthew Ballard]

Library note:

Therefore, if we create an instance that always applies, we set the priority of these instances to 100 (or something similar, which is below the default value of 1000).

If you filter the list of 2600+, 1504 of them have default priority. (None above thankfully)

[Edward van de Meent]

at first glance, a bunch of these look like class extends instances?

[Matthew Ballard]

Yes many are

[Edward van de Meent]

btw, what is the tag of the library note you're referring to?

[Matthew Ballard]

Matthew Ballard said:

Yes many are

792 to be exact

[Matthew Ballard]

Edward van de Meent said:

btw, what is the tag of the library note you're referring to?

"lower instance priority"

[Edward van de Meent]

"lower cancel priority" seems to be a related (duplicate/specialized) library note?

We lower the priority of inheriting from cancellative structures.
This attempts to avoid expensive checks involving bundling and unbundling with the IsDomain class.
since IsDomain already depends on Semiring, we can synthesize that one first.
#general > Why is `simpNF` complaining here?

[Matthew Ballard]

There are two issues:

1. slowing down instance synthesis that succeeds
2. slowing down instance synthesis that fails

Priority doesn't really matter for the latter as everything get tried. For that, the only real tool we have is scoping to a namespace.

I would argue that some are pretty crazy from a human perspective. For example docs#IsAddKleinFour.instFinite. If I was handed a random type and asked to check it is Finite, asking "Is it a Klein 4-group?" would not be anywhere on my list of questions. Unless, of course, I was already working with such things. But it is globally available and has default priority.

[Matthew Ballard]

Of the two issues, the latter seems to do the most damage to people's workflow.

[Edward van de Meent]

Matthew Ballard said:

For example docs#IsAddKleinFour.instFinite. If I was handed a random type and asked to check it is Finite, asking "Is it a Klein 4-group?" would not be anywhere on my list of questions.

looking into this, since among the fields of IsAddKleinFour is Nat.card T = 4, this indeed is a very useless instance :rolling_on_the_floor_laughing:

[Matthew Ballard]

Updated the gist to reflect that classes with more than one parameter exist.

[Kevin Buzzard]

Cool that we have a universal property for being the Klein four group though.

[Matthew Ballard]

I agree :)

[Matthew Ballard]

Matthew Ballard said:

Updated the gist to reflect that classes with more than one parameter exist.

Updated the code also now

[Matthew Ballard]

naughty_instances.csv
Here is a spreadsheet with the instances for easier human inspection

[Eric Wieser]

At some point there was an RFC to lean 4 to lower the priority of instances generated by extends (edit: lean4#2325), but I think it was rejected because it didn't actually affect performance.

[Matthew Ballard]

Yeah, I tried that about a year ago with different values for both the parent and non-parents. It didn't seem to make a big difference.

I think the main issue are instances that expand the search space too much. Eg you are searching for Unique and then you hit a Group -> Unique and you are crawling the whole algebraic hierarchy when it has little to do with your current setting

[Yury G. Kudryashov]

Probably, you mean Group -> Nonempty. You can't prove Group -> Unique.

[Eric Wieser]

I'm not really convinced that these unconditional instances are a bad thing, so long as none of them loop. Worst case scenario should be that we visit every typeclass once though these, right?

[Aaron Liu]

Eric Wieser said:

I'm not really convinced that these unconditional instances are a bad thing, so long as none of them loop. Worst case scenario should be that we visit every typeclass once though these, right?

No, you can repeat typeclasses with different parameters.

[Eric Wieser]

The examples I can think of all have structurally "smaller" parameters in the assumptions, if you're describing what I think you are

[Floris van Doorn]

I think instances that have the form MyClass (MyReducibleDefinition ..) are a footgun, since they always apply, but don't look like they do.

[Floris van Doorn]

Eric Wieser said:

I'm not really convinced that these unconditional instances are a bad thing, so long as none of them loop. Worst case scenario should be that we visit every typeclass once though these, right?

Is simp still checking whether a type is a subsingleton for all terms it traverses? You might be doing this check frequently, for many different types.

[Floris van Doorn]

But I'm very much in favor of scoping instances from a very domain-specific area to a general area with weak keys.

For example, the following failure spends 90% of the time trying to show that Fin 2 is a sifted category because of docs#CategoryTheory.IsSifted.nonempty (before #22780 it would also spend a bunch of time in the algebraic hierarchy).

import Mathlib

set_option trace.Meta.synthInstance true
-- set_option trace.profiler true
set_option profiler true
set_option profiler.threshold 1

-- attribute [-instance]
--   CategoryTheory.IsSifted.nonempty

example (A : Type*) : Subsingleton (Fin 2 → ℝ) := by
  try infer_instance
  sorry

[Matthew Ballard]

Yury G. Kudryashov said:

Probably, you mean Group -> Nonempty. You can't prove Group -> Unique.

Right. I was trying to say that Group + Stuff -> Unique. Depending on the ordering, you end up searching the algebraic hierarchy.

[Matthew Ballard]

Floris van Doorn said:

But I'm very much in favor of scoping instances from a very domain-specific area to a general area with weak keys.

If there is scoped notation, then there is no UX impact with scoping instances

[Matthew Ballard]

Eric Wieser said:

I'm not really convinced that these unconditional instances are a bad thing, so long as none of them loop. Worst case scenario should be that we visit every typeclass once though these, right?

Does caching use the context? I should look

[Matthew Ballard]

I can try to rerun my experiment setting all projection instances to 100

[Matthew Ballard]

Floris van Doorn said:

I think instances that have the form MyClass (MyReducibleDefinition ..) are a footgun, since they always apply, but don't look like they do.

Should we have a “redundant instance” linter? It wouldn’t ban them per se but the user would have to opt in in making it and give a doc string

[Floris van Doorn]

Maybe. We can also port the instance priority linter from Lean 3 and make sure it looks at the key, so that reducible definitions are also caught.
But before we do that, we probably should test that setting instance priorities actually speeds up (succeeding) instance synthesis.

[Eric Wieser]

docs#CategoryTheory.IsSifted.isSifted_of_hasBinaryCoproducts_and_nonempty forms a loop though, with IsSifted.nonempty

[Yury G. Kudryashov]

Why Nonempty (Fin 2) helps to prove Subsingleton (Fin 2 → _)?

[Kevin Buzzard]

Yes you would think that this is a step backwards!

[Yury G. Kudryashov]

Can you follow the path that leads to this search?

[Floris van Doorn]

docs#IsEmpty.instSubsingleton + docs#instIsEmptyForallOfNonempty
This indeed leads to the unfortunate consequence that you're solving useless side-conditions. Not sure how we can solve this... The simple search that type-class inference might just be too simple to figure out that these are "stupid" sequences of instances.

[Jovan Gerbscheid]

I made #22953 to reorder the arguments of docs#instIsEmptyForallOfNonempty, so it becomes

instance {p : α → Sort*} [∀ x, IsEmpty (p x)] [h : Nonempty α] : IsEmpty (∀ x, p x)

So then the useless side condition Nonempty α is only attempted after the main condition. This should fix the above slow synthesis.

[Jovan Gerbscheid]

Arguably, the same swap should be made in instCountableForallOfFinite, so it becomes

instance [∀ a, Countable (π a)] [Finite α] : Countable (∀ a, π a)

where Finite α plays the role of useless side condition.

[Michael Rothgang]

:working_on_it: the KleinFour instance

[Michael Rothgang]

#22958 scopes the KleinFour.instFinite instance

[Jovan Gerbscheid]

I was going to say that CategoryTheory.IsSifted.nonempty (with IsSifted.isSifted_of_hasBinaryCoproducts_and_nonempty) is a bad instance.

But even worse is that following traverses the algebraic hierarchy three times, once for Limits.WalkingPair, once for (J : Type _) and once for (J : Type):

import Mathlib

open CategoryTheory
set_option trace.Meta.synthInstance true
example (C : Type*) [Category C] : Limits.HasBinaryCoproducts C := by
  infer_instance

[Michael Rothgang]

#23052 scopes the IsSifted.nonempty instance.

[Michael Rothgang]

Results of the above: -0,5% on linting, neutral on instructions (which is probably not surprising, given that these files are close to leaf files).

[Michael Rothgang]

Jovan Gerbscheid said:

Arguably, the same swap should be made in instCountableForallOfFinite, so it becomes

instance [∀ a, Countable (π a)] [Finite α] : Countable (∀ a, π a)

where Finite α plays the role of useless side condition.

#23073 tries this (still running CI)

[Yury G. Kudryashov]

Re: #23073: No benchmark entry differed by at least +1.0⬝10⁹ instructions.

[Matthew Ballard]

Matthew Ballard said:

I can try to rerun my experiment setting all projection instances to 100

branch#mrb/reduce_prios will (should!) have a working toolchain in ~ 1 hr. If people want to hack on it to get it working, please do.

[Michael Rothgang]

CI in that run failed: from the log, in the "print lean and lake versions" step

info: downloading component 'lean'
error: binary package was not provided for 'linux'
Error: Process completed with exit code 1.

[Matthew Ballard]

CI didn't wait an hour :) The toolchain should be there now

[Matthew Ballard]

I've pushed it along but have to step away for the day. Please feel free to continue