Excellent post on dependent types, why parametric polymorphism is good, and building inscrutable type checkers: https://ucsd-progsys.github.io/liquidhaskell-blog/2020/04/12/polymorphic-perplexion.lhs/