Typed lambda calculus, recursion and halting

I am implementing a type system for a Turner style combinator graph

reduction system, based on Turner's paper

"A New Implementation Technique For Applicative Languages"

and was working through Roger Hindley's book "Basic Simple Type Theory".

He proves the Weak Normalization Theorem, that every typable lambda calculus

term has a beta-normal form. This means that we can alway find a beta

reduction sequence that halts at a normal form.

I was wondering how this result relates to the halting problem. Since Turing

provided one of the first proofs of the Weak Normalization Theorem, typable

terms cannot relate directly to halting computations. Does this mean that

the typable terms somehow miss the interesing part of the lambda calculus

where untypable terms may or may not have a normal form?

In particular, the fixed-point combinator Y is not typable, because it has

no normal form.

However, looking at Robin Milner's 1978 paper "A Theory of Type Polymorphism

in Programming", while he acknowledges that Y cannot be given a type, he is

able to introduce "fix" syntax which allows for recursive definitions and

assign types to such expressions. While maintaining the property that typed

programs cannot go wrong from a type point of view, presumably they can now

"go wrong" by not terminating.

It seems that typing of recursive programs using fix is possible because we

are always dealing with a particular instance, and not a general fixed-point

operator like Y. (In the same way as general self application, as in (lambda

x . x x) is not typable, but some particular cases, such as (I I) or (K K)

are?)

So, to finally get to my question -

Is it possible to define a set of pure combinators (e.g. SKIY and no

variables) and an abstraction process to remove variables from a language

such as the one Milner uses, in such a way that type checking can be

performed on the "compiled" combinator translation with the same result as

if it was performed on the original program? The problem being: how to

translate recursive definitions.