slow overloaded notation

Stream: lean4

[Mario Carneiro]

import Mathlib.Data.Matrix.Notation

def prop := Nat
infixr:40 " ⇒ " => Nat.add
def minImp (φ ψ χ θ τ : prop) : prop := φ ⇒ (ψ ⇒ χ) ⇒ ((θ ⇒ ψ) ⇒ χ ⇒ τ) ⇒ ψ ⇒ τ
-- 3.05 sec

The imports seem to make a difference, and my guess is that this has something to do with the fact that this notation is also defined in Mathlib.Logic.Relation. Could this also be related to example (p : P) : Q := p takes 0.25s to fail!?