Fix M ->> M(Fix M) ->> M(M(Fix M)) ->> ...and therefore it cannot be strongly normalizing.
Assume by contradiction that such term M exists. Then M has the form \x1x2...xn. x N1N2...Nk. Le t us construct the principal type of M by building a proof for |- M:T, where T is a variable representing a type expression. Since M is typable, x cannot be a free variable, hence we must have n>=1. Hence the first rule applied in the proof must be the abstraction rule, with a condition of the form T = T1 -> T2 and a premise of the form
\x1:T1 |- \x2...xn. x N1N2...Nk : T2Now, if n=1, then x1 = x, the next rule is the application, and one of the premises would be
\x1:T1|- x1 : T3 -> T2The unification T1 = T3 -> T2 however would imply that the type of M is not of the form A -> A -> A (because A would have to be instantiated to a type of the form T3 -> T4). Hence the above hypothesis is wrong, i.e. n must be at least 2. As a consequence, the next rule must be the abstraction rule again, with a condition of the form T2 = T3 -> T4 and a premise of the form
\x1:T1, x2:T3 |- \x3...xn. x N1N2...Nk : T4At this point we see that we cannot use neither the abstraction nor the application rule, for the same reason as above (we would instantiate the type too much). Hence we must apply necessarily the var rule, which means that k = 0, n = 2, and x must either be x1 or x2. In the first case, the type of M will be T = T1 -> T3 -> T1, in the second case it will be T = T1 -> T3 -> T3. In both cases, T is more general than A -> A -> A.
Note: even though A -> A -> A is not the principal type of any term in normal form, there are terms (not in normal form, of course) that have A -> A -> A as principal type. We leave for exercise to find such a term.