Slow TC for Module

Stream: mathlib4

[Tomas Skrivan]

I'm experiencing slow typeclass inference when using modules. In particular, opening lean namespace causes mysterious goal CoeFun Type ?m which fails and takes a long time.

mwe:

import Mathlib.Algebra.Module.Basic
import Mathlib.Analysis.Calculus.FDeriv.Basic

open Lean

set_option profiler true

def foo (R : Type _) [Ring R]
  {X : Type _} [AddCommGroup X] [Module R X]
  {X1 : Type _} [AddCommGroup X1] [Module R X1]
  {X2 : Type _} [AddCommGroup X2] [Module R X2]
  {X3 : Type _} [AddCommGroup X3] [Module R X3]
  {X4 : Type _} [AddCommGroup X4] [Module R X4]
  (x : X) : X := x

typeclass inference takes roughly 600ms on my machine.

The culprit is open Lean which causes the mysterious goal CoeFun Type ?m which fails and takes a long(ish) time. However, the import Mathlib.Analysis.Calculus.FDeriv.Basic makes it roughly 10x slower.

Any idea what is triggering CoeFun Type ?m? I was unable to decipher it from traces.

Tested on the latest commit cebb592 of mathlib4

[Yury G. Kudryashov]

docs#Lean.Module

[Yury G. Kudryashov]

It tries to interpret Module R X as Lean.Module R X. Since Lean.Module R is a Type, in order to apply it to X, it looks for CoeFun Type ?m.

[Yury G. Kudryashov]

If you import a large part of Mathlib, then it takes a long time to go over all possible branches.

[Tomas Skrivan]

:man_facepalming: ugh that is really unfortunate coincidence

[Tomas Skrivan]

Any tips on how I could have discovered it myself?

[Yury G. Kudryashov]

For me, the main tip was that open Lean makes elaboration of Module slow.

[Yury G. Kudryashov]

There were two possibilities: a strange instance and a name conflict.

[Yury G. Kudryashov]

open scoped Lean doesn't make it slow, so it's a name conflict.

[Tomas Skrivan]

Good to know, thanks!