I'm not sure the exact approach, but there's definitely some heavy lifting. My understanding is that most (all?) dependently typed languages are essentially theorem provers at heart.

See my answer here: https://news.ycombinator.com/item?id=10856736

It should be able to use a Hindley-Milner algorithm.