Abstract
Many type inference systems for Prolog programs are based on the tuple-distributive closure abstraction which ignores inter-argument dependencies. Thus, dependencies specified by head-only shared variables cannot be handled, and the inferred types are often very inaccurate. In this paper, we define an unfolding process which propagates such inter-argument dependencies: each call to a predicate that contains head-only shared variables is replaced by its definition. Hence, dependencies are actually propagated and the accuracy of the inferred types is improved. This unfolding process is repeated until a fix-point is reached in the computation of the type system. Termination is ensured by an abstraction function which limits the depth of recursive structures.