[Agda] type check with large constant

[Sergei Meshveliani]

Dear all,

I need to type-check a program that uses a certain large global constant
a.
And the function  test2  below is type-checked much longer than  test1,
It takes too long.
This is  Agda 2.5.3.

Can people, please, explain the effect?

--------------------------------------------------------------
open import Function using (_∘_; _$_)
open import Relation.Binary.PropositionalEquality using (_≡_; cong)
open import Data.Nat            using (ℕ; suc; _+_; _∸_)
open import Data.Nat.Properties using (+-comm)

a : ℕ
a = 12345

test1 :  ∀ n → (a + n) ∸ a ≡ (n + a) ∸ a
test1 n =  cong (_∸ a) (+-comm a n)

test2 :  ∀ n → suc ((a + n) ∸ a) ≡ suc ((n + a) ∸ a)
test2 n =  cong (suc ∘ (_∸ a)) (+-comm a n)

           -- cong suc (test1 n)
---------------------------------------------------------------

The interactive type-checker highlights the expression 
                     cong (suc ∘ (_∸ a)) (+-comm a n)

and hangs for a long time.

Also  test2  type-checks fast if it is implemented as  
cong suc (test1 n).

I can type-check the whole program with, say,  a = 7. 
But for a good run-time performance `a' needs to be large 
(and it relies on that the run-time arithmetic is built-in).

Thanks,

------
Sergei