If the untyped language is terminating, can we still derive a contradiction from `Type : Type`?
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.