[Agda] problem with `abstract'

[Andreas Abel]

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

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
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/