Skip to content

Commit

Permalink
Give helper type families more precise kinds
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
RyanGlScott committed Jun 30, 2024
1 parent b385b36 commit 320e2eb
Show file tree
Hide file tree
Showing 7 changed files with 229 additions and 83 deletions.
1 change: 1 addition & 0 deletions singletons-base/tests/SingletonsBaseTestSuite.hs
Original file line number Diff line number Diff line change
Expand Up @@ -166,6 +166,7 @@ tests =
, compileAndDumpStdTest "Prelude"
, compileAndDumpStdTest "T180"
, compileAndDumpStdTest "T361"
, compileAndDumpStdTest "T601a"
, compileAndDumpStdTest "T605"
],
testGroup "Database client"
Expand Down
73 changes: 73 additions & 0 deletions singletons-base/tests/compile-and-dump/Promote/T601a.golden
Original file line number Diff line number Diff line change
@@ -0,0 +1,73 @@
Promote/T601a.hs:(0,0)-(0,0): Splicing declarations
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 |]
======>
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
type ApSym0 :: forall (f :: Type -> Type)
a
b. (~>) (f ((~>) a b)) ((~>) (f a) (f b))
data ApSym0 :: (~>) (f ((~>) a b)) ((~>) (f a) (f b))
where
ApSym0KindInference :: SameKind (Apply ApSym0 arg) (ApSym1 arg) =>
ApSym0 a0123456789876543210
type instance Apply @(f ((~>) a b)) @((~>) (f a) (f b)) ApSym0 a0123456789876543210 = ApSym1 a0123456789876543210
instance SuppressUnusedWarnings ApSym0 where
suppressUnusedWarnings = snd ((,) ApSym0KindInference ())
type ApSym1 :: forall (f :: Type -> Type) a b. f ((~>) a b)
-> (~>) (f a) (f b)
data ApSym1 (a0123456789876543210 :: f ((~>) a b)) :: (~>) (f a) (f b)
where
ApSym1KindInference :: SameKind (Apply (ApSym1 a0123456789876543210) arg) (ApSym2 a0123456789876543210 arg) =>
ApSym1 a0123456789876543210 a0123456789876543210
type instance Apply @(f a) @(f b) (ApSym1 a0123456789876543210) a0123456789876543210 = Ap a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ApSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) ApSym1KindInference ())
type ApSym2 :: forall (f :: Type -> Type) a b. f ((~>) a b)
-> f a -> f b
type family ApSym2 @(f :: Type
-> Type) @a @b (a0123456789876543210 :: f ((~>) a b)) (a0123456789876543210 :: f a) :: f b where
ApSym2 a0123456789876543210 a0123456789876543210 = Ap a0123456789876543210 a0123456789876543210
type RightSparrowSym0 :: forall (f :: Type -> Type)
a
b. (~>) (f a) ((~>) (f b) (f b))
data RightSparrowSym0 :: (~>) (f a) ((~>) (f b) (f b))
where
RightSparrowSym0KindInference :: SameKind (Apply RightSparrowSym0 arg) (RightSparrowSym1 arg) =>
RightSparrowSym0 a0123456789876543210
type instance Apply @(f a) @((~>) (f b) (f b)) RightSparrowSym0 a0123456789876543210 = RightSparrowSym1 a0123456789876543210
instance SuppressUnusedWarnings RightSparrowSym0 where
suppressUnusedWarnings = snd ((,) RightSparrowSym0KindInference ())
type RightSparrowSym1 :: forall (f :: Type -> Type) a b. f a
-> (~>) (f b) (f b)
data RightSparrowSym1 (a0123456789876543210 :: f a) :: (~>) (f b) (f b)
where
RightSparrowSym1KindInference :: SameKind (Apply (RightSparrowSym1 a0123456789876543210) arg) (RightSparrowSym2 a0123456789876543210 arg) =>
RightSparrowSym1 a0123456789876543210 a0123456789876543210
type instance Apply @(f b) @(f b) (RightSparrowSym1 a0123456789876543210) a0123456789876543210 = RightSparrow a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (RightSparrowSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) RightSparrowSym1KindInference ())
type RightSparrowSym2 :: forall (f :: Type -> Type) a b. f a
-> f b -> f b
type family RightSparrowSym2 @(f :: Type
-> Type) @a @b (a0123456789876543210 :: f a) (a0123456789876543210 :: f b) :: f b where
RightSparrowSym2 a0123456789876543210 a0123456789876543210 = RightSparrow a0123456789876543210 a0123456789876543210
type RightSparrow_0123456789876543210 :: forall (f :: Type -> Type)
a
b. f a -> f b -> f b
type family RightSparrow_0123456789876543210 @(f :: Type
-> Type) @a @b (a :: f a) (a :: f b) :: f b where
RightSparrow_0123456789876543210 @f @a @b (x :: f a) (y :: f b) = Apply (Apply ApSym0 (Apply (Apply (<$@#@$) IdSym0) x)) y
type PMyApplicative :: (Type -> Type) -> Constraint
class PMyApplicative f where
type family Ap (arg :: f ((~>) a b)) (arg :: f a) :: f b
type family RightSparrow (arg :: f a) (arg :: f b) :: f b
type RightSparrow a a = RightSparrow_0123456789876543210 a a
14 changes: 14 additions & 0 deletions singletons-base/tests/compile-and-dump/Promote/T601a.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
module T601a where

import Data.Kind
import Data.Singletons.Base.TH
import Prelude.Singletons

$(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
|])
Loading

0 comments on commit 320e2eb

Please sign in to comment.