[Agda] Possible bug when using "with" on a partially applied function

[Christopher Jenkins]

lpaste here: http://lpaste.net/114815

I am aware that a function generated by "with" is not always well-typed.
I'm to understand this is limited to cases where, for example, function foo
takes as its argument B (bar a), where a : A and B : A -> Set, and we have
rewritten "bar a" to some "w", but foo remains untouched (i.e. its external
to the context).

However, this is *not* that situation here. Agda has mysteriously eaten n :
Nat, and replaced its occurrences with a : A (a parametric type),
generating a type error. I can't imagine this is anything other than a bug,
but if it isn't I'd at least like to know the rationale behind this
behaviour.

Note that I am aware that this definition of "swap" is terrible. I was
playing with Agda to see if I could push it to see the function is
involutive even in such a situation when I encountered this.

Thanks.

-- 
Christopher Jenkins
Computer Science 2013
Trinity University
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141123/3dcafba8/attachment.html