[Agda] problem with `abstract'

[Sergei Meshveliani]

On Sat, 2016-07-16 at 23:55 +0200, Andreas Abel wrote:
> Sorry, I cannot see off-hand where the problem is.  Please provide 
> some self-contained test (does not have to be minimal for now).
> 

-----------------------------------------------------------------
open import Data.Product  using (_×_; proj₂)
open import Data.List     using (List; []; map)
open import Data.List.All using (All) renaming ([] to []a)
open import Data.Nat      using (ℕ; _<_)

abstract
 f :  (A : Set) → A → ℕ
 f A a =  g nil seconds>0[]
   where
   Pair : Set
   Pair = A × ℕ

   nil : List Pair
   nil = []

   seconds>0[] :  All (_<_ 0) (map proj₂ nil)
   seconds>0[] =  []a

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

Agda 2.5.1.1 reports

home/mechvel/agda/tosave/bugs/july15-2016/Last.agda:16,42-45
Pair !=< (Data.Product.Σ (_A_16 A a) (λ _ → _B_13 A a))
of type Set
when checking that the expression nil has type
List (Data.Product.Σ (_A_16 A a) (λ _ → _B_13 A a))

With removed `abstract', it is type-checked.

Regards,

------
Sergei