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

[Sergei Meshveliani]

On Sun, 2016-07-17 at 14:12 +0200, Andreas Abel wrote:
> 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.
> [..]

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.

* Changing the line (2) to  
                        (a : Carrier) → ℕ 
  makes it type-checked.
* Appending  ' →'  to the line (1)  makes it type-checked.

Regards,

------
Sergei