Skip to content

Make singletons buildable after GHC#23515 #601

Open
Open
Make singletons buildable after GHC#23515#601
Labels
bug

Description

@RyanGlScott
RyanGlScott
opened on Jun 1, 2024

GHC#23515 tracks implementing this portion of GHC proposal #425 (Invisible binders in type declarations):

In type family and data family instances, the instantiation is fully determined by the left hand side, without looking at the right hand side.

A reasonable change, but one that will nevertheless cause several parts of singletons and singletons-base to fail to compile. This issue aims to identify all of these sources of breakage and how to fix them.

(There is a prototype implementation of this GHC proposal in GHC!12776, which is what I used to discover these breakages.)

Table of Contents

  1. Sing instances without explicit left-hand sides (EDIT: solved)
  2. Overly polymorphic lambda-lifting, part 1 (EDIT: solved)
  3. Overly polymorphic promoted class defaults (EDIT: mostly solved)
  4. Overly polymorphic instance methods (EDIT: mostly solved)
  5. Defunctionalizing declarations using visible dependent quantification (EDIT: solved)
  6. Overly polymorphic lambda-lifting, part 2 (EDIT: solved)
  7. Overly polymorphic local bindings

Sing instances without explicit left-hand sides

EDIT: This was fixed by #602.

There are places in singletons and singletons-base that declare Sing instances without specifying what type the Sing instance is for on the left-hand side, e.g.,

type instance Sing = SNat

This will no longer work after GHC#23515 is implemented. Instead, we must write:

type instance Sing @Nat = SNat

The following places in the code will need to be updated:

Overly polymorphic lambda-lifting, part 1

EDIT: This should be fixed as of #593.

This code will fail to compile after GHC#23515 is implemented:

singletons/singletons-base/src/Data/Singletons/Base/Instances.hs

Lines 34 to 41 in 7e5c92d

$(singletonsOnly [d|
foldl :: forall a b. (b -> a -> b) -> b -> [a] -> b
foldl f z0 xs0 = lgo z0 xs0
where
lgo :: b -> [a] -> b
lgo z [] = z
lgo z (x:xs) = lgo (f z x) xs
|])

This is because we will promote foldl to code that looks something like this:

{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Data.Kind

type TyFun :: Type -> Type -> Type
data TyFun a b

type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>

type Apply :: (a ~> b) -> a -> b
type family Apply f x

type SameKind :: k -> k -> Constraint
type SameKind a b = (() :: Constraint)

type family Lgo a b f z0 xs0 (z :: b) (ls :: [a]) :: b where
  Lgo a b f z0 xs0 z '[] = z
  Lgo a b f z0 xs0 z (x:xs) = Lgo a b f z0 xs0 (f `Apply` z `Apply` x) xs

data LgoSym0 tf where
  LgoSym0KindInference :: SameKind (Apply LgoSym0 arg) (LgoSym1 arg) =>
                          LgoSym0 a
type instance Apply LgoSym0 a = LgoSym1 a

data LgoSym1 a tf where
  LgoSym1KindInference :: SameKind (Apply (LgoSym1 a) arg) (LgoSym2 a arg) =>
                          LgoSym1 a b
type instance Apply (LgoSym1 a) b = LgoSym2 a b

data LgoSym2 a b tf where
  LgoSym2KindInference :: SameKind (Apply (LgoSym2 a b) arg) (LgoSym3 a b arg) =>
                          LgoSym2 a b f
type instance Apply (LgoSym2 a b) f = LgoSym3 a b f

data LgoSym3 a b f tf where
  LgoSym3KindInference :: SameKind (Apply (LgoSym3 a b f) arg) (LgoSym4 a b f arg) =>
                          LgoSym3 a b f z0
type instance Apply (LgoSym3 a b f) z0 = LgoSym4 a b f z0

data LgoSym4 a b f z0 tf where
  LgoSym4KindInference :: SameKind (Apply (LgoSym4 a b f z0) arg) (LgoSym5 a b f z0 arg) =>
                          LgoSym4 a b f z0 xs0
type instance Apply (LgoSym4 a b f z0) xs0 = LgoSym5 a b f z0 xs0

data LgoSym5 a b f z0 xs0 :: b ~> [a] ~> b where
  LgoSym5KindInference :: SameKind (Apply (LgoSym5 a b f z0 xs0) arg) (LgoSym6 a b f z0 xs0 arg) =>
                          LgoSym5 a b f z0 xs0 z
type instance Apply (LgoSym5 a b f z0 xs0) z = LgoSym6 a b f z0 xs0 z

data LgoSym6 a b f z0 xs0 (z :: b) :: [a] ~> b where
  LgoSym6KindInference :: SameKind (Apply (LgoSym6 a b f z0 xs0 z) arg) (LgoSym7 a b f z0 xs0 z arg) =>
                          LgoSym6 a b f z0 xs0 z ls
type instance Apply (LgoSym6 a b f z0 xs0 z) ls  = LgoSym7 a b f z0 xs0 z ls

type family LgoSym7 a b f z0 xs0 (z :: b) (ls :: [a]) :: b where
  LgoSym7 a b f z0 xs0 z ls = Lgo a b f z0 xs0 z ls

And this will fail with:

$ ~/Software/ghc3/_build/stage1/bin/ghc Foo.hs
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )
Foo.hs:50:58: error: [GHC-25897]
    • Couldn't match kind ‘b1’ with ‘b2’
      Expected kind ‘b2 ~> (a3 ~> b2)’,
        but ‘f’ has kind ‘b1 ~> (a1 ~> b1)’
      ‘b1’ is a rigid type variable bound by
        a family instance declaration
        at Foo.hs:50:15-19
      ‘b2’ is a rigid type variable bound by
        a family instance declaration
        at Foo.hs:50:21-42
    • In the third argument of ‘LgoSym5’, namely ‘f’
      In the type instance declaration for ‘Apply’
   |
