Skip to content
  • Ryan Scott's avatar
    Only flatten up to type family arity in coreFlattenTyFamApp (#16995) · 825c108b
    Ryan Scott authored and Marge Bot's avatar Marge Bot committed
    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:
    
    ```hs
    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 [Flatten], wrinkle 3` in `FamInstEnv`.
    825c108b