[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).
> 
> -- Andreas


Meanwhile, can you tell about this signature?
I skip  `→'  after  (open OverIntegral...).
In some other situations this leads to parse error.
I doubt about using `open' this way.

------
Sergei
  

> On 15.07.2016 21:35, Sergei Meshveliani wrote:
> > 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
> >
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> 
>