Is there a way to use a kind level class with type families?

Question

I was trying to define an integer type, and a typeclass that would allow operations on all Numberlike types.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE UndecidableInstances #-}
module TypeLevelInteger where
import qualified GHC.TypeLits as TL
import GHC.TypeLits (Natural,Nat)
import Data.Kind (Constraint)

type TypeNum :: k -> Constraint
class TypeNum k where 
    type (*) :: k -> k -> k
    type (+) :: k -> k -> k
    type (-) :: k -> k -> k
    type ToNat :: k -> Nat

I was then going to define an Integer type and make it an instance of NumType The problem is I get the error

 Expected a type, but ‘k’ has kind ‘k1’
  ‘k1’ is a rigid type variable bound by
    the class declaration for ‘TypeNum’
    at /workspaces/codespaces-haskell/TypeLevelInteger.hs:36:17-31
• In the kind ‘k -> k -> k’
  In the associated type family declaration for ‘*’

What can I do?

Answer 1

Look, everyone gets mixed up about this, often multiple times over their functional programming lives. Here's another way of looking at it that may help.

The thing that makes Type special is that it's the kind of all types that have values. So, if you have a :: t, then a is a value of type t which implies that t must have kind Type. Note that t can still be any type, as long as that type has kind Type. So, a :: t implies t :: Type, whatever t is. This is what @HTNW means in the comment that anything to the right of :: (i.e., t in a :: t) must have kind Type (i.e., t :: Type).

When you write the kind signature:

type (+) :: k -> k -> k

you are defining a type-level operator that takes two values, one on the left and one on the right, as in the type-level expression:

typexp1 + typexp2

But, if this expression is to make sense, then typexp1 and typexp2 must be (type-level) values of type k. In other words, typexp1, typexp2 :: k. That implies k :: Type because only types k of kind Type can have values like typexp1 and typexp2.

This is still true for an expression like:

[] + Maybe

Sure, [] and Maybe aren't of kind Type. Rather, they are of kind k = Type -> Type (i.e., [], Maybe :: Type -> Type). But everything's still fine because k :: Type for that particular choice of k.

This is why in your class:

class TypeNum k where
  type (+) :: k -> k -> k

the only reasonable kind of k is k :: Type. Imagine if we tried to define an instance for some k :: Type -> Type, like k = Maybe:

instance TypeNum Maybe where
  type x + y = ...

The type signature for (+) would be specialized to:

type (+) :: Maybe -> Maybe -> Maybe

What could this possibly mean? There are no type-level expressions of kind Maybe that we could supply as the left and right arguments of (+) because Maybe has the wrong kind (i.e., it's Maybe :: Type -> Type, a kind of types, like Maybe and [], that don't have any values).

That's why

type (+) :: k -> k -> k

implies k :: Type and why

class TypeNum k where
  type (+) :: k -> k -> k

implies

type TypeNum :: Type -> Constraint

The type-level argument k to TypeNum must be of kind Type (i.e., Int, not Maybe) for the signature k -> k -> k of the (+) operator to make sense.

The error message is just a confusing way of saying that the kind signature:

type TypeNum :: k1 -> Constraint

is too general because k1 is known to be equal to Type.