Open
Description
We seem to be spending a lot of time when checking the well-formedness of the withFunType, the type of the generated with-function:
agda/src/full/Agda/TypeChecking/Rules/Def.hs
Lines 1207 to 1215 in 4e4a86e
Testcase seems to go up in time quadratic in n:
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
T : (n : Nat) (A B : Set) → Set
T zero A B = B
T (suc n) A B = A → T n A B
t : {A B : Set} (n : Nat) (b : B) → T n A B
t zero b = b
t (suc n) b = λ _ → t n b
n = 3000
k : {B : Set} (b : B) → T n Nat B
k b = t n b
thm : {A B : Set} (a b : B) (eq : a ≡ b) → k a ≡ k b
thm a b eq rewrite eq = refl