50 | type instance Apply (LgoSym4 a b f z0) xs0 = LgoSym5 a b f z0 xs0
   |                                                          ^

The reason this happens is because the kinds of some of these defunctionalization symbols are more polymorphic than we want. For instance, compare the kinds of LgoSym4 and LgoSym5:

LgoSym4 :: Type -> Type -> (b ~> a ~> b) -> k1 -> k2 ~> b ~> [a] ~> b
LgoSym5 :: forall a b   -> (b ~> a ~> b) -> k1 -> k2 -> b ~> [a] ~> b

Note that the kind of LgoSym5 uses visible foralls, whereas the kind of LgoSym4 does not. This actually matters in practice, because when you write this:

type instance Apply (LgoSym4 a b f z0) xs0 = ...

If we do nothing but look at the left-hand side of the type family instance, we conclude that:

type instance Apply @k2 @(b1 ~> [a1] ~> b1) (LgoSym4 a b f z0) (xs0 :: k2) = ... :: b1 ~> [a1] ~> b1

Note that the type variables in @(b1 ~> [a1] ~> b1) are not the same as in (LgoSym4 a b ...), because nothing in the kind of LgoSym4 relates the two.

Now GHC proceeds to kind-check the right-hand-side against kind b1 ~> [a1] ~> b1:

LgoSym5 a b f z0 xs0 :: b1 ~> [a1] ~> b1

But this doesn't work, because LgoSym5 a b f z0 xs0 has kind b ~> [a] ~> b, not b1 ~> [a1] ~> b1! If we were allowed to unify a/a1 and b/b1, then this would kind-check, but this is not possible due to the changes brought on by GHC#23515.

