<br><div class="gmail_quote">On Thu, Oct 29, 2009 at 7:51 PM, Vag Vagoff <span dir="ltr"><<a href="mailto:vag.vagoff@gmail.com">vag.vagoff@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
module Bug where<br>
<br>
data Type : Set where value : Type<br>
data Test (h : Type) (h : Type) : Set where -- duplicate names [!]<br>
tst : Test _ _<br>
test : Test value value<br>
test = tst<br>
<br>
This source typechecks. Is it intended compiler behaviour?<br></blockquote><div><br></div><div>That's how it works at the moment. There's a discussion on shadowing in this issue on the bug tracker:</div><div><br>
</div><div><a href="http://code.google.com/p/agda/issues/detail?id=30">http://code.google.com/p/agda/issues/detail?id=30</a></div><div><br></div><div>Feel free to add comments to it.</div><div><br></div><div>/ Ulf</div></div>