[Agda] Odd `with' desugaring?

[Nils Anders Danielsson]

On 2009-12-20 02:26, Daniel Peebles wrote:
> This fails with:
>
> Dec (i' ≡ j) !=< Level of type Set
>
> on the i ≟ j line, supposedly in the `w' expression. I'm not really
> sure where `w' came from so I'm assuming it's from the desugaring of
> the with construct.

Right. It seems as if the auxiliary function generated by the with
machinery does not type check. This looks like a bug. Can you open a
ticket for it?

> As a workaround, if I manually make a q function that takes the Dec
> result of i ≟ j and matches on it, the whole thing works fine.

An easier option is perhaps to bind E in the top-level definition, so
you don't need to quantify over it in p.

--
/NAD