[Agda] arguments in `data' pattern

[Sergei Meshveliani]

Can anyone explain, please, 
what is the matter with the attached (small) code?

It includes

-----------------------------------------------------------------
data DecPrime : ℕ → Set      -- constructively decided primality 
     where
     prime    : {n : ℕ} → IsPrime n → DecPrime n
     unity    : DecPrime 1
     composed : {m n : ℕ} → IsNontrivialDivisor m n → DecPrime n

postulate  decPrime : (n : ℕ) → DecPrime n

f : ℕ → ℕ
f n = g n (decPrime n)
      where
      g : (m : ℕ) → DecPrime m → ℕ

      g 1 unity                = 1
      g _ (prime _)            = 2
      g _ (composed {k} {_} _) = k
------------------------------------------------------------------

This is on  Agda 2.4.2.3,  ghc-7.8.3.

The last pattern in  g  is not type-checked.
And if I remove  {_}  from it, then it is type-checked.
But `composed' has two implicit arguments. 

Does not this look strange? Can you, please, explain?

(the full code is attached).

Thanks,

------
Sergei
-------------- next part --------------
open import Level            using () renaming (zero to 0ℓ)
open import Function         using (case_of_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary  using (Rel)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
open import Data.Sum     using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃)
open import Data.Nat     using (ℕ; _*_)

------------------------------------------------------------------------------
_∣_ : Rel ℕ 0ℓ 
_∣_ m n =  ∃ \k → m * k ≡ n 

IsPrime : ℕ → Set
IsPrime p =  p ≢ 1  ×  (∀ {m n} → (m * n ≡ p) → m ≡ 1 ⊎ n ≡ 1)

¬prime-1 : ¬ IsPrime 1
¬prime-1 (1≢1 , _) =  1≢1 PE.refl

IsNontrivialDivisor : ℕ → ℕ → Set _
IsNontrivialDivisor m n =  m ≢ 1 × m ≢ n × m ∣ n

data DecPrime : ℕ → Set  
     where
     prime    : {n : ℕ} → IsPrime n → DecPrime n
     unity    : DecPrime 1
     composed : {m n : ℕ} → IsNontrivialDivisor m n → DecPrime n


to-Dec-IsPrime : ∀ {n} → DecPrime n → Dec (IsPrime n)  -- first test

to-Dec-IsPrime unity           =  no ¬prime-1
to-Dec-IsPrime (prime prime-n) =  yes prime-n
to-Dec-IsPrime (composed {m} {n} (m≢1 , m≢n , (q , mq≡n))) =  no ¬prime-n
   where
   postulate ¬prime-n : ¬ IsPrime n
 
postulate  decPrime : (n : ℕ) → DecPrime n 


f : ℕ → ℕ                             -- second test
f n = g n (decPrime n)
      where
      g : (m : ℕ) → DecPrime m → ℕ 

      g 1 unity                = 1
      g _ (prime _)            = 2
      g _ (composed {k} {_} _) = k