Only flatten up to type family arity in coreFlattenTyFamApp (#16995)
Among other uses, coreFlattenTyFamApp
is used by Core Lint as a
part of its check to ensure that each type family axiom reduces
according to the way it is defined in the source code. Unfortunately,
the logic that coreFlattenTyFamApp
uses to flatten type family
applications disagreed with the logic in TcFlatten
, which caused
it to spuriously complain this program:
type family Param :: Type -> Type
type family LookupParam (a :: Type) :: Type where
LookupParam (f Char) = Bool
LookupParam x = Int
foo :: LookupParam (Param ())
foo = 42
This is because coreFlattenTyFamApp
tries to flatten the Param ()
in LookupParam (Param ())
to alpha
(where alpha
is a flattening
skolem), and GHC is unable to conclude that alpha
is apart from
f Char
. This patch spruces up coreFlattenTyFamApp
so that it
instead flattens Param ()
to alpha ()
, which GHC can know for
sure is apart from f Char
. See
Note [Flattening]
, wrinkle 3 in FamInstEnv
.
Fixes #16995 (closed).