Type families in kind signatures with TypeInType

[David Menendez]

Should the code below work in GHC 8.0.1?

    {-# LANGUAGE TypeInType, TypeFamilies #-}

    import Data.Kind (Type)

    type family K t :: Type
    type family T t :: K t -> Type

    data List

    type instance K List = Type
    type instance T List = []


Right now, I get an error like this one:

min.hs:12:24: error:
    • Expected kind ‘K List -> Type’, but ‘[]’ has kind ‘* -> *’
    • In the type ‘[]’
      In the type instance declaration for ‘T’

which is puzzling, since K List -> Type and * -> * should be the same.

Obviously, TypeInType is experimental and incomplete. I’m just wondering if
this sort of thing is expected to work, or if I’m doing something not yet
supported or never to be supported

In particular, the kind signature for T is forall t -> K t -> Type, which
looks like DependentHaskell.

-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20160923/bfee1bad/attachment.html>