[Agda] implicit parameters and 'with'

[Florent Balestrieri]

Hello,

I noticed a weird behaviour of the typechecker. If you
confirm that it is not right then I will take the time to
fill a bug report.

Here is the problem: when an expression is on the right hand
side of a function declaration, Agda doesn't have any trouble
filling the implicit variables ; but if I move that
expression on the left hand side, using the 'with' construct,
then Agda fails. The example is quite complex so I didn't
want to spend ages simplifying it in case the behaviour
turned out to be known.

All the best
-- Florent