[Agda] `data'-record field overlap

[Andreas Abel]

Data modules are always opened, so if you uncomment the first line, then 
the second definition of foo within record Foo2 creates ambiguity.

However, record modules are not opened by default.  If you squeeze "open 
Foo2" inbetween the two record declarations, you also get an error.

While constructors can be overloaded, fields cannot (yet).  However, I 
do not think we will add ambiguous identifiers like foo that can both 
denote a constructor and a field.

Cheers,
Andreas

On 10.11.12 12:18 PM, Serge D. Mechveliani wrote:
> People,
> the program
>
>    -- data   Foo1 : Set where foo : Bool -> Foo1
>    record Foo2 : Set where field foo : Bool
>    record Foo3 : Set where field foo : Bool
>
> is accepted in Agda-2.3.0.1.
> And un-commenting the first line yields the report of a multiple
> definition for  foo.
>
> May be this is natural.
> Anyway, is this a deliberate language restriction?
>
> Thanks,
>
> ------
> 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/