Zulip Chat Archive

Stream: mathlib4

Topic: Nonempty function instance

Patrick Massot (Feb 16 2024 at 19:13):

In Mathlib we have docs#Pi.instNonempty

protected instance Pi.instNonempty {ι : Sort*} {α : ι → Sort*} [∀ i, Nonempty (α i)] :
    Nonempty (∀ i, α i) :=
  ⟨fun _ ↦ Classical.arbitrary _⟩

That is problematic:

#synth Nonempty (ℕ) -- fine
#synth Nonempty (ℕ → ℕ) -- fine
#synth Nonempty (ℕ → ℕ → ℕ) -- fine
#synth Nonempty (ℕ → ℕ → ℕ → ℕ) -- fine
#synth Nonempty (ℕ → ℕ → ℕ → ℕ → ℕ) -- fine
#synth Nonempty (ℕ → ℕ → ℕ → ℕ → ℕ → ℕ) -- fine
#synth Nonempty (ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ) -- deterministic time out

Patrick Massot (Feb 16 2024 at 19:14):

One “fix” is to add

protected instance (priority := high) Fun.instNonempty {ι : Sort*} {α : Sort*} [Nonempty α] :
    Nonempty (ι → α) :=
  ⟨fun _ ↦ Classical.arbitrary _⟩

Patrick Massot (Feb 16 2024 at 19:14):

Should we simply do that and move on? Or should we think more deeply about that?

Thomas Murrills (Feb 16 2024 at 19:31):

“5 arguments ought to be enough for anyone.”

Thomas Murrills (Feb 16 2024 at 19:32):

Is this an instance of a more general pattern? And is there some generic way to detect if we’re in a situation that would cause this particular kind of issue?

Patrick Massot (Feb 16 2024 at 19:33):

I don’t know but this is the second time in three days that I hit such an issue with dependent functions instances.

Yury G. Kudryashov (Feb 16 2024 at 19:36):

I remember that we had lots of these issues in Lean 3.

Matthew Ballard (Feb 16 2024 at 19:48):

What are the imports here?

Patrick Massot (Feb 16 2024 at 19:50):

I’m investigating the minimal imports.

Matthew Ballard (Feb 16 2024 at 19:51):

In the prelude there is 

instance (α : Sort u) {β : Sort v} [Nonempty β] : Nonempty (α → β) :=
  Nonempty.intro fun _ => Classical.ofNonempty

instance (α : Sort u) {β : α → Sort v} [(a : α) → Nonempty (β a)] : Nonempty ((a : α) → β a) :=
  Nonempty.intro fun _ => Classical.ofNonempty

which don't stop there

Patrick Massot (Feb 16 2024 at 19:52):

Doing 

@[reducible]
protected noncomputable def Classical.arbitrary (α) [h : Nonempty α] : α :=
  Classical.choice h


protected instance Pi.instNonempty {ι : Sort _} {α : ι → Sort _} [∀ i, Nonempty (α i)] :
    Nonempty (∀ i, α i) :=
  ⟨fun _ ↦ Classical.arbitrary _⟩

in a no-import file is not enough to trigger the issue. I’m looking for the other instances that create the issue.

Patrick Massot (Feb 16 2024 at 19:53):

It seems Lean goes on a grand tour of the Mathlib class hierarchy here.

Johan Commelin (Feb 16 2024 at 19:54):

So I guess it's important that you use Nat instead of a random X : Type.

Matthew Ballard (Feb 16 2024 at 19:54):

Haha 18466 lines

Matthew Ballard (Feb 16 2024 at 19:54):

Just tracing defeq

Patrick Massot (Feb 16 2024 at 19:56):

Johan: no, it also fails at

variable {α : Type} [Nonempty α]
#synth Nonempty (α → α → α → α → α → α → α → α)

Patrick Massot (Feb 16 2024 at 19:56):

But indeed I’ll continue my investigation in this setup.

Matthew Ballard (Feb 16 2024 at 19:56):

Or with Unit

Matthew Ballard (Feb 16 2024 at 19:56):

In fact it seems worse

Patrick Massot (Feb 16 2024 at 19:57):

No, Unit may have more instances

Patrick Massot (Feb 16 2024 at 20:02):

We have lots of Nonempty instances.

Patrick Massot (Feb 16 2024 at 20:03):

In particular any algebraic structure we have gives a Nonempty instance. Lean simply tries all of them and it takes a lot of time. It doesn’t seem to go deep.

Patrick Massot (Feb 16 2024 at 20:03):

But I really don’t understand how making a non-dependent function instance helps.

