If the untyped language is terminating, can we still derive a contradiction from `Type : Type`? Question

If a pure type system has a terminating proof language, can we have Type : Type at the logic level without causing paradoxes (i.e., without causing ∀ (x : *) -&gt; x to be inhabited)?

Example

Suppose we take a pure type theory such as the Calculus of Constructions, restrict functions to be affine (at most 1 variable uses) and add constructs for stratified duplications - see here for details. That language - which we could call EACC (Elementary Affine Calculus of Constructions) has a normalizing untyped fragment. That is, the reduction of any term - even ill-typed ones - is guaranteed to terminate due to the reduction rules (and, in particular, the restriction that duplicated terms can not change their levels).
The 'logic' of the contradiction with Type:Type is that you can create a term of any type including 'empty' type by 'cheating' by never returning. This is essentially the only way to cheat because of subject reduction and the subformula properties. 

Subject reduction states that evaluation of terms preserves their type.
If you have subject reduction and strong normalization (through whatever means), then you can infer that if you have a term of type T, you have a term of type T in a normal form - without any redexes (cuts) in it. 

You have to go over all your type rules and verify that all of them have subformula property except the cut rule (which normalization eliminates). 
I.e you have to verify that if one of the non-cut rules were to produce a term of type T then you'll have one of its premises produce the term of type T (perhaps somewhere deeper in the derivation tree).
AFAIK every good type system requires sub-formula property (I'd like to learn of examples that contradict it).

Since type derivations are supposed to be finite trees, and you have no axiom (0 premises) rule to introduce a term of an empty type, you can prove by induction that no tree can build a term of an empty type. 

To reiterate, the role of normalization is that cut rule does not have sub-formula property, so we have to eliminate it first while preserving the type of the term.

This is the general sketch of Gentzen's proofs of consistency of logics.