I can see two possible ways to fix this:

  1. If we wrote the defunctionalization symbols like this instead:

    {-# LANGUAGE GHC2024 #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Data.Kind

type TyFun :: Type -> Type -> Type
data TyFun a b

type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>

type Apply :: (a ~> b) -> a -> b
type family Apply f x

type SameKind :: k -> k -> Constraint
type SameKind a b = (() :: Constraint)

type family Lgo a b f z0 xs0 (z :: b) (ls :: [a]) :: b where
  Lgo a b f z0 xs0 z '[] = z
  Lgo a b f z0 xs0 z (x:xs) = Lgo a b f z0 xs0 (f `Apply` z `Apply` x) xs

data LgoSym0 a b f z0 xs0 :: b ~> [a] ~> b where
  LgoSym0KindInference :: SameKind (Apply (LgoSym0 a b f z0 xs0) arg) (LgoSym1 a b f z0 xs0 arg) =>
                          LgoSym0 a b f z0 xs0 z
type instance Apply (LgoSym0 a b f z0 xs0) z = LgoSym1 a b f z0 xs0 z

data LgoSym1 a b f z0 xs0 (z :: b) :: [a] ~> b where
  LgoSym1KindInference :: SameKind (Apply (LgoSym1 a b f z0 xs0 z) arg) (LgoSym2 a b f z0 xs0 z arg) =>
                          LgoSym1 a b f z0 xs0 z ls
type instance Apply (LgoSym1 a b f z0 xs0 z) ls = LgoSym2 a b f z0 xs0 z ls

type family LgoSym2 a b f z0 xs0 (z :: b) (ls :: [a]) :: b where
  LgoSym2 a b f z0 xs0 z ls = Lgo a b f z0 xs0 z ls

    Then the kinds of all defunctionalization symbols use visible foralls, thereby giving GHC enough information to kind-check this program even with the changes brought on by GHC#23515:

    LgoSym0 :: forall a b -> (b ~> a ~> b) -> k1 -> k2 -> b ~> [a] ~> b
LgoSym1 :: forall a b -> (b ~> a ~> b) -> k1 -> k2 -> b -> [a] ~> b
LgoSym2 :: forall a b -> (b ~> a ~> b) -> k1 -> k2 -> b -> [a] -> b

    This is exactly the change proposed in Reduce defunctionalization symbol bloat related to local variables #592. (I think fixing Reduce defunctionalization symbol bloat related to local variables #592 is worth doing independently of this issue, but it's nice to know that it helps here as well).

  2. Generate this code instead:

    type instance Apply @_ @(b ~> [a] ~> b) (LgoSym4 a b f z0) xs0 = LgoSym5 a b f z0 xs0

    It should be possible to generate this code without requiring too much cleverness on singletons-th's end.

Later in the Defunctionalizing declarations using visible dependent quantification section, we will see an example where option (1) won't suffice and where option (2) is required. And later in the Overly polymorphic lambda-lifting, part 2 section, we will see an example where neither option (1) nor option (2) are sufficient.

Overly polymorphic promoted class defaults

EDIT: This issue no longer occurs within singletons-base:

Note that the underlying issue still applies regardless of the changes above, however—you'll still need to provide standalone kind signatures in places that didn't require them before.

Consider this program:

$(promote [d|
  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
  |])

We have not given MyApplicative a standalone kind signature, but the intent is that f is inferred to be of kind Type -> Type. However, consider what happens when MyApplicative is promoted:

{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Data.Kind

type TyFun :: Type -> Type -> Type
data TyFun a b

type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>

type Apply :: (a ~> b) -> a -> b
type family Apply f x

type Id :: a -> a
type family Id x where
  Id x = x

type IdSym0 :: a ~> a
data IdSym0 z
type instance Apply IdSym0 x = Id x

class PFunctor f where
  type (x :: a) <$ (y :: f b) :: f a

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

type RightSparrowDefault :: f a -> f b -> f b
type family RightSparrowDefault x y where
  RightSparrowDefault x y = Ap (IdSym0 <$ x) y

There's something suspicious about RightSparrowDefault. It has the standalone kind signature f a -> f b -> f b, and GHC will kind-generalize this to forall {k} (f :: k -> Type) (a :: k) (b :: k). f a -> f b -> f b. The actual body of RightSparrowDefault, however, requires k to be Type. GHC does not like this after the changes brought on by GHC#23515, and it will reject it:

$ ~/Software/ghc3/_build/stage1/bin/ghc Foo.hs
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )
Foo.hs:38:43: error: [GHC-25897]
    • Couldn't match kind ‘k’ with ‘*’
      When matching kinds
        a :: k
        b0 :: *
      Expected kind ‘f0 b0’, but ‘x’ has kind ‘f a’
      ‘k’ is a rigid type variable bound by
        a family instance declaration
        at Foo.hs:38:3-46
    • In the second argument of ‘(<$)’, namely ‘x’
      In the first argument of ‘Ap’, namely ‘(IdSym0 <$ x)’
      In the type family declaration for ‘RightSparrowDefault’
   |
38 |   RightSparrowDefault x y = Ap (IdSym0 <$ x) y
   |                                           ^

(This is the same issue described in Note [Fully saturated defunctionalization symbols]).

It's tempting to try to repair the issue by removing the standalone kind signature:

type family RightSparrowDefault (x :: f a) (y :: f b) :: f b where
  RightSparrowDefault x y = Ap (IdSym0 <$ x) y

But GHC won't accept that, regardless of whether you have the changes from GHC#23515 or not:

$ ~/Software/ghc3/_build/stage1/bin/ghc Foo.hs
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )
Foo.hs:32:12: error: [GHC-17370]
    • Different names for the same type variable: ‘a’ and ‘b’
    • In the class declaration for ‘PMyApplicative’
   |
