Skip to content

Kind classes compile with PolyKinds

I was asking around on #haskell to better understand the new language extension, -XTypeInType, and how it is different from -XPolyKinds.

To study it, I was working with the following small example:

{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, PolyKinds #-}
module Main where

-- Define a Type for the natural numbers, zero and a successor
data Nat = Z | S Nat

class Addable k where
  type (a :: k) + (b :: k) :: k

instance Addable Nat where
  type (Z + a) = a
  type (S a) + b = S (a + b)

main :: IO ()
main = putStrLn "Shouldn't this need TypeInType?"

(for more context, see https://gist.github.com/Tritlo/ce5510e80935ac398a33934ee47c7930)

Since according to a responder on #haskell, the ability to have kind classes required TypeInType, and should not work with PolyKinds.

As the documentation mentions that there could be leakage between PolyKinds and TypeInType and to report such leaks, I felt that I should report it.

Edited by Matthías Páll Gissurarson
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information