+Note [Typechecking rules]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+We *infer* the typ of the LHS, and use that type to *check* the type of
+the RHS. That means that higher-rank rules work reasonably well. Here's
+an example (test simplCore/should_compile/rule2.hs) produced by Roman:
+
+ foo :: (forall m. m a -> m b) -> m a -> m b
+ foo f = ...
+
+ bar :: (forall m. m a -> m a) -> m a -> m a
+ bar f = ...
+
+ {-# RULES "foo/bar" foo = bar #-}
+
+He wanted the rule to typecheck.
+