[Agda] `let' in function signature

[Sergei Meshveliani]

Please, what is wrong in the below program?

---------------------------------------------------------------
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Data.Nat using (ℕ; suc; pred; _*_; _^_)

postulate  anything : ∀ {a} {A : Set a} → A
postulate  pSum : ℕ → ℕ	→ ℕ

pSum-eq :  (q n : ℕ) → let q' = suc n
                       in
                       (pSum q' n) * q  ≡  pred (q' ^ (suc n))  -- (1)
pSum-eq 1 0 =  goal
               where
               postulate goal :  (pSum 2 0) * 1  ≡  pred (2 ^ 1)

pSum-eq _ _ =  anything
----------------------------------------------------------------

Agda 2.5.3  reports

  2 != 1 of type ℕ
  when checking that the expression goal has type
  pSum 1 ℕ.zero * 1 ≡ pred (1 ^ 1)

After replacing  q'  with  (suc q)  in the line (1), the type check
succeeds.

Is this a bug?

Regards,

------
Sergei