32 |   type Ap (x :: f (a ~> b)) (y :: f a) :: f b
   |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

As such, we're stuck between a rock and a hard place.

Unfortunately, I don't know if singletons-th will be able to promote classes like MyApplicative anymore—at least, not without making some minor edits to clarify what the kind of f is. My vision is being able to write this instead:

$(promote [d|
  type MyApplicative :: (Type -> Type) -> Constraint
  class Functor f => MyApplicative f where
  -- Or, alternatively,
  -- class Functor f => MyApplicative (f :: Type) where
    ...
  |])

And then singletons-th would generate this default instead:

type RightSparrowDefault :: forall (f :: Type -> Type) a b. f a -> f b -> f b
type family RightSparrowDefault x y where
  RightSparrowDefault x y = Ap (IdSym0 <$ x) y

And then everything would be fine and dandy. Currently, singletons-th does not do this, but it could with a bit of additional work to make the (Type -> Type) kind from the class flow down through to the promoted class method default.

Overly polymorphic instance methods

EDIT: I believe all known examples of this issue in singletons-base have been worked around in #607 and #611. The underlying issue still applies, however.

Just as class defaults can be overly polymorphic, so too can instance methods. Consider this example:

-- NB: Compose :: (k -> Type) -> (j -> k) -> j -> Type

$(promote [d|
  instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap h (Compose x) = Compose (fmap (fmap h) x)
  |])

Currently, this instance will be promoted to:

