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

[Sergei Meshveliani]

On Sun, 2016-07-17 at 21:13 +0200, Andreas Abel wrote:
> 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.
> 

And
  f : (A : Set)
      (a : A) → ℕ

  f _ _ = 0

is type-checked. 
Anyway, as it is intended, this is not important for me. 
If the thing is not parsed, I would add arrow.  

Regards,

------
Sergei