[Agda] stuck with "unsolved metas"

[Sergei Meshveliani]

Dear Agda developers,

I observe the following effect (in Agad 2.5.1, ghc-7.10.2).

----------------------------------------------------------------------------------
module _ {α α=} (upIR : UpIntegralRing α α=)
         (_∣?_ : let Mg = UpIntegralRing.*magma upIR
                 in  Decidable₂ $ Magma._∣_ Mg
         )
         (open OverIntegralRing-2 upIR _∣?_ using (Prime∣split))
         (prime∣split : Prime∣split)
  where
  open OverIntegralRing-0 upIR _∣?_ using (_∣'?_; *upCMon-NZ; 
                                                  *cancel-nz)
  open OverIntegralRing-2 upIR _∣?_ using (Prime∣split←→Prime∣split-nz)

  module NZ =  OfCancellativeCommMonoid-0 *upCMon-NZ *cancel-nz _∣'?_

  implic :  Prime∣split → NZ.Prime∣split
  implic =  proj₁ Prime∣split←→Prime∣split-nz

  debug :  NZ.Prime∣split
  debug =  implic prime∣split
----------------------------------------------------------------------------------


It reports  "unsolved metas"  for the last line.

Usually it helps adding implicit arguments. But not in this case:
  
    debug =  implic (\ {p a b} → prime∣split {p} {a} {b})

still leads to "unsolved metas" for this line.


Prime∣split  is declared in the two parameterized modules:

-------------------------------------
OverIntegralRing-2.Prime∣split =
                   ∀ {p a b} → IsPrime p → p ∣ (a * b) → p ∣ a ⊎ p ∣ b

NZ.Prime∣split =   ∀ {p a b} → IsPrime p → p ∣ (a ∙ b) → p ∣ a ⊎ p ∣ b
-------------------------------------

(IsPrime  is defined a bit differently in the second module, and _*_ is
replaced  _∙_).

These types are type-checked in the `implic' function.
But applying implic to a module parameter value is not type-checked.

Can you, please, advise?
May be, you can somehow guess. 

(The code is large. Many parameterized modules importing each other,
nested records, etc. Difficult to reduce.
)

Regards,

------
Sergei