Curry-style typing and realizability make it sensible to allow a top type to type every term, even non-normalizing ones.