[Agda] using inspect is tricky

[Florent Balestrieri]

Hello,

I have the following problem:

Given two functions `f' and `g' such that the type of `g x'
depend on the expression `f x'.

I'm defining a function `p':

> p x with f x | g x
>
> ... | .a | h a = ?

In the body, I need the equality proof that:

> f x == a

alas, I cannot manage to use inspect: it just won't be
instantiated, and I get:

> p x with f x | inspect (f x) | g x
>
> ... | .a | i | h a = ?

which is not very helpful.

I then tried to instantiate `g x' but for some typing reason,
agda refuses to inspect `g x' when `f x' is also in the
`with' clause (It is still a bit unclear why exactly).

That is, I can write

> p x with inspect (g x)

but not

> p x with f x | inspect (g x)

Many thanks for the helpful people here!
-- Florent