[Haskell-cafe] Non-atomic "atoms" for type-level programming

[Tillmann Rendel]

> - if type-level tags (such as 'data TTrue'/'data TFalse') are declared
>    repeatedly in separate modules, they represent separate types,
>    preventing shared use (your type-level predicate doesn't return
>    my version of 'TTrue'/'TFalse')

How is the need for a common import for 'data TTrue; data TFalse' 
different then the need for a common import for 'data Bool = True | False'?

Clearly, the advent of type-level programming necessitates the design of 
a type-level standard library, which provides standard abstractions to 
enable interoperation of custom libraries. But I don't see why the 
module system should not scale to type-level programming.

   Tillmann