Quantifying class methods' kind variables using `TypeAbstractions` is fragile when higher-order kinds are involved

While writing a fix for #604, I attempted to give Traversable a standalone kind signature, only for singletons-th to generate code that failed to kind-check. Here is a minimized example of the problem:

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

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

$(promoteOnly [d|
  type Traversable' :: (Type -> Type) -> Constraint
  class (Functor t, Foldable t) => Traversable' t where
    traverse' :: Applicative f => (a -> f b) -> t a -> t (f b)
  |])

This will generate the following code:

    type Traverse'Sym0 :: forall (t_abhI :: Type -> Type)
                                 a_abhK
                                 f_abhJ
                                 b_abhL. (~>) ((~>) a_abhK (f_abhJ b_abhL)) ((~>) (t_abhI a_abhK) (t_abhI (f_abhJ b_abhL)))
    data Traverse'Sym0 :: (~>) ((~>) a_abhK (f_abhJ b_abhL)) ((~>) (t_abhI a_abhK) (t_abhI (f_abhJ b_abhL)))
      where
        Traverse'Sym0KindInference :: SameKind (Apply Traverse'Sym0 arg_abhO) (Traverse'Sym1 arg_abhO) =>
                                      Traverse'Sym0 a6989586621679053181
    type instance Apply Traverse'Sym0 a6989586621679053181 = Traverse'Sym1 a6989586621679053181
    instance SuppressUnusedWarnings Traverse'Sym0 where
      suppressUnusedWarnings = snd ((,) Traverse'Sym0KindInference ())
    type Traverse'Sym1 :: forall (t_abhI :: Type -> Type)
                                 a_abhK
                                 f_abhJ
                                 b_abhL. (~>) a_abhK (f_abhJ b_abhL)
                                         -> (~>) (t_abhI a_abhK) (t_abhI (f_abhJ b_abhL))
    data Traverse'Sym1 (a6989586621679053181 :: (~>) a_abhK (f_abhJ b_abhL)) :: (~>) (t_abhI a_abhK) (t_abhI (f_abhJ b_abhL))
      where
        Traverse'Sym1KindInference :: SameKind (Apply (Traverse'Sym1 a6989586621679053181) arg_abhO) (Traverse'Sym2 a6989586621679053181 arg_abhO) =>
                                      Traverse'Sym1 a6989586621679053181 a6989586621679053182
    type instance Apply (Traverse'Sym1 a6989586621679053181) a6989586621679053182 = Traverse' a6989586621679053181 a6989586621679053182
    instance SuppressUnusedWarnings (Traverse'Sym1 a6989586621679053181) where
      suppressUnusedWarnings = snd ((,) Traverse'Sym1KindInference ())
    type Traverse'Sym2 :: forall (t_abhI :: Type -> Type)
                                 a_abhK
                                 f_abhJ
                                 b_abhL. (~>) a_abhK (f_abhJ b_abhL)
                                         -> t_abhI a_abhK -> t_abhI (f_abhJ b_abhL)
    type family Traverse'Sym2 @(t_abhI :: Type
                                          -> Type) @a_abhK @f_abhJ @b_abhL (a6989586621679053181 :: (~>) a_abhK (f_abhJ b_abhL)) (a6989586621679053182 :: t_abhI a_abhK) :: t_abhI (f_abhJ b_abhL) where
      Traverse'Sym2 a6989586621679053181 a6989586621679053182 = Traverse' a6989586621679053181 a6989586621679053182
    type PTraversable' :: (Type -> Type) -> Constraint
    class PTraversable' (t_abhI :: Type -> Type) where
      type family Traverse' @(t_abhI :: Type
                                        -> Type) @a_abhK @f_abhJ @b_abhL (arg_abhM :: (~>) a_abhK (f_abhJ b_abhL)) (arg_abhN :: t_abhI a_abhK) :: t_abhI (f_abhJ b_abhL)

Which causes GHC to error thusly:

Bug.hs:13:2: error: [GHC-83865]
    • Expected kind ‘* -> *’, but ‘f_abhJ’ has kind ‘*’
    • In the second argument of ‘(~>)’, namely ‘(f_abhJ b_abhL)’
      In the kind ‘(~>) a_abhK (f_abhJ b_abhL)’
      In the associated type family declaration for ‘Traverse'’
   |
13 | $(promoteOnly [d|
   |  ^^^^^^^^^^^^^^^^...

To see what the problem is, look more closely at the definition of Traverse':

    type PTraversable' :: (Type -> Type) -> Constraint
    class PTraversable' (t_abhI :: Type -> Type) where
      type family Traverse' @(t_abhI :: Type
                                        -> Type) @a_abhK @f_abhJ @b_abhL (arg_abhM :: (~>) a_abhK (f_abhJ b_abhL)) (arg_abhN :: t_abhI a_abhK) :: t_abhI (f_abhJ b_abhL)

Note that the @f_abhJ binder does not have an explicit kind signature. When I introduced the ability for promoted class methods to bind their kind variables using TypeAbstractions (in #596), I had assumed that GHC would be able to infer that f_abhJ :: Type -> Type. The reality is much more dire, however: because f_abhJ lacks an explicit kind signature, GHC assumes that f_abhJ :: Type! As a result, there is a kind mismatch.

I'd like to blame GHC here, but I'm not sure that I could even call this behavior a GHC bug. GHC has a convention that when you write type family T a (without any other kind information), then GHC will default a's kind to Type. As such, if you write:

type C :: Type -> Constraint
class C c where
  type T a c

Then it seems consistent for GHC to default a's kind to Type as well. Similarly if you wrote T @a c.

This is a perfectly consistent design on GHC's end, but one that is very inconvenient for singletons's needs. The only way to repair this would be to annotate f_abhJ with an explicit Type -> Type kind signature, but this would require some cleverness in order to infer. In general, you'd likely need full-blown kind inference in order to do this well, and I am very reluctant to go down that path. Nor can we write something like (f_abhJ :: _) and leverage GHC's kind inference, since GHC doesn't allow writing wildcard types in type family declarations.

Unfortunately, I think this means that the proposal in #589 is simply not viable with the current state of GHC. I propose to revert #596, especially given that this is a blocker for fixing #604.

goldfirere / singletons

Quantifying class methods' kind variables using `TypeAbstractions` is fragile when higher-order kinds are involved #605