[Haskell-cafe] Strange error with GADT DataKinds -- needs TypeInType!?

[Tom Ellis]

Can anyone explain why the type instance for K is fine but the one for I
needs TypeInType?  (It does indeed work when I turn on TypeInType.)



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

data T a b where
  K :: b -> T a b
  I :: T a a

type family F (a :: T ka kb)

-- Data constructor ‘I’ cannot be used here
--        (Perhaps you intended to use TypeInType)
-- type instance F 'I = ()

type instance F ('K b) = ()