[Agda] Path to success with Agda?

[Ignat Insarov]

Cool, let us dig in!

> If you ignore some bugs in the pattern matcher (which you might well bump
> into), from my learning experience, I think it is the best to learn why Agda
> refuses your pattern by writing out a helper function supposedly generated by
> the pattern matcher and with-patterns; recall that this is also how Agda
> handles it after all (at least this is how the doc phrases it). By writing a
> helper out, you might obtain some information about why Agda rejects you, or
> you might just succeed. The latter case could mean that you just phrased a
> smarter helper than Agda could, or you worked around an Agda bug.

I am all for it, but how do I write such a helper? I tried to follow the
language reference, but it does not make sense. It reads more like a remainder
for someone who is already familiar with the principles, than as an
introduction.

> To answer your questions directly, if a case split fails, it is likely that
> the variable you are splitting is depended on by some other type, which
> triggers some further mechanisms that eventually fails the case split. Another
> common possibility is that you turned on without-K, but your case split
> effectively is doing that. This case can be checked by observing whether a
> case split will cause unification of the same variable.

What do you mean when you say _«a case split will cause unification of the same
variable»_?

> If your with-pattern fails, it could mean that you are not generalizing
> enough. For example, if you are with-patterning a term of type (foo bar) and
> it fails, it might be fixed by generalizing bar before (foo bar), which causes
> both bar and (foo bar) being abstracted and thus making the Typechecker happy.

What does it mean to _«generalize»_ here? Following your example, how would a
generalized _bar_ look? What does it mean for _bar_ and _foo bar_ to be
abstracted? How does this help with type checking?