+-- | When we are comparing (or matching) types or terms, we are faced with
+-- \"going under\" corresponding binders. E.g. when comparing:
+--
+-- > \x. e1 ~ \y. e2
+--
+-- Basically we want to rename [@x@ -> @y@] or [@y@ -> @x@], but there are lots of
+-- things we must be careful of. In particular, @x@ might be free in @e2@, or
+-- y in @e1@. So the idea is that we come up with a fresh binder that is free
+-- in neither, and rename @x@ and @y@ respectively. That means we must maintain:
+--
+-- 1. A renaming for the left-hand expression
+--
+-- 2. A renaming for the right-hand expressions
+--
+-- 3. An in-scope set
+--
+-- Furthermore, when matching, we want to be able to have an 'occurs check',
+-- to prevent:
+--
+-- > \x. f ~ \y. y
+--
+-- matching with [@f@ -> @y@]. So for each expression we want to know that set of
+-- locally-bound variables. That is precisely the domain of the mappings 1.
+-- and 2., but we must ensure that we always extend the mappings as we go in.
+--
+-- All of this information is bundled up in the 'RnEnv2'
+data RnEnv2