Why exactly does this fail?<br>Should it?<br><br>data foo : (y : Bool) → if y then Set else Set where<br>  bar : foo true Bool<br><br>The error I get is<br><br>if @0 then Set else Set != Set of type Set₁<br>when checking the definition of foo<br>

<br>which is a little cryptic (but probably no more so than my declaration).<br>