I would like to add some basic convenience features to Dafny, such as the ability to define set union in Dafny (see this question). But the internals of Dafny don't seem to be well documented and I don't know where to begin.
How can I add such a feature?
This is an excellent question. I'm not sure why it was downvoted. Thanks for asking. I wish I had known better where to look for information on its internals when I started getting into Dafny.
Rustan has many tutorials/papers/examples on how to use Dafny. (In fact, I would say we suffer slightly from an embarrassment of riches here, because there are so many resources spread over nearly a decade that it can be hard to know where to start. But that's a story for another day.) Also, Dafny is a living project: things change, and so some documents are out of date. You should just prepare yourself for this, and always be willing to open a new file and try things out in modern Dafny.
All that said, there are comparatively few resources about the internals of Dafny. The best way to proceed is to make sure you have a thorough understanding of the theory behind Dafny, and then just read the code. (It's quite good!) Here are some concrete pointers.
The Dafny Reference Manual is essentially an annotated description of the input grammar to Dafny. It was last edited in earnest about two years ago now, so some things are out of date, but it is still invaluable as a mostly exhaustive list of Dafny features. (Please file github issues if you find specific things missing, and we'll try to fix them.) I recommend reading it cover-to-cover.
Check out Rustan's summer school course that give a theoretical presentation of Dafny and Boogie. Also check out this earlier summer school course on Spec#, which, gets many of the same ideas across, but at a more leisurely pace.
Learn to program in Boogie.
Start with the (10 years old, but still 90% accurate) manual This is Boogie 2. Understanding Boogie deeply will help you see, by comparison, what Dafny brings to the table.
Ask Dafny to translate some examples to Boogie for you (using the command-line option /print:foo.bpl), and read the resulting Boogie code.
Read the Boogie test suite to see more examples. Start with the textbook directory. Ignore directories with interesting names.
Also check out this paper on Boogie's more-sophisticated-than-you-might-expect type system. (It goes beyond Hindley-Milner polymorphism!)
Learn at least a little bit about Z3.
Focus especially on how it uses triggers to handle quantifiers. A good introduction to the Dafny-level view of triggers is the paper Trigger Selection Strategies to Stabalize Automatic Program Verifiers.
Ask Boogie to translate some (small) examples to Z3 for you (using the command-line option /proverLog:foo.smt2), and read the resulting Z3 code. This is very hard, but worth it once or twice for your own edification. It can also be occasionally helpful during debugging.
Dig into the Dafny test suite.
Read tests. There are a lot of tests in the test suite, and in many cases is the only place to see a real, live, working example of some feature. If there are features that are not represented in the test suite, please file a Github issue, and we'll try to take care of it.
Learn to run the tests, so that you can test whether your improvements to Dafny break existing programs. (The basic idea is to install the lit testing tool and point it at the Test directory.)
Read the code.
main() for the command-line tool. Trace through and find the phases and read the ones you're interested in. Ask questions. Unfortunately, there's no great place for concrete, detailed questions about Dafny's internals. Stack Overflow isn't appropriate; neither is Github. Perhaps the best stop-gap is to file "request for documentation" issues on Github, and we'll see what we can do.
I'm hoping Rustan may chime in if there are things I missed.
Good luck, and in words of Rustan: Program Safely!
This page (scroll down to "Dafny") also links to some more papers on Dafny that you might find interesting.