Skip to content

Only flatten up to type family arity in coreFlattenTyFamApp (#16995)

Ryan Scott requested to merge RyanGlScott/ghc:wip/T16995 into master

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).

Edited by Ryan Scott

Merge request reports