But there are a few languages that have both, such as Ur and Coq, and possibly others. Also, I know that there's work on a more powerful module system for Haske

But there are a few languages that have both, such as Ur and Coq, and possibly others. Also, I know that there's work on a more powerful module system for Haskell called Backpack (although, I'm not really familiar with it). I agree that there are certain conceptual incompatibilities between the two as you mention, but they're both so useful that it seems like there must be good ways to bring them together, or at least make both of them available.