I program very often in idris2 and I cannot agree more. LLMs tend to take the least effort possible to the point where most of the time, llms are just not useful to program with dependent types. At least, not yet

Have you tried giving them the types you want and then have them auto complete? They are pretty good at a auto completing abstractions