A mundane use of dependent types... I just tried to add an environment variable to Idris 2, and it wouldn't compile because I forgot to add it to the --help output.
*offers compiler a jelly baby*
That probably sounds like it'd be annoying, but it took about 20 seconds to fix, and it's not as annoying as forgetting the feature is there.
We always give talks that show off the fancy stuff. Maybe one day I should collect together all these everyday little things and talk about them instead.
I would need some new jokes to keep it interesting, I suppose.
