parse error ? with open in telescope [Re: [Agda] problem with `abstract']

[Andreas Abel]

On 17.07.2016 10:58, Sergei Meshveliani wrote:
> 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.

If you encounter this parse error (you said "in other situations"), 
please alert us.

>> 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/