In this paper, a new comprehensive framework for higher-order
rewriting is introduced, which combines aspects of earlier defined
frameworks with novel ones: function symbols and free variables have
both a type and an arity; rewrite rules operate on terms in
beta-eta-normal form and use higher-order pattern matching to
search for a redex; rules of functional type are admitted without
compromising the relationship between equational reasoning and
confluence thanks to the assumption that their lefthand side is a
pattern in the sense of Miller; the polymorphic type system is
powerfull enough so as to encode the simply typed
lambda-calculus. The study of this rewrite relation is carried out
first at an abstract level of its own interest called \emph{normal
rewriting}. It is shown that the Church-Rosser properties of normal
rewriting follow from a termination assumption, the joinability of
irreducible critical pairs, and the presence of appropriate extended
rules. These abstract results allow to capture and generalize
Nipkow's approach to higher-order rewriting as well as our approach
with types and arities.