I thought dependent types were types that depended on a value? What they are proposing are types that depend on types or compile time constants.