A type-level program is still a program. Non-constructive proofs are addressing the question "will this program crash or go wrong if I extend it to do X, regardless of how I achieve that?", which is exactly the domain of type-level programming.