[Agda] problem with `abstract'

[Sergei Meshveliani]

Dear Agda developers,

the following usage of `abstract' is not type-checked in 
Agada 2.5.1.1 + ghc-7.10.2 : 

-----------------------------------------------------------------------
open import Relation.Binary using () renaming (Decidable to Decidable₂)
open import Data.Product    using (_×_; proj₂)
open import Data.List       using (List; map)
open import Data.List.All   using (All) 
open import Data.Nat as Nat using (ℕ; _<_)

-- of appliaction --       
open import Structures0 using (Magma)
open import Structures3 using (UpIntegralRing)
open import Structures7 using (module OverIntegralRing-3)

abstract 
 f : ∀ {α α=} → 
     (upIR : UpIntegralRing α α=) → 
     (open UpIntegralRing upIR using (Carrier; 1#; *magma))
     (_∣?_ : Decidable₂ (Magma._∣_ *magma)) →  
     (open OverIntegralRing-3 upIR _∣?_ using (Factorization))   

     (a : Carrier) → Factorization a → Carrier 

 f {α} {_} upIR _∣?_ a ft =  g (ftPairs ft) (exps>0 ft)
   where
   open UpIntegralRing     upIR      using (Carrier; 1#)        
   open OverIntegralRing-3 upIR _∣?_ using (Factorization)
   open Factorization                using (ftPairs; exps>0) 

   Pair : Set α 
   Pair = Carrier × ℕ

   g :  (pairs : List Pair) → All (_<_ 0) (map proj₂ pairs) → Carrier
   g _ _ =  1# 
----------------------------------------------------------------------

The report is

------------------
/home/mechvel/agda/tosave/bugs/july15-2016/Last.agda:31,54-59
Pair !=<
(Data.Product.Σ (_A_39 upIR _∣?_ a ft pairs)
 (λ _ → _B_36 upIR _∣?_ a ft pairs))
of type (Set α)
when checking that the expression pairs has type
List (Data.Product.Σ (_A_39 upIR _∣?_ a ft pairs)
 (λ _ → _B_36 upIR _∣?_ a ft pairs))
-------------------


* With `abstract' removed, it is type-checked.
* With "List Pair"  replaced with  "List (Carrier × ℕ)",  
  it is type-checked.
* With removing the second argument from the signature of  g,
  it is type-checked.

Is this a bug?
Do I need to provide a self-contained code 
(reduction needs a certain effort),
or may be, you already guess what is the matter? 

Regards,

------
Sergei