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

Conversation

RyanGlScott
Copy link
Collaborator

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:

$(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:

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:

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

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.

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 RyanGlScott force-pushed the T601-helper-tyfam-precise-kinds branch from 320e2eb to 1668618 Compare June 30, 2024 21:29
@RyanGlScott RyanGlScott merged commit 48b419a into master Jul 1, 2024
24 checks passed
@RyanGlScott RyanGlScott deleted the T601-helper-tyfam-precise-kinds branch July 1, 2024 22:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant