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

[Andreas Abel]

On 17.07.2016 15:23, Sergei Meshveliani wrote:
>
> The program
>
>    f :  ∀ {α α=} → (A : Setoid α α=) →
>                    (open Setoid A using (Carrier))      -- (1)
>                    Carrier → ℕ                          -- (2)
>    f _ _ = 0
>
>
> yields a parse error report in Agda 2.5.1.1.

Yes, but so would

   f : (A : Set)
       A -> A

so it is not different from

   g : (open M)
       A -> A

Both yield parse errors, and that is intended.


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