title: How to create a "kind class" in Haskell, or ad-hoc polymorphism at the type-level using type families
body: <p>I'm studying the type family features of Haskell, and type level computation.
  It appears it's quite easy to get parametric polymorphism at the type-level using <code>PolyKinds</code>:</p>
  
  <pre><code>{-# LANGUAGE DataKinds, TypeFamilies, KindSignatures, GADTs, TypeOperators, UndecidableInstances, PolyKinds, MultiParamTypeClasses, FlexibleInstances #-}
  
  data NatK = Z | S NatK
  data IntK = I NatK NatK
  
  infix 6 +
  type family (x :: NatK) + (y :: NatK) :: NatK where
      Z     + y = y
      (S x) + y = S (x + y)
  
  -- here's a parametrically polymorphic (==) at the type-level
  -- it also deals specifically with the I type of kind IntK
  infix 4 ==
  type family (a :: k) == (b :: k) :: Bool where
      (I a1 a2) == (I b1 b2) = (a1 + b2) == (a2 + b1)
      a == a = True
      a == b = False
  </code></pre>
  
  <p>I can do things like <code>:kind! Bool == Bool</code> or <code>:kind! Int == Int</code> or <code>:kind! Z == Z</code> and <code>:kind! (I Z (S Z)) == (I (S Z) (S (S Z)))</code>.</p>
  
  <p>However I want to make <code>type +</code> ad-hoc polymorphic. So that it's constrained to the instances I give it. The 2 instances here, would be types of kind <code>NatK</code> and types of kind <code>IntK</code>.</p>
  
  <p>I first tried making it parametrically polymorphic:</p>
  
  <pre><code>infix 6 :+
  type family (x :: k) :+ (y :: k) :: k where
      Z         :+ y = y
      (S x)     :+ y = S (x :+ y)
      (I x1 x2) :+ (I y1 y2) = I (x1 :+ y1) (x2 :+ y2)
  </code></pre>
  
  <p>This works, as I can do <code>:kind! (I (S Z) Z) :+ (I (S Z) Z)</code>.</p>
  
  <p>However I can also do <code>:kind! Bool :+ Bool</code>. And this doesn't make any sense, but it allows it as a simple type constructor. I want to create a type family that doesn't allow such errant types.</p>
  
  <p>At this point I'm lost. I tried type classes with a <code>type</code> parameter. But that didn't work.</p>
  
  <pre><code>class NumK (a :: k) (b :: k) where
      type Add a b :: k
  
  instance NumK (Z :: NatK) (b :: NatK) where
      type Add Z b = b
  
  instance NumK (S a :: NatK) (b :: NatK) where
      type Add (S a) b = S (Add a b)
  
  instance NumK (I a1 a2 :: IntK) (I b1 b2 :: IntK) where
      type Add (I a1 a2) (I b1 b2) = I (Add a1 b1) (Add a2 b2)
  </code></pre>
  
  <p>It still allows <code>:kind! Add Bool Bool</code>.</p>
  
  <p>Does this have something to do with the <code>ConstraintKinds</code> extension, where I need to constrain the <code>:+</code> or <code>Add</code> to some "kind class"?</p>