Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Give helper type families more precise kinds #612

Merged
merged 1 commit into from
Jul 1, 2024

Commits on Jun 30, 2024

  1. Give helper type families more precise kinds

    When promoting a class or instance method, we generate a "helper" type family
    definition that contains the actual implementation of the class or instance
    method. Prior to this patch, it was possible that the kind of the helper type
    family could be more polymorphic than desired. For instance, `singletons-th`
    would promote this:
    
    ```hs
    $(promote [d|
      type MyApplicative :: (Type -> Type) -> Constraint
      class Functor f => MyApplicative f where
        ap :: f (a -> b) -> f a -> f b
    
        rightSparrow :: f a -> f b -> f b
        rightSparrow x y = ap (id <$ x) y
      |])
    ```
    
    To this:
    
    ```hs
    type PMyApplicative :: (Type -> Type) -> Constraint
    class PMyApplicative f where
      type Ap (x :: f (a ~> b)) (y :: f a) :: f b
      type RightSparrow (x :: f a) (y :: f b) :: f b
      type RightSparrow x y = RightSparrowDefault x y
    
    -- The helper type family
    type RightSparrowDefault :: forall f a b. f a -> f b -> f b
    type family RightSparrowDefault x y where
      RightSparrowDefault x y = Ap (IdSym0 <$ x) y
    ```
    
    Note that GHC would generalize the standalone kind signature of
    `RightSparrowDefault` to:
    
    ```hs
    type RightSparrowDefault :: forall {k} (f :: k -> Type) (a :: k) (b :: k).
                                f a -> f b -> f b
    ```
    
    This is more general than intended, as we want `f` to be of kind `Type -> Type`
    instead. After all, we said as much in the standalone kind signature for
    `MyApplicative`! This excessive polymorphism doesn't actively cause problems in
    today's GHC, but they will cause problems in a future version of GHC that
    implements [GHC#23515](https://gitlab.haskell.org/ghc/ghc/-/issues/23515).
    (See #601.)
    
    This patch resolves the issue by propagating kind information from the class's
    standalone kind signature (or, in the case of instance declarations, the
    instance head) to the helper type family declarations. After this patch, we now
    generate the following kind for `RightSparrowDefault` (as verified by the new
    `T601a` test case):
    
    ```hs
    type RightSparrowDefault :: forall (f :: Type -> Type) a b.
                                f a -> f b -> f b
    ```
    
    This piggybacks on machinery that was added in #596 to do most of the heavy
    lifting.
    
    Resolves the "Overly polymorphic promoted class defaults" section of #601.
    RyanGlScott committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    1668618 View commit details
    Browse the repository at this point in the history