What is the kind of polymorphic/polykinded tuples?

Question

While I was going through the haskell-excercises questions. I saw the following code which creates an aggregate Constraint by applying each type to a Constraint constructor. In GHC it seems deeply nested tuples of Constraints are still of kind Constraint (perhaps flattened ?).

{-# LANGUAGE DataKinds     #-}
{-# LANGUAGE PolyKinds     #-}
{-# LANGUAGE TypeFamilies  #-}
{-# LANGUAGE TypeOperators #-}


type family All (c :: Type -> Constraint) (xs :: [Type]) :: Constraint where
  All c '[] = ()
  All c (x ': xs) = (c x, All c xs)

-- >>> :kind! All
-- All :: (* -> Constraint) -> [*] -> Constraint
-- = All

-- >>> :kind! All Eq '[Int, Double, Float]
-- All Eq '[Int, Double, Float] :: Constraint
-- = (Eq Int, (Eq Double, (Eq Float, () :: Constraint)))

I tried to generalize it using PolyKinds extension as following.

{-# LANGUAGE DataKinds     #-}
{-# LANGUAGE PolyKinds     #-}
{-# LANGUAGE TypeFamilies  #-}
{-# LANGUAGE TypeOperators #-}


type family All' (c :: k -> r) (xs :: [k]) :: r where
  All' c '[] = ()
  All' c (x ': xs) = (c x, All' c xs)

-- >>> :kind! All'
-- All' :: (k -> r) -> [k] -> r
-- = All'

--- This one works. Tuples of Types is a Type.
-- >>> :kind! All' Maybe '[Int, Double, Float]
-- All' Maybe '[Int, Double, Float] :: *
-- = (Maybe Int, (Maybe Double, (Maybe Float, ())))

--- However this one gets stuck.
-- >>> :kind! All' Eq '[Int, Double, Float]
-- All' Eq '[Int, Double, Float] :: Constraint
-- = All' Eq '[Int, Double, Float]

Is the kind of '(,) (a :: k) (b :: k) also of kind k. Looking below it doesn't seems so, so I wonder why the type family definition All' c (x ': xs) = (c x, All' c xs) was accepted in the first place (considering the type family return kind was r)?

λ> :kind! '(,)
'(,) :: a -> b -> (a, b)
= '(,)

λ> :kind! '(,) ('True :: Bool) ('False :: Bool)
'(,) ('True :: Bool) ('False :: Bool) :: (Bool, Bool)
= '( 'True, 'False)

UPDATE

As @Daniel Wagner already mentioned below the (,) used here is considered as Type -> Type -> Type and the kind parameter r is instantiated to Type within the second equation above (All' c (x ': xs) = (c x, All' c xs)). In fact if we had used '(,), it would have correctly returned a type error. I was able to further confirm it using a technique described in this blog post as following (All' is instantiated with kinds k, and *):

λ> :set -fprint-explicit-kinds
λ> :info All'
type All' :: forall k r. (k -> r) -> [k] -> r
type family All' @k @r c xs where
  forall k (c :: k -> *). All' @k @(*) c ('[] @k) = ()
  forall k (c :: k -> *) (x :: k) (xs :: [k]).
    All' @k @(*) c ((':) @k x xs) = (c x, All' @k @(*) c xs)

Answer 1

There is a syntactic pun here. There are actually several different commas, with differing kinds:

 (,) :: Type -> Type -> Type
 (,) :: Constraint -> Constraint -> Constraint -- ...ish
'(,) :: a -> b -> (a, b)

Note that none of these kinds unify with any other. Additionally, the second one is a bit of a lie; if x :: Constraint and y :: Constraint, then (x, y) :: Constraint, but the comma cannot be put prefix as in (,) x y.

When attempting to disambiguate the first two, GHC assumes you are using (,) :: Type -> Type -> Type unless you are in a place which syntactically cannot use that (e.g. to the left of an =>) or you have given an explicit kind annotation of :: Constraint. The single-tick ' disambiguates between the first two and the last one.