Also "Wingman" for Haskell does some type-driven code generation. (It might be part of the haskell language server now, I get it when I use the vscode plugin.)

Also "Wingman" for Haskell does some type-driven code generation. (It might be part of the haskell language server now, I get it when I use the vscode plugin.) When the solution is ambiguous, Idris (and I believe wingman) will supply suggestions that you can pick from. In your `bar` case, `bar xs = 42` is also a solution. Idris suggests 0 1 2 3 ... I think, it's going off of the constructors for the return type. I expect this technology to improve over time (try to use arguments, etc.) Idris and Agda will also do stuff short of "fill in the answer" like "case split an argument for me" or "insert the appropriate constructor or lambda and leave a hole inside". This is quite helpful in cases where it's not gonna find the answer, but can type out the next step or two for you. (Wingman might have this, I haven't used it much. I don't know Coq at all.) On the Agda side, the first couple of sections of "Programming Language Foundations in Agda" will walk you through using that functionality. Idris has a couple of videos that others have pointed out. It's fun stuff.