Bug 779 [Re: [Agda] record syntax error]

[Andreas Abel]

This is a bug in Agda, I filed it as issue 779.

On 02.01.13 7:55 PM, Serge D. Mechveliani wrote:
> Please, what is wrong in the attached program?
>
> 123 lines code in  Main.agda.zip  is attached to this letter.
>
> This is for  Agda-2.3.2 made from source, MAlonzo, ghc-7.4.1.
>
> It looks like the responsible fragment is
> (with a couple of math symbols changed)
>
> ---------------------------------------------------------------
> record DMonoid (c l : Level) : Set (setoidLevel c l) where
>    field
>      semigroup : DSemigroup c l
>
>    private  M     = DSemigroup.magma semigroup
>             dS    = DSetoid.decSetoid $ Magma.setoid M
>             S     = DecSetoid.setoid dS
>             _*_   = Magma._*_ M
>             mbU   = Magma.mbLeftUnity M
>             justU = justLeftUnity mbU
>    field
>      hasUnity : justU === true
>
>    unity : LeftUnity S _*_
>    unity  with mbU | hasUnity
>    ...  | leftUnity u | _ = u
>    ...  | unknown     | ()
>
>    e : Setoid.Carrier S
>    e = LeftUnity.e unity
>
>    _~~_ = Setoid._~~_ S
>
>    field  foo : e ~~ (e * e)
> ---------------------------------------------------------------
>
> `field' is intermingled 3 times with defining values,
> the  foo  field uses  e,  and  e  is extracted from `unity',
> `unity'  is defined ealier in this record.
>
> The report is
> -----------------------------
> ...
> lation/Binary/InducedPreorders.agdai).
>     Skipping Data.Colist (/home/mechvel/agda/lib-0.6/src/Data/Colist.agdai).
>    Skipping Data.String (/home/mechvel/agda/lib-0.6/src/Data/String.agdai).
>   Skipping IO.Primitive (/home/mechvel/agda/lib-0.6/src/IO/Primitive.agdai).
>
> Missing definition for unity
> -----------------------------
>
> If we remove the line of  foo,  then the type checker becomes satisfied
> with the definition for `unity' (which, I think, is valid in both cases).
>
> I wonder of whether I am stuck by this effect.
>
> The code in  Main.agda  is contrived, obtained from the real one by
> removing its parts, as possible.
>
> Regards,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/