[Agda] fixity declarations and records: bug?

[Wolfgang Jeltsch]

Hello,

the following code is accepted by Agda 2.2.4:

> module Test where
>
>   open import Data.Unit
>
>   record R : Set₁ where
>
>     infixl 7 _*_
>     infixl 6 _+_
>
>     field
>       _+_ : Set → Set → Set
>       _*_ : Set → Set → Set
>       x : ⊤ + ⊤ * ⊤

Now I change it to the following:

> module Test where
>
>   open import Data.Unit
>
>   record R : Set₁ where
>
>     infixl 7 _*_
>     infixl 6 _+_
>
>     _+_ : Set → Set → Set
>     _+_ X Y = X
>
>     _*_ : Set → Set → Set
>     _*_ X Y = X
>
>     field
>       x : ⊤ + ⊤ * ⊤

Agda tells me that it cannot parse the type ⊤ + ⊤ * ⊤. It seems as if the 
fixity declarations for _+_ and _*_ wouldn’t be taken into account. Is this a 
bug?

Now I replace the line

>     _+_ X Y = X

by

>     X + Y = X

Now, Agda tells me that it cannot even parse the left-hand side X + Y, which 
surprises me. What surprises me even more is that Agda gives the Set₁ in the 
3rd non-empty line as the position of the error. Is this really correct? What 
have I missed?

Best wishes,
Wolfgang