--- The 'btvs' are a subset of 'qtvs'. They are the ones we can
--- instantiate to a boxy type variable, because they'll definitely be
--- filled in later. This isn't always the case; sometimes we have type
--- variables mentioned in the context of the type, but not the body;
--- f :: forall a b. C a b => a -> a
--- Then we may land up with an unconstrained 'b', so we want to
--- instantiate it to a monotype (non-boxy) type variable
+-- Note [Pre-sub boxy]
+-- The 'btvs' are a subset of 'qtvs'. They are the ones we can
+-- instantiate to a boxy type variable, because they'll definitely be
+-- filled in later. This isn't always the case; sometimes we have type
+-- variables mentioned in the context of the type, but not the body;
+-- f :: forall a b. C a b => a -> a
+-- Then we may land up with an unconstrained 'b', so we want to
+-- instantiate it to a monotype (non-boxy) type variable
+--
+-- The 'qtvs' that are *neither* fixed by the pre-subsumption, *nor* are in 'btvs',
+-- are instantiated to TauTv meta variables.