typeclass inference confusion

Stream: mathlib4

[Kevin Buzzard]

In the below snippet I have a ring R and a field K and I ask typeclass inference a question involving R and K. I also have a K-module V which is completely irrelevant to the question. To my surprise, typeclass inference's answer to the question involves V, and indeed one of the questions which typeclass inference spends the longest on involves V. My question is: how does typeclass inference even notice V? Note: my question is not "why oh why oh why does typeclass inference do this mathematically stupid thing" (the answer usually being "because this instance is being tried"), it is literally "how does typeclass inference even notice V's existence?" (i.e. "which instance is triggering this?"). I have unfolded everything and I cannot see what instance is triggering typeclass inference to even notice V. Should I be putting some other trace options on?

I ask because in my actual application typeclass inference gets totally bogged down in a completely irrelevant question of this nature and I would like to stop it doing this, but I cannot work out the underlying cause.

import Mathlib

universe uR uK uV

-- needed for `IsDedekindDomain.FiniteAdeleRing R K`
variable (R : Type uR) [CommRing R] [IsDedekindDomain R]
    (K : Type uK) [Field K] [Algebra R K] [IsFractionRing R K]

-- totally irrelevant
variable (V : Type uV) [AddCommGroup V] [Module K V]

open IsDedekindDomain

set_option trace.profiler true in
set_option trace.profiler.useHeartbeats true in
set_option trace.profiler.threshold 1 in
#synth Module (FiniteAdeleRing R K) (FiniteAdeleRing R K)
/-
[Elab.command] [3971649.000000] #synth Module (FiniteAdeleRing R K) (FiniteAdeleRing R K) ▼
  [step] [47.000000] expected type: Sort ?u.1038, term
      Type uR
  [step] [927.000000] expected type: Type uR, term
      CommRing R ▶
  [Meta.whnf] [21.000000] Non-easy whnf: CommRing R
  [step] [3073.000000] expected type: Prop, term
      IsDedekindDomain R ▶
  [Meta.whnf] [21.000000] Non-easy whnf: IsDedekindDomain R
  [step] [47.000000] expected type: Sort ?u.1055, term
      Type uK
  [step] [928.000000] expected type: Type uK, term
      Field K ▶
  [Meta.whnf] [21.000000] Non-easy whnf: Field K
  [step] [41214.000000] expected type: Type (max uK uR), term
      Algebra R K ▶
  [Meta.whnf] [21.000000] Non-easy whnf: Algebra R K
  [step] [42259.000000] expected type: Prop, term
      IsFractionRing R K ▶
  [Meta.whnf] [241.000000] Non-easy whnf: IsFractionRing R K ▶
  [Meta.whnf] [157.000000] Non-easy whnf: IsFractionRing R K ▶
  [Meta.whnf] [157.000000] Non-easy whnf: IsFractionRing R K ▶
  [step] [47.000000] expected type: Sort ?u.1252, term
      Type uV
  [step] [936.000000] expected type: Type uV, term
      AddCommGroup V ▶
  [Meta.whnf] [21.000000] Non-easy whnf: AddCommGroup V
  [step] [264769.000000] expected type: Type (max uV uK), term
      Module K V ▶
  [Meta.whnf] [21.000000] Non-easy whnf: Module K V
  [step] [219137.000000] expected type: <not-available>, term
      Module (FiniteAdeleRing R K) (FiniteAdeleRing R K) ▶
  [Meta.synthInstance] [3395634.000000] ✅️ Module (FiniteAdeleRing R K) (FiniteAdeleRing R K) ▶
-/

The thing that is bamboozling me is

  [step] [264769.000000] expected type: Type (max uV uK), term
      Module K V ▶

-- note that 264769.000000 is one of the biggest numbers in the trace.

[Ruben Van de Velde]

Curious. Can you then easily work around it with omit V in or similar?

[Kevin Buzzard]

No because it's happening in the middle of something else.

[Sébastien Gouëzel]

I think that in #synth it first resynthetizes everything in the variable lines before starting the real job. So I'm not sure what you see here is really relevant. Do you have a less minimal example?

[Jovan Gerbscheid]

As @Sébastien Gouëzel says, the Elab.step trace node that you are pointing out is that of elaborating the [Module K V] from the variable command, and is not part of the synthesis from the #synth command.

[Eric Wieser]

Does

noncomputable example : Module (FiniteAdeleRing R K) (FiniteAdeleRing R K) :=
  set_option trace.profiler.useHeartbeats true in
  set_option trace.profiler.threshold 1 in
  set_option trace.profiler true in
  inferInstance

avoid the issue?

[Eric Wieser]

(note that you want to turn the profiler on last to prevent it profiling the set_option commands)

[Kevin Buzzard]

Oh I remember seeing this before now! I think Sebastien even opened an issue about it. Thanks! I'll go back to my original problem with this in mind.