Sure, that would be a good reason to go there. I didn't mean to cast aspersions at dependent types. I was just confused/amused at the typical case being cast as a hypothetical.