Matthew Ballard (Feb 16 2024 at 20:18):

I don't understand why we aren't done after this

trace

Matthew Ballard (Feb 16 2024 at 20:19):

It proceeds to continue trying for Inhabited Nat

Yury G. Kudryashov (Feb 16 2024 at 20:49):

Shouldn't algebraic structure->nonempty instances have low priority?

Yury G. Kudryashov (Feb 16 2024 at 20:50):

Zero and One instances have priority 20

Yury G. Kudryashov (Feb 16 2024 at 20:50):

So, Lean should try Pi instance first.

Yury G. Kudryashov (Feb 16 2024 at 20:52):

How knows enough meta-programming to list all the "generic" instances with their priorities?

Kevin Buzzard (Feb 16 2024 at 21:04):

Patrick Massot said:

Johan: no, it also fails at

variable {α : Type} [Nonempty α]
#synth Nonempty (α → α → α → α → α → α → α → α)

This works fine for me (even after import Mathlib). I need one more alpha to push it over the edge though :-)

Matthew Ballard (Feb 16 2024 at 21:14):

It is like it forgets it has already used docs#instInhabitedNat to close the goal Inhabited Nat and then proceeds to forget about that instInhabitedNat completely

Thomas Murrills (Feb 16 2024 at 21:17):

Yury G. Kudryashov said:

How knows enough meta-programming to list all the "generic" instances with their priorities?

Here's an extremely quick way to see which instances match a given term along with their priority:

import Lean
import Mathlib

open Lean Meta Elab Term

