Tracing time of type class inference

Stream: new members

[Nicolò Cavalleri]

At some point of some new code I wrote, Lean is taking a very long time (several minutes) to resolve all the type class inference. I saw I can trace the result with trace.class_instances true, but is there a way to rank all the results by the time it took lean to find them? I want to understand where exactly it is taking so long so I can try to play with priorities

[Scott Morrison]

Typically each individual step in trace.class_instances true is somewhat uniform in time. The thing you're really looking for is the parts of the typeclass search that are extremely deep (the number in parentheses), because that often indicates a combinatorial blow-up in the search tree, which is what you want to avoid.

But I'd also be happy to hear an answer to your actual question! :-)

[Nicolò Cavalleri]

Well basically this is a #mwe of my problem:

import geometry.manifold.algebra.smooth_functions
import ring_theory.derivation

open_locale manifold

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
{E : Type*} [normed_group E] [normed_space 𝕜 E]
{H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
(M : Type*) [topological_space M] [charted_space H M]

variables (X : derivation 𝕜 C^∞⟮I, M; 𝕜⟯ C^∞⟮I, M; 𝕜⟯)

structure test extends derivation 𝕜 C^∞⟮I, M; 𝕜⟯ C^∞⟮I, M; 𝕜⟯

The last two lines both take ages to compile and in particular the last line triggers a deterministic timeout although it compiles through lean --make on the command line. I played with set_option trace.class_instances true for the past 3 hours but I still did not manage to understand where is type class inference having such a hard time...

[Nicolò Cavalleri]

What priorities can I change to make this work?

[Kevin Buzzard]

import geometry.manifold.algebra.smooth_functions
import ring_theory.derivation

open_locale manifold

variables {𝕜 : Type} [nondiscrete_normed_field 𝕜]
{E : Type} [normed_group E] [normed_space 𝕜 E]
{H : Type} [topological_space H] (I : model_with_corners 𝕜 E H)
(M : Type) [topological_space M] [charted_space H M]

def foo := @derivation 𝕜 C^∞⟮I, M; 𝕜⟯ _ _ -- instant

#check @derivation 𝕜 C^∞⟮I, M; 𝕜⟯ _ _ -- Π [_inst_3_1 : algebra 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯] ...

example : algebra 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ := infer_instance -- instant
example : algebra 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ := infer_instance -- instant

def bar := @derivation 𝕜 C^∞⟮I, M; 𝕜⟯ _ _ _
-- elaboration of bar took 3.34s

[Kevin Buzzard]

[class_instances] caching instance for comm_ring C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
@smooth_map_comm_ring 𝕜 _inst_1 E _inst_2 _inst_3 𝕜
  (@normed_ring.to_normed_group 𝕜
     (@normed_comm_ring.to_normed_ring 𝕜
        (@normed_field.to_normed_comm_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
  (@normed_field.to_normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))
  H
  _inst_4
  I
  𝕜
  (@uniform_space.to_topological_space 𝕜
     (@metric_space.to_uniform_space' 𝕜
        (@semi_normed_group.to_pseudo_metric_space 𝕜
           (@normed_group.to_semi_normed_group 𝕜
              (@normed_ring.to_normed_group 𝕜
                 (@normed_comm_ring.to_normed_ring 𝕜
                    (@normed_field.to_normed_comm_ring 𝕜
                       (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))
  𝓘(𝕜, 𝕜)
  M
  _inst_5
  _inst_6
  𝕜
  (@semi_normed_comm_ring.to_comm_ring 𝕜
     (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
        (@normed_field.to_normed_comm_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
  (@uniform_space.to_topological_space 𝕜
     (@metric_space.to_uniform_space' 𝕜
        (@semi_normed_ring.to_pseudo_metric_space 𝕜
           (@semi_normed_comm_ring.to_semi_normed_ring 𝕜
              (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                 (@normed_field.to_normed_comm_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
  (@charted_space_self 𝕜
     (@uniform_space.to_topological_space 𝕜
        (@metric_space.to_uniform_space' 𝕜
           (@semi_normed_group.to_pseudo_metric_space 𝕜
              (@normed_group.to_semi_normed_group 𝕜
                 (@normed_ring.to_normed_group 𝕜
                    (@normed_comm_ring.to_normed_ring 𝕜
                       (@normed_field.to_normed_comm_ring 𝕜
                          (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))))
  _

[Kevin Buzzard]

Hmm. Lean is looking for an is_scalar_tower instance. The type of the term that Lean is trying to find is here. It takes over 700 lines to write out with pp.all true. Let's call that term X.

The trace then looks like this:

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : X := @derivation.is_scalar_tower ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6 ?x_7 ?x_8 ?x_9 ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : X := @power_series.is_scalar_tower ?x_11 ?x_12 ?x_13 ?x_14 ?x_15 ?x_16 ?x_17 ?x_18 ?x_19 ?x_20
failed is_def_eq
[class_instances] (0) ?x_0 : X := @mv_power_series.is_scalar_tower ?x_21 ?x_22 ?x_23 ?x_24 ?x_25 ?x_26 ?x_27 ?x_28 ?x_29 ?x_30 ?x_31
failed is_def_eq
[class_instances] (0) ?x_0 : X := @continuous_multilinear_map.is_scalar_tower ?x_32 ?x_33 ?x_34 ?x_35 ?x_36 ?x_37 ?x_38 ?x_39 ?x_40 ?x_41 ?x_42 ?x_43  ?x_44  ?x_45  ?x_46  ?x_47  ?x_48  ?x_49  ?x_50  ?x_51  ?x_52  ?x_53  ?x_54  ?x_55  ?x_56  ?x_57  ?x_58  ?x_59
failed is_def_eq
[class_instances] (0) ?x_0 : X := @module.real_complex_tower ?x_60 ?x_61 ?x_62
failed is_def_eq
...

(fourteen of these, each taking up over 700 lines of output) until it finally finds @is_scalar_tower.of_ring_hom ?x_140 ?x_141 ?x_142 ?x_143 ?x_144 ?x_145 ?x_146 ?x_147 ?x_148 which it gets extremely excited about (spending well over 1000 lines of debugging output on, doing lots of hard work like finding comm_semiring instances on 𝕜 and linear_ordered_comm_ring instances and etc etc) until it eventually gives up on this, and we're back to

[class_instances] (0) ?x_0 : X := @is_scalar_tower.comap ?x_149 ?x_150 ?x_151 ?x_152 ?x_153 ?x_154 ?x_155 ?x_156
failed is_def_eq

(a reminder that each one of these lines with an X represents 715 lines of output). We then run into

[class_instances] (0) ?x_0 : X := @is_scalar_tower.right ?x_194 ?x_195 ?x_196 ?x_197 ?x_198

and Lean launches into this big search for a proof that 𝕜 is a normed field etc again, but this time it works out and Lean caches the term whose type is this gigantic X.

Ultimately this is a small number of attempts by the type class inference system (20 or so, not an unreasonable number) to find a term whose type is humungous in pp.all land, but I don't know whether that sort of thing affects speed in practice because I have no idea how type class inference actually works.

[Kevin Buzzard]

Making the following file on the command line

import geometry.manifold.algebra.smooth_functions
import ring_theory.derivation

open_locale manifold

variables {𝕜 : Type} [nondiscrete_normed_field 𝕜]
{E : Type} [normed_group E] [normed_space 𝕜 E]
{H : Type} [topological_space H] (I : model_with_corners 𝕜 E H)
(M : Type) [topological_space M] [charted_space H M]

set_option trace.class_instances true
structure test extends derivation 𝕜 C^∞⟮I, M; 𝕜⟯ C^∞⟮I, M; 𝕜⟯

and piping all output to a text file gives you an 11 megabyte text file. After 2 minutes it does succeed.

[Kevin Buzzard]

import geometry.manifold.algebra.smooth_functions
import ring_theory.derivation

open_locale manifold

variables {𝕜 : Type} [nondiscrete_normed_field 𝕜]
{E : Type} [normed_group E] [normed_space 𝕜 E]
{H : Type} [topological_space H] (I : model_with_corners 𝕜 E H)
(M : Type) [topological_space M] [charted_space H M]

namespace instances

def algebra : algebra 𝕜 C^∞⟮I, M; 𝕜⟯ := infer_instance -- instant

attribute [instance, priority 10000] algebra

def tower : is_scalar_tower 𝕜 C^∞⟮I, M; 𝕜⟯ C^∞⟮I, M; 𝕜⟯ := infer_instance -- instant

attribute [instance, priority 10000] tower

end instances

structure test extends derivation 𝕜 C^∞⟮I, M; 𝕜⟯ C^∞⟮I, M; 𝕜⟯

terminates in around 12 seconds on my machine

[Kevin Buzzard]

But def foo := derivation 𝕜 C^∞⟮I, M; 𝕜⟯ C^∞⟮I, M; 𝕜⟯ is essentially instant, so the issue really is with the structure command, meaning that I can't go any further.

[Nicolò Cavalleri]

Thank you very much Kevin for this answer, I am learning so much from it

[Kevin Buzzard]

Unfortunately I am not learning the answer to the problem

[Nicolò Cavalleri]

So first of all how did you locate that is_scalar_tower was the problem? I was looking at the output as well and I actually was doing ctrl+f to locate which instances were taking most of the lines, and I was also thinking it was probably is_scalar_tower but I was not sure because still the output file was huge and is_scalar_tower only appears in a small section of it

[Nicolò Cavalleri]

Kevin Buzzard said:

Unfortunately I am not learning the answer to the problem

As for why is there a bigger issue with the structure command?

[Nicolò Cavalleri]

Also what are the terms ?x_i exactly?

[Kevin Buzzard]

They're variables. Or, because Lean already has things which are called variables, it might be best to call them metavariables. They're terms whose values will be assigned later.

[Nicolò Cavalleri]

Ok and then what does failed is_def_eq mean? I mean how does it conclude things are not def_eq if they depend on metavariables that have not been assigned yet?

[Kevin Buzzard]

Lean knows that mul ?x_1 ?x_2 =?= add ?x_3 ?x_4 can't ever be true by definition, if mul is just defined to be a constant and add is defined to be a different constant.

[Nicolò Cavalleri]

Kevin Buzzard said:

Lean knows that mul ?x_1 ?x_2 =?= add ?x_3 ?x_4 can't ever be true by definition, if mul is just defined to be a constant and add is defined to be a different constant.

Oh I thought this was not our case because the type is is_scalar_tower on both sides but I guess the point here is that is_scalar_tower is a dependent type on other types and it is the other types that are different

[Nicolò Cavalleri]

Yeah it is kind of a miracle then that def tower : is_scalar_tower 𝕜 C^∞⟮I, M; 𝕜⟯ C^∞⟮I, M; 𝕜⟯ := infer_instance is instant... I am very puzzled

[Kevin Buzzard]

I don't know how definitional equality works but I can quite believe that there is an algorithm which allows there to be holes in the terms which are checked. For example

example : ∃ n, n = 37 :=
begin
  existsi _,
  /-
  ⊢ ?m_1 = 37

  ⊢ ℕ
  -/
  { -- ⊢ ?m_1 = 37
    refl },
  -- done
end

[Nicolò Cavalleri]

Btw on my machine it is still taking a long time (although much better than before) and another instance that is taking very long is output.txt

[Nicolò Cavalleri]

I don't know what size_of is, but is there a quick way to get a condensed expression of this type, like disableing pp_all a posteriori? There are too many parentheses for a human...

[Kevin Buzzard]

I don't think you're supposed to be messing with has_sizeof -- isn't this some internal thing?

[Nicolò Cavalleri]

Ok! Can you remind me how you trace time of things?

[Kevin Buzzard]

set_option profiler true

[Nicolò Cavalleri]

But can you read the output directly in visual studio? it tells me 0 messages...

[Eric Rodriguez]

it'll be hidden in All Messages

[Kevin Buzzard]

the profiler only works on stuff after the option has been set, and you can click on any blue underline to see output.

[Eric Rodriguez]

image.png

[Nicolò Cavalleri]

Immagine-2021-05-24-140614.png

[Nicolò Cavalleri]

Maybe does not work with structures?

[Kevin Buzzard]

I'm not sure the profiler runs on structures.

[Nicolò Cavalleri]

Ok I see thanks!

[Kevin Buzzard]

I have no idea what is happening when that structure is being made, or why it takes so long. We need help. You might want to promote this thread to #general where more experts are reading. Call it something like making new structure is slow

[Kevin Buzzard]

and just post the MWE

[Kevin Buzzard]

and a link to this thread

[Nicolò Cavalleri]

Well actually adding

def sizeof : has_sizeof (derivation 𝕜 C^∞⟮I, M; 𝕜⟯ C^⊤⟮I, M; 𝕜⟯) := infer_instance
attribute [instance, priority 100000] sizeof

to the namespace instances makes everything super quick

[Nicolò Cavalleri]

I don't need to repeat the section namespace instances in every file as long as I import a file where it is included right?

[Kevin Buzzard]

Those instances are a hack and are not for use in a production environment.

[Nicolò Cavalleri]

Kevin Buzzard said:

Those instances are a hack and are not for use in a production environment.

You mean I can't publish them to mathlib? Not even if I include everything in a section so to make it local?

[Notification Bot]

This topic was moved by Scott Morrison to #general > Tracing time of type class inference