[Agda] Path to success with Agda?

[Ignat Insarov]

Hello!

I have been trying to learn Agda time and again and I have not made much headway
yet. Once I stray a little aside from the happy path of _Programming Language
Foundations with Agda_, things start to get sour. Even the exercises in the book
give me a hard time whenever they let me a little freedom to get myself lost.

* You cannot always make cases for a given parameter. If you want to understand
  when you can and cannot make cases for a parameter, you have to read a thesis
  of the person that has written the pattern matching code.

* You cannot always have a with-abstraction — sometimes the auxiliary functions
  it compiles to do not type check. If you want to understand when you can and
  cannot make a with-abstraction, you only have the language reference to help
  you out, and it does not explain the problem in enough detail.

But there is nothing in the language to help me write proofs but pattern
matching and with-abstractions!

My first language is Haskell and it was a bit hard to learn, but there was the
amazing community to support my efforts. With Agda, the main venue seems to be
the Zulip chat, but it is more dead than alive. No one is rushing to explain
anything to me.

I have no problem learning Type Theory by itself, since there are great books
out there. Σ types, eliminators, you name it — no problem. My problem seems to
be rooted in the technical difficulties that are specific to Agda — the pattern
matching algorithm and the ill-typed with-abstractions.

Are there any success stories from people that did not learn Agda as a student
with the people that have written Agda itself or do research in Type Theory with
Agda or something to that end? I can see how someone might get good with Agda if
one is near to an expert, but doing it on my own seems to be a hard task. Ars
longa, vita brevis! What is the path I should take so that I get to write
realistic proofs and still have time left to enjoy the success?