[Agda] Re: Help debugging

[Stefan Monnier]

> In cases like this one, where seemingly correct patterns are not
> accepted, it can be a good idea to let Agda write the patterns for you
> by using case-split.

In my case, the code started with a variable in place of "inHere" and it
"worked", and then I used case-split at which point the problem appeared.

> If you load this code you will see that Agda cannot infer the type of t.

Great, thanks.  Any hope to see the error message improved so that
I could have figured out that this was the problem?
E.g. it seems this error should be signalled right at the
type-declaration line

  problem : ∀{Δ τ Δ' t} → (P' : Extend (Δ :: τ) Δ') → t ∈ Δ' → ℕ

before Agda even tries to process the function's definition.


        Stefan