GitLab

Note [Flattening] in GHC.Core.FamInstEnv describes an obscure "flattening" operation. (This is not the operation used during type-checking!) It comes from the closed type families paper. The core of the algorithm is to replace every type family application with a fresh variable.

However, it must be done in a pure context, so we have no source of Uniques nearby. Instead, we require an InScopeSet from the caller, and go through a fair amount of work making sure the fresh variables are fresh enough.

The result of flattening is then sent to unify with a potential type family equation. To be correct, the set of variables in the equation and the set of variables in the target must be distinct. This means that the flattening operation must have an InScopeSet that includes all variables used in the equation. In turn, this requirement means we must re-flatten a target for every equation. This seems shockingly inefficient.

Instead, I propose to take advantage of the fact that flattened types have a very short lifespan: they just get sent to the unifier, and then are never heard from again. With this in mind, we can use a UniqSupply specially built for flattening.

-- | This flattening operation must generate fresh Uniques for its type family
-- applications. Happily, the results of flattening are always short-lived: they
-- are sent to the unifier and then are never seen again. So, we create a
-- UniqSupply just to be used locally during the flatten operation. Each flatten
-- operation will produce the same sequence of Uniques, but that's fine.
--
-- The alternative is to use an InScopeSet. But these means re-flattening a
-- given type family application before comparing it against each type family
-- equation or class instance. That's inefficient; this is better, and simpler
-- than tracking an InScopeSet.
flatten_uniq_supply :: UniqSupply
{-# NOINLINE flatten_uniq_supply #-}
flatten_uniq_supply = unsafePerformIO (mkSplitUniqSupply 'f')

data FlattenEnv
  = FlattenEnv { fe_type_map :: TypeMap TyVar
                 -- domain: exactly-saturated type family applications
                 -- range: fresh variables
               , fe_in_scope :: InScopeSet
                 -- See Note [Flattening]
               , fe_uniq_supply :: UniqSupply }

As the Note explains, the fe_in_scope is still needed so that the two F b in Either (forall b. F b) (forall b. F b) don't get flattened to the same variable. But the UniqSupply should still simplify this algorithm, and avoid the need to pass in an InScopeSet to start it off.