The process of type inference is the fact of guessing, given an user-written program, what the type of this program is. In general, there may be several correct types for a given program. For example, the program fun x -> x can be given the types int -> int and bool -> bool.
Given a program, a type for this program is principal if it is the most general type that can be given to this program, in the sense that all other psosible types are specialization (instances) of this type. With my fun x -> x example, the polymorphic 'a -> 'a is a principal type.
A type system has the property of principal typing if for every term in the system, there's a principal type that subsumes (is a more general version, or a "supertype") all the other possible typings of the term.
Type systems with principal typing: ML, System F Type systems without principal typing: ML + overloaded operators, ML + polymorphic recursion (it can make the inference of the principal type undecidable) , Haskell's typesystem