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

Tom Ellis tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk
Thu May 3 21:24:43 UTC 2018

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 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) = ()

More information about the Haskell-Cafe mailing list