[Agda] complex indices

[Ramana Kumar]

Why exactly does this fail?
Should it?

data foo : (y : Bool) → if y then Set else Set where
  bar : foo true Bool

The error I get is

if @0 then Set else Set != Set of type Set₁
when checking the definition of foo

which is a little cryptic (but probably no more so than my declaration).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120222/e0bc5cef/attachment.html