[Agda] fixity declarations and records: bug?

[Ulf Norell]

On Thu, Oct 1, 2009 at 1:53 AM, Wolfgang Jeltsch <g9ks157k at acme.softbase.org
> wrote:

> Hello,
>
> > 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?


The problem is that the only definitions you're allowed before the fields in
a record are definitions that could go in a let (at the moment, those are of
the form f x y z = ...). The reason for this is that records are modelled by
single constructor datatypes (with some eta rules) and so we need to be able
to construct the type of this constructor. In your example the type would be

  let _+_ : Set → Set → Set
      _+_ X Y = X

      _*_ : Set → Set → Set
      _*_ X Y = X
  in (x : ⊤ + ⊤ * ⊤) → R
Unfortunately you're not allowed fixity declarations in lets, which is why
it doesn't parse.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091001/5996132a/attachment.html