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.