Dependent if expressions without dependent types

This post showcases a folklore trick for implementing code that seems like it should require dependent types without actually requiring dependent types. In fact, this trick works in any language with ...