In order to verify that a terminating program terminates, one thing that can be done is to actually run the program. That may take a lot of time. If the program is typed in a total type-system, we can instead just type-check the program. That will take some time too, sometimes "a lot" too.
I'm looking for results that formalize the relation of the complexity of type-checking to the complexity of normalization for a various type-systems, i.e. possible speedup ratios. Is that relation always well defined? I'm not sure.
But we can give some lower bounds by demonstrating families of typed terms.
I'm interested mostly in any of the well known type systems such as System F, predicative variants of system F, including 'Rank 1' variant and Calculus of constructions. 'Intersection types' are particularly interesting case since they characterize the family of normalizing lambda terms.