For a good article on the current state of play in Haskell, Richard Eisenberg’s thesis is very good – chapter 2 discusses a load of extensions of Haskell to enable type level programming. He also has a good series of blog posts on various Dependent Types aspects. There are a number of interesting YouTube videos too, including this one of using dependent types in a RegExp library.
At some level, the type checking becomes theorem proving. For the Idris language, there are slides from a talk on how this process happens, and there’s another phd thesis on type checking Haskell which discusses some of the trade offs.
While we are talking about type checking, there is a repository where the author is writing variants on Hindley-Milner type checking in F#. It’s a very interesting learning resource, as the examples are small enough to step in the debugger, so you can watch what happens when a let bound function is generalised by the system.