{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Data.Functor.Compose
import Data.Kind

type TyFun :: Type -> Type -> Type
data TyFun a b

type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>

type Apply :: (a ~> b) -> a -> b
type family Apply f x

class PFunctor f where
  type Fmap (h :: a ~> b) (x :: f a) :: f b

type FmapSym0 :: (a ~> b) ~> f a ~> f b
data FmapSym0 z
type instance Apply FmapSym0 h = FmapSym1 h

type FmapSym1 :: (a ~> b) -> f a ~> f b
data FmapSym1 g z
type instance Apply (FmapSym1 h) x = Fmap h x

instance PFunctor (Compose f g) where
  type Fmap h x = FmapCompose h x

type FmapCompose :: (a ~> b) -> Compose f g a -> Compose f g b
type family FmapCompose g c where
  FmapCompose h ('Compose x) = 'Compose (Fmap (FmapSym1 h) x)

There are two problems with this code:

  1. When GHC kind-checks FmapCompose's standalone kind signature, it will kind-generalize it to:

    type FmapCompose :: forall {k} (f :: k -> Type) (g :: Type -> k) (a :: Type) (b :: Type).
                    (a ~> b) -> Compose f g a -> Compose f g b

    This is too general for our needs, as calling Fmap requires that both f and g be of kind Type -> Type:

    $ ~/Software/ghc3/_build/stage1/bin/ghc Foo.hs
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )
Foo.hs:37:60: error: [GHC-25897]
    • Couldn't match kind ‘k’ with ‘*’
      When matching kinds
        g :: * -> k
        g0 :: * -> *
      Expected kind ‘f0 (g0 a)’, but ‘x’ has kind ‘f (g a)’
      ‘k’ is a rigid type variable bound by
        a family instance declaration
        at Foo.hs:37:3-61
    • In the second argument of ‘Fmap’, namely ‘x’
      In the first argument of ‘'Compose’, namely ‘(Fmap (FmapSym1 h) x)’
      In the type family declaration for ‘FmapCompose’
   |
37 |   FmapCompose h ('Compose x) = 'Compose (Fmap (FmapSym1 h) x)
   |                                                            ^

  2. GHC will kind-generalize the instance PFunctor (Compose f g) declaration to:

    instance forall {k} (f :: k -> Type) (g :: Type -> k) (a :: Type) (b :: Type).
         PFunctor (Compose f g) where ...

    Which is also too polymorphic:

    $ ~/Software/ghc3/_build/stage1/bin/ghc Foo.hs
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )
Foo.hs:33:33: error: [GHC-25897]
    • Couldn't match kind ‘k’ with ‘*’
      Expected kind ‘Compose @{*} @{*} f g a’,
        but ‘x’ has kind ‘Compose @{k} @{*} f g a’
      ‘k’ is a rigid type variable bound by
        a family instance declaration
        at Foo.hs:(32,1)-(33,33)
    • In the second argument of ‘FmapCompose’, namely ‘x’
      In the type instance declaration for ‘Fmap’
      In the instance declaration for ‘PFunctor (Compose f g)’
   |
33 |   type Fmap h x = FmapCompose h x
   |                                 ^

Again, I think users will need some kind of manual edits in order to make this sort of code work. A workaround exists in today's singletons-th which works well enough:

$(promote [d|
  -- NB: Note the explicit `f :: Type -> Type` kind signature
  instance (Functor f, Functor g) => Functor (Compose (f :: Type -> Type) g) where
    fmap h (Compose x) = Compose (fmap (fmap h) x)
  |])

This will make singletons-th generate code that looks like this:

{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Data.Functor.Compose
import Data.Kind

type TyFun :: Type -> Type -> Type
data TyFun a b

type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>

type Apply :: (a ~> b) -> a -> b
type family Apply f x

class PFunctor f where
  type Fmap (h :: a ~> b) (x :: f a) :: f b

type FmapSym0 :: (a ~> b) ~> f a ~> f b
data FmapSym0 z
type instance Apply FmapSym0 h = FmapSym1 h

type FmapSym1 :: (a ~> b) -> f a ~> f b
data FmapSym1 g z
type instance Apply (FmapSym1 h) x = Fmap h x

instance PFunctor (Compose (f :: Type -> Type) g) where
  type Fmap h x = FmapCompose h x

type FmapCompose :: forall (f :: Type -> Type) g a b.
                    (a ~> b) -> Compose f g a -> Compose f g b
type family FmapCompose g c where
  FmapCompose h ('Compose x) = 'Compose (Fmap (FmapSym1 h) x)

Defunctionalizing declarations using visible dependent quantification

EDIT: This was fixed by #603.

When you promote this type-level declaration:

$(promote [d|
  type P :: forall k -> k -> Type
  type P k (a :: k) = Proxy a
  |])

singletons-th will generate this code:

{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Data.Kind
import Data.Proxy

type TyFun :: Type -> Type -> Type
data TyFun a b

type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>

type Apply :: (a ~> b) -> a -> b
type family Apply f x

type SameKind :: k -> k -> Constraint
type SameKind a b = (() :: Constraint)

type P :: forall k -> k -> Type
type P k (a :: k) = Proxy a

data PSym0 z where
  PSym0KindInference :: SameKind (Apply PSym0 arg) (PSym1 arg) =>
                        PSym0 k
type instance Apply PSym0 k = PSym1 k

data PSym1 k :: k ~> Type where
  PSym1KindInference :: SameKind (Apply (PSym1 k) arg) (PSym2 k arg) =>
                        PSym1 k a
type instance Apply (PSym1 k) a = PSym2 k a

type family PSym2 k (a :: k) :: Type where
  PSym2 k a = P k a(#overly-polymorphic-lambda-lifting-part-1)

GHC will now reject this with:

$ ~/Software/ghc3/_build/stage1/bin/ghc Foo.hs
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )
Foo.hs:31:31: error: [GHC-25897]
    • Couldn't match kind ‘k’ with ‘arg’
      Expected kind ‘TyFun arg Type -> Type’,
        but ‘PSym1 k’ has kind ‘TyFun k Type -> Type’
      ‘k’ is a rigid type variable bound by
        a family instance declaration
        at Foo.hs:31:21-27
      ‘arg’ is a rigid type variable bound by
        a family instance declaration
        at Foo.hs:31:15-19
    • In the type instance declaration for ‘Apply’
   |
31 | type instance Apply PSym0 k = PSym1 k
   |                               ^^^^^^^

If this feels familiar, it's because we've already seen this exact same scenario play out before in the Overly polymorphic lambda-lifting, part 1 section. In particular, we have defunctionalization symbols with the following kinds:

PSym0 :: Type     ~> k ~> Type
PSym1 :: forall k -> k ~> Type

Note that the kind of PSym1 uses a visible forall, whereas the kind of PSym0 does not. Therefore, when GHC kind-checks the left-hand side of this type family instance:

type instance Apply PSym0 k = ...

GHC concludes that:

type instance Apply @Type @(k1 ~> Type) PSym0 k = ... :: k1 ~> Type

Where k1 is distinct from k. Therefore, when we kind-check the right-hand side:

... = PSym1 k :: k1 ~> Type

We have a kind error, as PSym1 k has kind k ~> Type, not k1 ~> Type. (Note that k1 happens to be called "arg" in the error message above.)

This time, the trick from #592 (i.e., option (1) in the Overly polymorphic lambda-lifting, part 1 section) won't work, as there is no lambda-lifting happening here. The most viable solution is to implement option (2) in the Overly polymorphic lambda-lifting, part 1 section by generating this code:

type instance Apply @_ @(k ~> Type) PSym0 k = PSym1 k

Overly polymorphic lambda-lifting, part 2

EDIT: This was fixed by #610.

Neither option (1) nor option (2) from the Overly polymorphic lambda-lifting, part 1 section above are enough to make this example work:

$(promote [d|
  nub                     :: forall a. (Eq a) => [a] -> [a]
  nub l                   = nub' l []
    where
      nub' :: [a] -> [a] -> [a]
      nub' [] _           = []
      nub' (x:xs) ls      = if x `elem` ls then nub' xs ls else x : nub' xs (x:ls)
  |])

singletons-th will generate (roughly) the following code when promoting nub:

{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Data.Type.Bool

class PEq a where
  type (x :: a) == (y :: a) :: Bool

type Elem :: a -> [a] -> Bool
type family Elem x ls where
  Elem _ '[] = False
  Elem x (y:ys) = x == y || Elem x ys

type family LetScrutinee a x xs ls l where
  LetScrutinee a x xs ls l = Elem x ls

type family Case a x xs ls l t where
  Case a x xs ls l True  = Nub' a l xs ls
  Case a x xs ls l False = x : Nub' a l xs (x:ls)

type family Nub' a l (x :: [a]) (ls :: [a]) :: [a] where
  Nub' a l '[]    _  = '[]
  Nub' a l (x:xs) ls = Case a x xs ls l (LetScrutinee a x xs ls l)

type Nub :: forall a. [a] -> [a]
type family Nub l where
  Nub @a l = Nub' a l l '[]

GHC will now reject this:

$ ~/Software/ghc3/_build/stage1/bin/ghc Foo.hs
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )
Foo.hs:20:37: error: [GHC-25897]
    • Couldn't match kind ‘a1’ with ‘a2’
      Expected kind ‘[a2]’, but ‘xs’ has kind ‘[a1]’
      ‘a1’ is a rigid type variable bound by
        a family instance declaration
        at Foo.hs:20:3-41
      ‘a2’ is a rigid type variable bound by
        a family instance declaration
        at Foo.hs:20:8-23
    • In the third argument of ‘Nub'’, namely ‘xs’
      In the type family declaration for ‘Case’
   |
20 |   Case a x xs ls l True  = Nub' a l xs ls
   |                                     ^^

Foo.hs:21:41: error: [GHC-25897]
    • Couldn't match kind ‘a1’ with ‘a2’
      Expected kind ‘[a2]’, but ‘xs’ has kind ‘[a1]’
      ‘a1’ is a rigid type variable bound by
        a family instance declaration
        at Foo.hs:21:3-49
      ‘a2’ is a rigid type variable bound by
        a family instance declaration
        at Foo.hs:21:8-24
    • In the third argument of ‘Nub'’, namely ‘xs’
      In the second argument of ‘(:)’, namely ‘Nub' a l xs (x : ls)’
      In the type family declaration for ‘Case’
   |
21 |   Case a x xs ls l False = x : Nub' a l xs (x:ls)
   |                                         ^^

The problem is that Case's kind is too polymorphic:

Case :: Type -> a -> [a] -> [a] -> k -> Bool -> [a]

Rather than something like:

Case :: forall a -> a -> [a] -> [a] -> [a] -> Bool -> [a]

However, we can do better here. Note that none of the arguments to Case have any kind signatures whatsoever:

type family Case a x xs ls l t where ...

This is silly, because we can determine the kinds of several of these arguments (e.g., ls and l) by looking at the syntax of nub. And indeed, if we sprinkle even a couple of these kind signatures into the definition of Case:

type family Case a x xs (ls :: [a]) (l :: [a]) t where ...

Then GHC accepts the program once more. It should be possible to generate these kind signatures during lambda lifting.

Parts of singletons-base which are affected by this issue are:

Overly polymorphic local bindings

Here is a problematic example, boiled down from the Singletons/T296.hs test case:

$(promote [d|
  n :: forall a. Maybe a
  n = let z = let x :: Maybe a
                  x = Nothing in x
      in z
  |])

This translates to the following code:

{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind

type family LetX a :: Maybe a where
  LetX a = 'Nothing

type family LetZ a where
  LetZ a = LetX a

type N :: forall a. Maybe a
type family N @a :: Maybe a where
  N @a = LetZ a

LetZ is problematic. GHC 9.10.1 accepts it, but gives it a counterintuitive kind:

λ> :info LetZ
type LetZ :: forall {a}. Type -> Maybe a
type family LetZ @{a} a1 where
  forall a. LetZ @{a} a = LetX a

Rather than giving it the kind forall a -> Maybe a, it's given the kind Type -> Maybe a, and the type family equation for LetZ matches on the invisible kind argument (LetZ @{a} a = ...). A more recent GHC will reject this with:

$ ~/Software/ghc3/_build/stage1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
Bug.hs:14:12: error: [GHC-25897]
    • Couldn't match kind ‘a2’ with ‘a1’
      Expected kind ‘Maybe a1’, but ‘LetX a’ has kind ‘Maybe a2’
      ‘a2’ is a rigid type variable bound by
        a family instance declaration
        at Bug.hs:14:8
      ‘a1’ is a rigid type variable bound by
        a family instance declaration
        at Bug.hs:14:3-17
    • In the type family declaration for ‘LetZ’
   |
14 |   LetZ a = LetX a
   |            ^^^^^^

Some singletons-base test suite failures that have similar root causes:

  • Singletons/CaseExpressions.hs:

    singletons/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.hs

    Lines 25 to 29 in 037fc0e

    foo4 :: forall a. a -> a
    foo4 x = case x of
    y -> let z :: a
    z = y
    in z 

    Singletons/CaseExpressions.hs:0:0: error: [GHC-25897]
    • Expected kind ‘a0’, but ‘y’ has kind ‘a’
      ‘a0’ is a rigid type variable bound by
        a family instance declaration
        at Singletons/CaseExpressions.hs:(0,0)-(0,0)
      ‘a’ is a rigid type variable bound by
        a family instance declaration
        at Singletons/CaseExpressions.hs:(0,0)-(0,0)
    • In the second argument of ‘Let0123456789876543210ZSym0’, namely
        ‘y’
      In the type family declaration for ‘Case_0123456789876543210’
  |
8 | $(singletons [d|
  |  ^^^^^^^^^^^^^^^...

  • Singletons/T183.hs:

    singletons/singletons-base/tests/compile-and-dump/Singletons/T183.hs

    Line 53 in 037fc0e

    foo8 x@(Just (_ :: a) :: Maybe a) = x 

    Singletons/T183.hs:0:0: error: [GHC-25897]
    • Expected kind ‘a0’, but ‘wild_0123456789876543210’ has kind ‘a’
      ‘a0’ is a rigid type variable bound by
        a family instance declaration
        at Singletons/T183.hs:(0,0)-(0,0)
      ‘a’ is a rigid type variable bound by
        a family instance declaration
        at Singletons/T183.hs:(0,0)-(0,0)
    • In the second argument of ‘Apply’, namely
        ‘(wild_0123456789876543210 :: a)’
      In the type family declaration for ‘Let0123456789876543210X’
  |
6 | $(singletons [d|
  |  ^^^^^^^^^^^^^^^...

  • Singletons/T296.hs:

    singletons/singletons-base/tests/compile-and-dump/Singletons/T296.hs

    Lines 9 to 13 in 037fc0e

    f :: forall a. MyProxy a -> MyProxy a
    f MyProxy =
    let x = let z :: MyProxy a
    z = MyProxy in z
    in x 

    Singletons/T296.hs:0:0: error: [GHC-25897]
    • Couldn't match kind ‘a0’ with ‘a’
      Expected kind ‘MyProxy a’,
        but ‘Let0123456789876543210ZSym0 a’ has kind ‘MyProxy a0’
      ‘a0’ is a rigid type variable bound by
        a family instance declaration
        at Singletons/T296.hs:(0,0)-(0,0)
      ‘a’ is a rigid type variable bound by
        a family instance declaration
        at Singletons/T296.hs:(0,0)-(0,0)
    • In the type family declaration for ‘Let0123456789876543210X’
  |
6 | $(singletons [d|
  |  ^^^^^^^^^^^^^^^...

  • Singletons/T433.hs:

    singletons/singletons-base/tests/compile-and-dump/Singletons/T433.hs

    Lines 41 to 43 in 037fc0e

    id7 (x :: b) = g
    where
    g = (x :: b) 

    Singletons/T433.hs:0:0: error: [GHC-25897]
    • Expected kind ‘b2’, but ‘x’ has kind ‘b1’
      ‘b1’ is a rigid type variable bound by
        a family instance declaration
        at Singletons/T433.hs:(0,0)-(0,0)
      ‘b2’ is a rigid type variable bound by
        a family instance declaration
        at Singletons/T433.hs:(0,0)-(0,0)
    • In the type family declaration for ‘Let0123456789876543210G’
  |
7 | $(promote [d|
  |  ^^^^^^^^^^^^...

  • Singletons/T581.hs:

    singletons/singletons-base/tests/compile-and-dump/Singletons/T581.hs

    Lines 30 to 32 in 5f0d420

    instance C3 (Maybe a) where
    m3 :: Maybe a -> b -> (Maybe a, b)
    m3 x y = (fmap (\xx -> (xx :: a)) x, y) 

    Singletons/T581.hs:0:0: error: [GHC-25897]
    • Expected kind ‘a0’, but ‘xx’ has kind ‘a’
      ‘a0’ is a rigid type variable bound by
        a family instance declaration
        at Singletons/T581.hs:(0,0)-(0,0)
      ‘a’ is a rigid type variable bound by
        a family instance declaration
        at Singletons/T581.hs:(0,0)-(0,0)
    • In the type family declaration for ‘Lambda_0123456789876543210’
  |
6 | $(singletons
  |  ^^^^^^^^^^^...

Truth be told, I'm not quite sure what to do about these sorts of examples. The only way I can imagine fixing this examples is by either rewriting the code or by sprinkling type annotations in random parts of the code. You might think that the takeaway here is "local bindings without top-level type signatures are bad", but that's not quite true, since GHC will continue to accept examples like this one:

$(promote [d|
  n :: forall a. Maybe a
  n = let z = Nothing
      in z
  |])

Sadly, we may just have to accept that GHC's kind inference just isn't up to the task in all cases and advise users to omit type signatures at their peril.

Metadata

Metadata

Assignees

No one assigned

    Labels

    bug

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions