We present System F_RE — a novel extension of the polymorphic lambda-caluclus System F_ω extended with higher-order term rewriting and equational reasoning to model Haskell’s feature of rewrite rules. We develop a theoretical basis for automatic correctness checking of rules in this framework. We also provide a new tool, ReCheck, which implements advanced rewriting techniques to ensure the correctness of rewrite rules. Key to our method is ensuring local confluence and termination of rules. We demonstrate our method by checking various sample rewrite rules involving laws in the style of Algebra of Programming, higher-order functions, monads, and rules in existing programs in Hackage.