[smallnamespace]

That's an interesting (and correct!) objection — in stats terms, it's the choice between having false positives (your type checker rejects some valid programs) vs. false negatives (Valgrind didn't catch these cases).

If you're writing safety-critical software though, being forced to restructure your code to satisfy the type checker (which, in this case, is kind of a simple proof assistant) seems like a sane tradeoff.