elab "#show_instances " e:term : command => Command.runTermElabM fun _ => do
  let e ← elabTerm e none
  let x ← (← getGlobalInstancesIndex).getUnify e tcDtConfig
  let xs := x.map fun i => (i.priority, i.globalName?.getD `noname)
  logInfo m!"{xs.qsort fun a b => (a.1 < b.1 || a.1 == b.1 && a.2.quickLt b.2)}"

variable (α : Type)
#show_instances Nonempty α

Eric Wieser (Feb 16 2024 at 21:19):

Is the problem here that DiscrTrees don't index foralls?

Eric Wieser (Feb 16 2024 at 21:19):

And so the lookup has nothing to index on?

Matthew Ballard (Feb 16 2024 at 21:20):

Why would that show up at 6 arrows and not 5?

Yury G. Kudryashov (Feb 16 2024 at 21:20):

One problem I see is that docs#instNonempty has default priority

Yury G. Kudryashov (Feb 16 2024 at 21:21):

And docs#instForAllNonemptyNonempty matches too

Kevin Buzzard (Feb 16 2024 at 21:21):

Some features from the instance trace:

...
  [Meta.synthInstance] ✅ apply @LocalRing.toNontrivial to Nontrivial α
    [Meta.synthInstance.tryResolve] ✅ Nontrivial α ≟ Nontrivial α
    [Meta.synthInstance] new goal Semiring α
...
    [Meta.synthInstance] new goal LinearOrderedSemiring α
...
    [Meta.synthInstance] new goal NormedField α
...
    [Meta.synthInstance] new goal PartialOrder α
...
    [Meta.synthInstance] new goal CompleteDistribLattice α
...
    [Meta.synthInstance] new goal CoheytingAlgebra α
...
  [Meta.synthInstance] ✅ apply @NormedAddTorsor.toAddTorsor' to AddTorsor ?m.1622 α
...
    [Meta.synthInstance] new goal TopologicalSpace α
...
        [Meta.synthInstance] new goal (i : α) → AddGroup (?m.4681 i)
          [Meta.synthInstance.instances] #[@AddSubgroupClass.toAddGroup, @AddCommGroup.toAddGroup, @AddGroupWithOne.toAddGroup, @SeminormedAddGroup.toAddGroup, @NormedAddGroup.toAddGroup, @Pi.addGroup, @DMatrix.instAddGroupDMatrix, Real.instAddGroupReal, @TrivSqZeroExt.addGroup, @QuotientAddGroup.Quotient.addGroup, @Matrix.addGroup, @Additive.addGroup, @instAddGroupLex, @ContinuousMap.instAddGroupContinuousMap, Rat.addGroup, MulOpposite.addGroup, @ULift.addGroup, @MvPowerSeries.instAddGroupMvPowerSeries, @MeasureTheory.SimpleFunc.instAddGroup, AddOpposite.addGroup, @AddSubgroup.toAddGroup, @AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid, @DomAddAct.instAddGroupDomAddAct, @LocallyConstant.instAddGroupLocallyConstant, Int.instAddGroupInt, @CommRingCat.Colimits.ColimitType.AddGroup, @MeasureTheory.AEEqFun.instAddGroup, @Nat.ArithmeticFunction.instAddGroupArithmeticFunctionToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid, @SmoothMap.addGroup, FreeLieAlgebra.instAddGroupFreeLieAlgebra, @instAddGroupUniformFun, @Filter.Germ.addGroup, @CauSeq.addGroup, @DFinsupp.instAddGroupDFinsuppToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid, @instAddGroupUniformOnFun, @AddMonoid.Coprod.instAddGroupCoprodToAddZeroClassToAddMonoidToSubNegAddMonoidToAddZeroClassToAddMonoidToSubNegAddMonoid, @ZeroAtInftyContinuousMap.instAddGroup, @Equiv.instAddGroupShrink, @instAddGroupShrink, @Unitization.instAddGroup, @PowerSeries.instAddGroupPowerSeries, @Holor.instAddGroupHolor, @OrderDual.instAddGroup, @Prod.instAddGroup, @FreeAddGroup.instAddGroupFreeAddGroup, @AddCon.addGroup, @HahnSeries.instAddGroupHahnSeriesToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid, @Finsupp.addGroup, @UniformSpace.Completion.addGroup, @SymAlg.addGroup, @AddUnits.instAddGroup, @AddGroupCat.limitAddGroup, AddGroupCat.instGroupα, AddGroupCat.instGroupα_1, @AddMonCat.instGroupαAddMonoidOfToAddMonoidToSubNegAddMonoid, @AddGroupCat.FilteredColimits.colimitAddGroup, @AddGroupCat.addGroupObj, @instAddGroupObjOppositeOpensαTopologicalSpaceOfTopologicalSpace_coeToQuiverToCategoryStructOppositeSmallCategoryToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeOpensTypeToQuiverToCategoryStructTypesToPrefunctorPresheafSmoothSheaf]
...
          [Meta.synthInstance.tryResolve] 💥 AddGroup
                (?m.4681
                  i) ≟ AddGroup
                ((TopCat.Sheaf.presheaf (smoothSheaf (?m.4796 i) (?m.4802 i) (?m.4803 i) (?m.4806 i))).obj (?m.4811 i))
...
  [Meta.synthInstance] ✅ apply @UpgradedPolishSpace.toMetricSpace to MetricSpace (α → α)
...
    [Meta.synthInstance] new goal CanonicallyOrderedCommSemiring (α → α → α)
...

OK that's enough, and I'm only 4000 lines into 42000+ lines of trace output.

This has come up several times recently. One big problem with typeclass inference that we're seeing is that it's somehow intrinsically really stupid, and it has been able to get away with this because it is also really fast, but now mathlib is really big, and this is beginning to cost us. There seems to be no way to say "there is no topology here, so don't even think about starting to look through the topology heirarchy, which I have unfortunately had to import because there is topology used in a proof of a non-topological result which I needed earlier".

Yury G. Kudryashov (Feb 16 2024 at 21:27):

If I increase priority of docs#instNonemptyForAll, then it works.

Eric Wieser (Feb 16 2024 at 21:29):

I think lean4#2325 might help here

Matthew Ballard (Feb 16 2024 at 21:31):

It exhibits the same behavior with just core but has less to go through

Yury G. Kudryashov (Feb 16 2024 at 21:31):

I see in the backtrace that it applies Pi.instNonempty, then _inst, then propagates back; then it tries Nontrivial.to_nonempty for no obvious reason.

Eric Wieser (Feb 16 2024 at 21:32):

This is instant:

import Lean
import Mathlib

variable {α : Type} [Nonempty α]

set_option synthInstance.maxSize 4096
#synth Nonempty (α → α → α → α → α → α → α → α → α → α → α)

Matthew Ballard (Feb 16 2024 at 21:33):

For 

set_option trace.Meta.synthInstance true in
set_option trace.Meta.isDefEq true in
#synth Nonempty (Nat → Nat → Nat → Nat → Nat → Nat)

we get

trace

Eric Wieser (Feb 16 2024 at 21:33):

It's taking forever to fail because maxSize is forbidding it from finding the right instance, so now it has to try absolutely everything else (which will never succeed anyway)

Eric Wieser (Feb 16 2024 at 21:34):

It looks to me like TC search forgot how to count...

Eric Wieser (Feb 16 2024 at 21:35):

What's the trick for expanding the entire log tree view at once in the goal view?

Matthew Ballard (Feb 16 2024 at 21:36):

set_option trace.Meta.synthInstance true in
set_option trace.Meta.isDefEq true in
#synth Nonempty (Nat → Nat → Nat → Nat → Nat → Nat → Nat)

gives

trace

continued

Matthew Ballard (Feb 16 2024 at 21:36):

Matthew Ballard (Feb 16 2024 at 21:36):

Eric Wieser said:

What's the trick for expanding the entire log tree view at once in the goal view?

lake env lean and print to file?

Kevin Buzzard (Feb 16 2024 at 21:37):

I did lake build Mathlib.scratch.scratch10 > crap

Eric Wieser (Feb 16 2024 at 21:38):

set_option trace.Meta.synthInstance.newAnswer true makes it clear what's going on with the sizes

Eric Wieser (Feb 16 2024 at 21:39):

The progression is

2
6
14
30
62
126
254
510
1022
2046

Matthew Ballard (Feb 16 2024 at 21:39):

What is size counting?

Eric Wieser (Feb 16 2024 at 21:40):

I'm not sure, but if you combine it with set_option pp.explicit true then it's clear that the term size grows at least quadratically

Matthew Ballard (Feb 16 2024 at 21:41):

And I guess the dependent versions are longer than the non-dependent ones

Eric Wieser (Feb 16 2024 at 21:41):

I think it would be worth looking into the sizes more precisely

Kevin Buzzard (Feb 16 2024 at 21:42):

You mean like this ?

Matthew Ballard (Feb 16 2024 at 21:43):

maximum number of instances used to construct a solution in the type class instance synthesis procedure

Matthew Ballard (Feb 16 2024 at 21:43):

register_builtin_option synthInstance.maxSize : Nat := {
  defValue := 128
  descr := "maximum number of instances used to construct a solution in the type class instance synthesis procedure"
}

Kevin Buzzard (Feb 16 2024 at 21:45):

I assumed you were proposing adding it to the OEIS entry

Eric Wieser (Feb 16 2024 at 21:46):

Oh, may

Kevin Buzzard said:

You mean like this ?

My original intent was to look up the sequence, but after pasting it was pretty obvious!

Eric Wieser (Feb 16 2024 at 21:46):

Maybe it becomes exponential because every binder introduces horrible dependently-typed metavariables?

Patrick Massot (Feb 16 2024 at 21:46):

I guessed too! Does it mean I have IQ at least 50?

Patrick Massot (Feb 16 2024 at 21:47):

(I never took an actual IQ test, but to me it looks like the kind of question they ask)

Eric Wieser (Feb 16 2024 at 21:49):

The bonus question asks you to recite the OEIS id from memory

Eric Wieser (Feb 16 2024 at 21:50):

This one has the same exponential behavior, but here it's actually justified because this really is the size of the term:

abbrev ProdSelf (α) := α × α
#synth Nonempty (ProdSelf <| ProdSelf <| ProdSelf <| ProdSelf <| ProdSelf <| ProdSelf <| ProdSelf α)

Eric Wieser (Feb 16 2024 at 21:50):

(though I guess you could argue that if common-subexpression-elimination is a thing, this is also dramatically overcounting)

Kevin Buzzard (Feb 16 2024 at 21:50):

Right -- this reminds me of that Coq blog post about Group (G x G x G x G x G x G x G)

Eric Wieser (Feb 16 2024 at 21:51):

The numbers grow linearly for #synth Nonempty (α × α × α × α × α × α × α × α × α × α × α × α × α × α × α × α × ...), as you'd expect

Matthew Ballard (Feb 16 2024 at 21:51):

In docs#Lean.Meta.SynthInstance.addAnswer

if cNode.size ≥ (← read).maxResultSize then
      trace[Meta.synthInstance.answer] "{crossEmoji} {← instantiateMVars (← inferType cNode.mvar)}{Format.line}(size: {cNode.size} ≥ {(← read).maxResultSize})"

where is trace.Meta.synthInstance.answer?

Matthew Ballard (Feb 16 2024 at 21:53):

Never registered?

Thomas Murrills (Feb 16 2024 at 22:00):

Looks like it was added in this commit along with other synthInstance trace improvements, and was just accidentally left out

Matthew Ballard (Feb 16 2024 at 22:01):

The class it replaced discarded wasn't registered either?

Thomas Murrills (Feb 16 2024 at 22:06):

Oh, interesting... (Unrelated, but maybe we should lint to make sure every explicit trace class is in fact registered somewhere...possibly before it's used?)

Matthew Ballard (Feb 16 2024 at 22:26):

lean#3373

Last updated: May 02 2025 at 03:31 UTC