Overly general kind for PAlternative

[RyanGlScott]

The kind of PAlternative should be (Type -> Type) -> Constraint, but it is instead:

λ> :k PAlternative
PAlternative :: forall {k}. (k -> Type) -> Constraint

We should fix this. Two possible ways to do so:

1. When promoting the Alternative class, give f an explicit kind signature, i.e.,

   class Applicative f => Alternative (f :: Type -> Type) where ...

   We may need to do this anyway as part of Make singletons buildable after GHC#23515 #601.

2. Currently, when singletons-th promotes a class definition, it omits the superclasses, as they aren't needed at the type level. This does hav one drawback, however: we do not benefit from any kind information that the superclasses might have. In the specific example of Alternative, its superclass Applicative is promoted to something with the correct kind:

   λ> :k PApplicative
   PApplicative :: (Type -> Type) -> Constraint
   

   Therefore, if we promoted the definition of Alternative to something like this:

   class PApplicative f => PAlternative f where ...

   Then GHC's kind inference would be able to figure out that f should be of kind Type -> Type.

I'm inclined to try option (2) first, but option (1) may also be worth doing (if not now, then as part of #601).

[RyanGlScott]

On second thought, option (2) is not as straightforward as I thought. Consider:

$(promote [d|
  class Supercls (T a) => Cls a where ...
  |]) 

Where T is a data type. Ideally, we would promote this to:

class PSupercls (T a) => PCls a where ...

But this requires figuring out that Supercls is a class so that we give it the prefix P, but we also do not want to give T the same prefix (since data types do not require them). This might be doable with some amount of (local) reification, but it feels like a lot of work for what should be a simple workaround. At this point, I'm not so convinced it's that simple.

---

Technically, this isn't a new problem, as you would encounter the same thing if you tried to promote a definition like this one:

f :: Dict (Supercls (T a))

That being said, singletons doesn't really support exotic definitions like this one, so the problem has never been an issue in practice.

[RyanGlScott]

Actually, I take back what I said above in #604 (comment). We have already solved this problem in the context of singling, since we want to turn things like Supercls (T a) into SSupercls (T a), not SSupercls (ST a). This is handled by the singPred function. Specifically, it ensures that when you single an application C (A_1 ... A_n), then the singled version will be SC (A_1 ... A_n). That is, C will be converted to SC, but the arguments will not be converted to SA_1 ... SA_n.

This approach works well for singPred, so we should be able to adapt it to a promotePred function that does something similar, but for promotion instead of singling.

[RyanGlScott]

I've tried out the promotePred function proposed in #604 (comment). It works well enough, but after trying it, I've realized that it doesn't go far enough. In particular, we now have:

λ> :k PAlternative
PAlternative :: (Type -> Type) -> Constraint

And similarly for PAlternative's promoted methods:

λ> :kind Empty
Empty :: forall (f :: Type -> Type) a. f a
λ> :kind (<|>)
(<|>) :: forall (f :: Type -> Type) a. f a -> f a -> f a

However, this doesn't affect the kinds of the promoted methods' defunctionalization symbols:

λ> :kind (<|>@#@$)
(<|>@#@$) :: forall {k} (f :: k -> Type) (a :: k).
             TyFun (f a) (f a ~> f a) -> Type
λ> :kind EmptySym0
EmptySym0 :: forall {k} (f :: k -> Type) (a :: k). f a

This means that this code still wouldn't work in a future version of GHC where the instantiation of type family instances is fully determined by the left-hand side (see #601). Moreover, it's not clear to me how we could repair the kinds of the defunctionalization symbols, which are defined separately from the PAlternative class. If GHC had the ability to use constraints in kinds, we might be able to make this work, but GHC doesn't support this (at least, not yet).

As such, I think the only way to truly fix this issue would be option (1) from #604 (comment). It's a bit sad, but oh well. We should also make sure to audit other classes in singletons-base in case they suffer from a similar issue.

[RyanGlScott]

Besides PAlternative, here are some other promoted classes and defunctionalization symbols that have overly general kinds:

• The defunctionalization symbols for (*>) in PApplicative:

  λ> :kind (*>@#@$)
  (*>@#@$) :: forall {k} (f :: k -> Type) (a :: k) (b :: k).
              TyFun (f a) (f b ~> f b) -> Type
  

• The defunctionalization symbols for (>>) in PMonad:

  λ> :kind (>>@#@$)
  (>>@#@$) :: forall {k} (m :: k -> Type) (a :: k) (b :: k).
              TyFun (m a) (m b ~> m b) -> Type
  

• The PMonadPlus class:

  λ> :kind PMonadPlus
  PMonadPlus :: forall {k}. (k -> Type) -> Constraint
  

• The PMonadFail class:

  λ> :kind PMonadFail
  PMonadFail :: forall {k}. (k -> Type) -> Constraint
  

• The defunctionalization symbols for Length in PFoldable:

  λ> :kind LengthSym0
  LengthSym0 :: forall {k} (t :: k -> Type) (a :: k).
                TyFun (t a) Natural -> Type