We define two type assignment systems for first-order rewriting extended with application, -abstraction,
and -reduction, using a combination of intersection types and second-order polymorphic types. The first system
is the general one, for which we prove subject reduction, and strong normalisation of typeable terms. The second
is a decidable subsystem of the first, by restricting to rank 2 (intersection and quantified) types. For this system
we define, using an extended notion of unification, a notion of principal typing which is more general than ML’s
principal type property, since also the types for the free variables of terms are inferred