Coercion triggers timeout

Stream: mathlib4

[Michael Stoll]

I'm opening a new thread since the problem seems to be fairly unrelated to apply?. See #mathlib4 > apply? failure @ 💬 for the history.

import Mathlib.Data.Complex.Norm

set_option trace.profiler true
set_option trace.profiler.threshold 10

variable (x : ℝ) (z : ℂ)

-- this works fine:
#check (norm_add_le (x : ℂ) z : ‖x + z‖ ≤ ‖Complex.ofReal x‖ + ‖z‖)

-- this times out:
#check (norm_add_le (↑x) z : ‖x + z‖ ≤ ‖Complex.ofReal x‖ + ‖z‖)

In the linked thread, you can see how this comes up when using exact? or apply?, even when avoiding ↑x in the code.

It appears that lean gets lost in trying to unify @norm ℂ SeminormedAddGroup.toNorm (coming from docs#norm_add_le) and @norm ℂ Complex.instNorm, but for some strange reason only when I use ↑x and not (x : ℂ) or Complex.ofReal x.

[Michael Stoll]

A possibly more minimal version:

import Mathlib.Data.Complex.Norm

lemma test {α : Type*} [Norm α] (a b : α) : ‖a‖ = ‖b‖ := sorry

variable (x : ℝ) (z : ℂ)

#count_heartbeats in -- Used 34 heartbeats
#check test (↑x) z

#count_heartbeats in -- Used 34 heartbeats
#check test (x : ℂ) z

#count_heartbeats in -- Used 41 heartbeats
#check (test (x : ℂ) z : ‖Complex.ofReal x‖ = ‖z‖)

#count_heartbeats in -- Used 217827 heartbeats
#check (test (↑x) z : ‖Complex.ofReal x‖ = ‖z‖)

seal Real.sqrt in
#count_heartbeats in -- Used 114 heartbeats
#check (test (↑x) z : ‖Complex.ofReal x‖ = ‖z‖)

In the second example, lean seems to introduce a metavariable for (↑x) that stays unassigned apparently until the very end, and it keeps unfolding definitions, in particular of the norm on the complex numbers. sealing docs#Real.sqrt stops this (compare docs#Complex.instNorm -- the definition is Real.sqrt (Complex.normSq z)) and makes it almost as fast as with the explicit type ascription.

In #24752, I'm trying to see what the fallout is when I make docs#Real.sqrt irreducible.

[Michael Stoll]

There are no big changes; overall build needs about 50 fewer Giga-instructions.

[Michael Stoll]

But somehow my impression is that this is a work-around and not a fix.
With

set_option trace.profiler true
set_option trace.profiler.threshold 0
set_option pp.all true

building the test file and looking at the output, I see several (13, to be precise) occurrences of

            [Meta.isDefEq] [0.00000...] ❌️ Complex.ofReal x =?= ?m.526

and I am wondering why at this point the metavariable ?m.526 does not get assigned to Complex.ofReal x (if it did, the whole going down rabbit holes by unfolding would be avoided).

[Michael Stoll]

Note that what happens is roughly this (many intermediate lines omitted and without pp.all):

      [Meta.isDefEq] [0.001783] ❌️ ‖↑x‖ = ‖z‖ =?= ‖?m.526‖ = ‖z‖
            [Meta.isDefEq] [0.000002] ❌️ ↑x =?= ?m.526
          [Meta.isDefEq] [0.001702] ❌️ Complex.instNorm.1 ↑x =?= Complex.instNorm.1 ?m.526
            [Meta.isDefEq] [0.001668] ❌️ √(Complex.normSq ↑x) =?= √(Complex.normSq ?m.526)
              [Meta.isDefEq] [0.001642] ❌️ Complex.normSq ↑x =?= Complex.normSq ?m.526
                  [Meta.isDefEq] [0.000002] ❌️ ↑x =?= ?m.526
                [Meta.isDefEq] [0.001546] ❌️ MonoidWithZeroHom.funLike.1 Complex.normSq
                      ↑x =?= MonoidWithZeroHom.funLike.1 Complex.normSq ?m.526
                  [Meta.isDefEq] [0.001479] ❌️ (↑Complex.normSq).toFun ↑x =?= (↑Complex.normSq).toFun ?m.526
                      [Meta.isDefEq] [0.000002] ❌️ ↑x =?= ?m.526
                    [Meta.isDefEq] [0.001420] ❌️ (↑Complex.normSq).1 ↑x =?= (↑Complex.normSq).1 ?m.526
                      [Meta.isDefEq] [0.001352] ❌️ (↑x).re * (↑x).re +
                            (↑x).im *
                              (↑x).im =?= Complex.re ?m.526 * Complex.re ?m.526 + Complex.im ?m.526 * Complex.im ?m.526
                          [Meta.isDefEq] [0.000366] ❌️ (↑x).re * (↑x).re =?= Complex.re ?m.526 * Complex.re ?m.526
                              [Meta.isDefEq] [0.000072] ❌️ (↑x).re =?= Complex.re ?m.526
                                  [Meta.isDefEq] [0.000002] ❌️ ↑x =?= ?m.526
                            [Meta.isDefEq] [0.000243] ❌️ instHMul.1 (↑x).re
                                  (↑x).re =?= instHMul.1 (Complex.re ?m.526) (Complex.re ?m.526)
                              [Meta.isDefEq] [0.000202] ❌️ Mul.mul (↑x).re
                                    (↑x).re =?= Mul.mul (Complex.re ?m.526) (Complex.re ?m.526)
                                      [Meta.isDefEq] [0.000001] ❌️ ↑x =?= ?m.526
                                [Meta.isDefEq] [0.000121] ❌️ Real.instMul.1 (↑x).re
                                      (↑x).re =?= Real.instMul.1 (Complex.re ?m.526) (Complex.re ?m.526)
                                  [Meta.isDefEq] [0.000092] ❌️ Real.mul✝ (↑x).re
                                        (↑x).re =?= Real.mul✝ (Complex.re ?m.526) (Complex.re ?m.526)
                                    [Meta.isDefEq] [0.000065] ❌️ (↑x).re =?= Complex.re ?m.526
                                        [Meta.isDefEq] [0.000001] ❌️ ↑x =?= ?m.526
                        [Meta.isDefEq] [0.000813] ❌️ instHAdd.1 ((↑x).re * (↑x).re)
                              ((↑x).im *
                                (↑x).im) =?= instHAdd.1 (Complex.re ?m.526 * Complex.re ?m.526)
                              (Complex.im ?m.526 * Complex.im ?m.526)
(...)
              [Meta.isDefEq.onFailure] [0.000002] ❌️ √(Complex.normSq ↑x) =?= √(Complex.normSq ?m.526)
        [Meta.isDefEq.onFailure] [0.000002] ❌️ ‖↑x‖ = ‖z‖ =?= ‖?m.526‖ = ‖z‖
    [Meta.isDefEq] [0.000859] ❌️ ‖?m.526‖ = ‖z‖ =?= ‖↑x‖ = ‖z‖
      [Meta.isDefEq] [0.000835] ❌️ ‖?m.526‖ =?= ‖↑x‖
          [Meta.isDefEq] [0.000002] ❌️ ?m.526 =?= ↑x
        [Meta.isDefEq] [0.000812] ❌️ Complex.instNorm.1 ?m.526 =?= Complex.instNorm.1 ↑x
          [Meta.isDefEq] [0.000804] ❌️ √(Complex.normSq ?m.526) =?= √(Complex.normSq ↑x)
            [Meta.isDefEq] [0.000788] ❌️ Complex.normSq ?m.526 =?= Complex.normSq ↑x
                [Meta.isDefEq] [0.000001] ❌️ ?m.526 =?= ↑x
              [Meta.isDefEq] [0.000764] ❌️ MonoidWithZeroHom.funLike.1 Complex.normSq
                    ?m.526 =?= MonoidWithZeroHom.funLike.1 Complex.normSq ↑x
(...)
            [Meta.isDefEq.onFailure] [0.000002] ❌️ √(Complex.normSq ?m.526) =?= √(Complex.normSq ↑x)
      [Meta.isDefEq.onFailure] [0.000002] ❌️ ‖?m.526‖ = ‖z‖ =?= ‖↑x‖ = ‖z‖

(sealing docs#Real.sqrt prevents it from also unfolding square roots all the way down...)

[Michael Stoll]

Then it goes on a tangent starting with

    [Elab.coe] [0.001073] adding coercion for test ?m.526 z : ‖?m.526‖ = ‖z‖ =?= ‖↑x‖ = ‖z‖
      [Meta.isDefEq] [0.000812] ❌️ Eq ‖?m.526‖ =?= Eq ‖↑x‖
        [Meta.isDefEq] [0.000788] ❌️ ‖?m.526‖ =?= ‖↑x‖
            [Meta.isDefEq] [0.000001] ❌️ ?m.526 =?= ↑x
          [Meta.isDefEq] [0.000770] ❌️ Complex.instNorm.1 ?m.526 =?= Complex.instNorm.1 ↑x
            [Meta.isDefEq] [0.000764] ❌️ √(Complex.normSq ?m.526) =?= √(Complex.normSq ↑x)
              [Meta.isDefEq] [0.000747] ❌️ Complex.normSq ?m.526 =?= Complex.normSq ↑x
                  [Meta.isDefEq] [0.000001] ❌️ ?m.526 =?= ↑x
(... repeating its fruitless endeavors)
              [Meta.isDefEq.onFailure] [0.000002] ❌️ √(Complex.normSq ?m.526) =?= √(Complex.normSq ↑x)
        [Meta.isDefEq.onFailure] [0.000002] ❌️ Eq ‖?m.526‖ =?= Eq ‖↑x‖
      [Meta.synthInstance] [0.000207] 💥️ CoeT (‖?m.526‖ = ‖z‖) ⋯ (‖↑x‖ = ‖z‖)
        [Meta.synthInstance] [0.000027] new goal CoeT (‖?m.526‖ = ‖z‖) ⋯ (‖↑x‖ = ‖z‖)
        [Meta.synthInstance] [0.000145] 💥️ apply @instCoeT to CoeT (‖?m.526‖ = ‖z‖) ⋯ (‖↑x‖ = ‖z‖)
          [Meta.synthInstance.tryResolve] [0.000126] 💥️ CoeT (‖?m.526‖ = ‖z‖) ⋯ (‖↑x‖ = ‖z‖) ≟ CoeT ?m.601 ?m.602 ?m.601
            [Meta.isDefEq] [0.000122] 💥️ CoeT (‖?m.526‖ = ‖z‖) ⋯ (‖↑x‖ = ‖z‖) =?= CoeT ?m.601 ?m.602 ?m.601

[Michael Stoll]

@Jovan Gerbscheid @Matthew Ballard any ideas as to whether this is expected or possibly a bug? I have no idea how unification works in detail, but my naive expectation would be that when the question is whether I can unify a metavariable with a concrete term, then the answer should certainly be "yes".

[Kevin Buzzard]

Yes I am also surprised by this (in the test file above, with pp.all on):

    [Meta.isDefEq] [3.452198] ❌️ @Eq.{1} Real (@Norm.norm.{0} Complex Complex.instNorm ?m.367)
          (@Norm.norm.{0} Complex Complex.instNorm
            z) =?= @Eq.{1} Real (@Norm.norm.{0} Complex Complex.instNorm (Complex.ofReal x))
          (@Norm.norm.{0} Complex Complex.instNorm z) ▶

You would have thought that there was a pretty obvious answer to this...

[Kevin Buzzard]

It doesn't like the answer for some reason...

      [] [3.452163] ❌️ @Norm.norm.{0} Complex Complex.instNorm
            ?m.367 =?= @Norm.norm.{0} Complex Complex.instNorm (Complex.ofReal x) ▼
        [delta] [0.000008] ❌️ @Norm.norm.{0} Complex Complex.instNorm
              ?m.367 =?= @Norm.norm.{0} Complex Complex.instNorm (Complex.ofReal x) ▼
          [] [0.000003] ❌️ ?m.367 =?= Complex.ofReal x

[Aaron Liu]

Maybe it's not assignable yet?

[Jovan Gerbscheid]

Yes, the metavariable is not assignable:

  [] [5.900020] ❌️ ‖↑x‖ =?= ‖?m.367‖ ▼
    [] [0.000006] ❌️ ↑x =?= ?m.367 ▼
      [] ↑x [nonassignable] =?= ?m.367 [nonassignable]

I'd guess is that this is by design: whenever you write the ↑x, Lean is only allowed to fill in the arrow by synthesizing the coercion instance.

[Jovan Gerbscheid]

And the slowness in unification is the same as in #mathlib4 > simp timeout at `whnf` @ 💬: exponentially slow unification in the presence of metavariables.

[Jovan Gerbscheid]

Since this unification slowness seems to be quite common, I made a small minimal example. It takes about 6s to fail, and this time is exponential in the number that I set to 15.

class A (n : Nat) where
  x : Nat

instance [A n] : A (n+1) where
  x := A.x n

theorem test [A 0] : A.x 15 = sorry := sorry

set_option trace.profiler true in
example [A 1] : A.x 15 = sorry := by
  rw [@test]

[Michael Stoll]

Jovan Gerbscheid said:

I'd guess is that this is by design: whenever you write the ↑x, Lean is only allowed to fill in the arrow by synthesizing the coercion instance.

But at that point, we are already dealing with Complex.ofReal x, so it is clear what the coercion is?

[Jovan Gerbscheid]

The unification algorithm doesn't know anything about coercions. So it has to be filled in by a type class search.

[Michael Stoll]

What I was trying to say is that

[Meta.isDefEq] [0.00000...] ❌️ Complex.ofReal x =?= ?m.526

does not involve a coercion (as far as I understand it): the left hand side is the application of an explicit function to an explicit variable.

[Michael Stoll]

Another observation is that parts of the trace are repeated several times (partly with sides switched), so it appears that very possibly something could be gained by caching the failures.

[Jovan Gerbscheid]

Yes, but the right hand side represents the expression ↑x. Apparently this how Lean implements the ↑: replace the entire expression with an unassignable metavariable. And later fill it in.

[Michael Stoll]

Here is a #mwe without using type classes.

def g {α : Type} (a : α) : Nat → Nat
| 0 => 0
| n + 1 => g a n

theorem foo {α : Type} (a b : α) : g a 1000 = g b 1000 := sorry

variable (x : Nat) (y : Int)

set_option maxRecDepth 2000 -- otherwise error in the second #check below

set_option trace.profiler true
set_option trace.profiler.threshold 0

#check (foo (x : Int) y : g (x : Int) 1000 = g y 1000)

#check (foo (↑x) y : g (x : Int) 1000 = g y 1000)

[Michael Stoll]

The first #check gives this trace:

[Elab.command] [0.004925] #check (foo (x : Int) y : g (x : Int) 1000 = g y 1000) ▼
  [step] [0.000174] expected type: Type, term
      Nat ▶
  [step] [0.000087] expected type: Type, term
      Int ▶
  [step] [0.004360] expected type: <not-available>, term
      (foo (x : Int) y : g (x : Int) 1000 = g y 1000) ▼
    [] [0.003584] expected type: Sort ?u.281, term
        g (x : Int) 1000 = g y 1000 ▶
    [] [0.000657] expected type: g (↑x) 1000 = g y 1000, term
        foo (x : Int) y ▶
    [Meta.isDefEq] [0.000056] ✅️ g (↑x) 1000 = g y 1000 =?= g (↑x) 1000 = g y 1000 ▼
      [] [0.000002] ✅️ g (↑x) 1000 =?= g (↑x) 1000       [] [0.000001] ✅️ g y 1000 =?= g y 1000       [] [0.000001] ✅️ Nat =?= Nat       [isLevelDefEq] [0.000000] ✅️ 0 =?= 0
  [Meta.check] [0.000095] ✅️ foo (↑x) y ▶

[Michael Stoll]

The second one gives

[Elab.command] [0.095349] #check (foo (↑x) y : g (x : Int) 1000 = g y 1000) ▼
  [step] [0.000106] expected type: Type, term
      Nat ▶
  [step] [0.000055] expected type: Type, term
      Int ▶
  [step] [0.094532] expected type: <not-available>, term
      (foo (↑x) y : g (x : Int) 1000 = g y 1000) ▼
    [] [0.003083] expected type: Sort ?u.342, term
        g (x : Int) 1000 = g y 1000 ▶
    [] [0.052486] expected type: g (↑x) 1000 = g y 1000, term
        foo (↑x) y ▶
    [Meta.isDefEq] [0.038652] ✅️ g ?m.395 1000 = g y 1000 =?= g (↑x) 1000 = g y 1000 ▼
      [] [0.038588] ✅️ g ?m.395 1000 =?= g (↑x) 1000 ▼
        [delta] [0.000011] ❌️ g ?m.395 1000 =?= g (↑x) 1000 ▶
        [whnf] [0.000033] Non-easy whnf: (fun motive x h_1 h_2 ↦ Nat.casesOn x (h_1 ()) fun n ↦ h_2 n) (fun x ↦ Nat) 1000 h_1 h_2         [whnf] [0.000011] Non-easy whnf: (fun motive x h_1 h_2 ↦ Nat.casesOn x (h_1 ()) fun n ↦ h_2 n) (fun x ↦ Nat) 1000 h_1 h_2
        [] [0.038467] ✅️ g ?m.395 999 =?= g (↑x) 999 ▼
          [delta] [0.000005] ❌️ g ?m.395 999 =?= g (↑x) 999 ▶
          [whnf] [0.000010] Non-easy whnf: (fun motive x h_1 h_2 ↦ Nat.casesOn x (h_1 ()) fun n ↦ h_2 n) (fun x ↦ Nat) 999 h_1 h_2           [whnf] [0.000009] Non-easy whnf: (fun motive x h_1 h_2 ↦ Nat.casesOn x (h_1 ()) fun n ↦ h_2 n) (fun x ↦ Nat) 999 h_1 h_2
          [] [0.038418] ✅️ g ?m.395 998 =?= g (↑x) 998 ▶
      [] [0.000004] ✅️ g y 1000 =?= g y 1000       [] [0.000000] ✅️ Nat =?= Nat       [isLevelDefEq] [0.000000] ✅️ 0 =?= 0
  [step] [0.000173] expected type: Int, term
      ↑x ▶
  [Meta.isDefEq] [0.000000] ✅️ Int =?= Int
  [Meta.check] [0.000031] ✅️ foo (↑x) y ▶

it unfolds the definition of g until the very end (when it succeeds, but only because g a n does not actually depend on a or n).

[Michael Stoll]

At the point where we try to unify (say) Complex.ofReal x with the metavariable representing ↑x, we know what type ↑x is supposed to have. So it should be possible to synthesize the relevant coercion instance at that point and thus fill in the arrow.

[Jovan Gerbscheid]

In your example, the second #check isn't significantly slower than the first, so I think it's not such a big deal. I think the real problem is the exponentially slow unification.

[Michael Stoll]

It's a toy example, and it is still 20 times slower, and increasing 1000 to 10000 or so gives a stack overflow. But you are certainly right that exponentially slow unification is a problem.

[Jovan Gerbscheid]

When I change the 1000 to a 2000, the two #check are similarly slow

[Michael Stoll]

You have to change all 1000 to 2000. On the web server, I then get

[Elab.command] [0.008249] #check (foo (x : Int) y : g (x : Int) 2000 = g y 2000)
[Elab.command] [0.367612] #check (foo (↑x) y : g (x : Int) 2000 = g y 2000)

(with set_option maxRecDepth 5000; otherwise the second check gives an error.)

[Jovan Gerbscheid]

Ah sorry, my mistake

[Michael Stoll]

What is the rationale for making the metavariable that stands for the coerced value unassignable?

[Jovan Gerbscheid]

If it were assignable, then it could be assigned anyhting; e.g. something other than a coercion. But I'm just guessing about these implementation details

[Michael Stoll]

In the context of my earlier Mathlib example, consider:

import Mathlib.Data.Complex.Norm

lemma test {α : Type*} [Norm α] (a b : α) : ‖a‖ = ‖b‖ := sorry

variable (x : ℝ) (z : ℂ)

#count_heartbeats in -- Used 217734 heartbeats
#check (test (↑x) z : ‖Complex.ofReal x‖ = ‖z‖)

#count_heartbeats in -- Used 40 heartbeats
#check (test z (↑x) : ‖z‖ = ‖Complex.ofReal x‖)

The difference is that in the first case, the expected type of ↑x is still a metavariable when the expression left of the colon is elaborated, whereas in the second case, it is already known to be ℂ, which leads to the coercion being looked for and found at this point, and then unification is basically trivial. In the first case, we still have the unassignable metavariable ?m.abcfor ↑x in the mix when the expression left of the colon is elaborated with the expected type given, which leads to the frantic, but eventually unsuccessful attempt to unify ‖?m.abc‖ with ‖Complex.ofReal x‖. At this point the expected type of ?m.abc is known to be ℂ, but this does not help.

I'm wondering whether it might by possible to detect this situation (this may involve remembering that the unassignable metavariable came from a coercion) and then re-elaborate the coercion with its then known expected type before proceeding.

I think I will open a thread in the lean4 channel for this (later; I have other obligations now).

[Michael Stoll]

If you have observed apply? or exact? timing out (or taking a very long time) unexpectedly, this may be related to what is described in this thread, and so you may want to up-vote the issue I created for this: lean4#8364