[Agda] Re: `data'-record field overlap

[Francesco Mazzoli]

At Sat, 10 Nov 2012 15:18:16 +0400,
Serge D. Mechveliani wrote:
> 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?

Looks like a bug, you don't need records or data.  This works:

    module Foo where
      foo : Bool
      foo = true

    foo : Bool
    foo = true

This doesn't:    

    foo : Bool
    foo = true

    module Foo where
      foo : Bool
      foo = true

Francesco