Just reading chain of thought traces for Agda (I'm using Qwen 3.8-Flash-Next) and it's struggling so hard with just the syntax, long before it can struggle with semantics or type errors.
Admittedly I'm not much better, Agda has some crazy scoping rules at times and its operators are a mess, so much worse than Haskell, but at least I don't have to re-learn from scratch after every compaction.
No, Agda's mixfix operators and general syntactic malleability is state-of-the-art in programming language design. Try learning how to write it yourself, before relying on LLM to write it for you.
It's a cool hack. It's also a catastrophe for actual usage. State-of-the-art doesn't mean good, it just means new, shiny and complex. Not being able to do syntax highlighting without a full typechecking pass is a usability nightmare.
Anyway, that's not the part I the human struggle with, it's remembering what level of infix each new custom operator has. Why λ() isn't equivalent with λ{}, if `a b , c` is `(a b) , c` or `a (b , c)` with this version of comma (Though now I've given up on the others and just use Σ a (λ _ -> b) for all kinds of tuples just to make it consistent). Why implicits won't unify as I expect them to. Why with just doesn't work in a reasonable fashion at all ever beyond the most basic two cases (no nesting and only nest in the final case). Literally copy pasting from the docs doesn't parse.
Cool trick, but in practice it was a mistake and Haskell's take on custom operators was far enough.
Operator fixity is a non-issue; if you don't like how the fixities have been set up, you can change them at will, even in the middle of an `import` statement. Nobody is making you use custom infix operators, either; you can write Agda that looks mostly like a Lisp if you wish.
Improving `with` is ongoing work; there was a presentation on it at the recent Agda implementors' meeting.
There's real people with real feelings building Agda, and not very many of them either. Consider that before publicly denigrating their work, with such shallow criticism to boot.
Yeah I know this pain. I actually have had some success by giving the agent a style guide for Lean that is strictly not conventional. The nice syntactic shortcuts and different modes that make Lean more ergonomic for humans, in my experience, actually make it easier for an agent to trip itself up.
Admittedly I'm not much better, Agda has some crazy scoping rules at times and its operators are a mess, so much worse than Haskell, but at least I don't have to re-learn from scratch after every compaction.