There was a research C compiler, maybe related to the meta-compilation effort that became Coverity, that did something like this. It let you attach arbitrary attributes to a variable and then enforce invariants regarding those attributes. The one that caught my eye was tagging checked vs. unchecked user input, so that using such input before checking (or sanitizing) would become a type error. It's a shame that the idea didn't catch on more.