Type families in kind signatures with TypeInType

[Simon Peyton Jones]

This is an example of https://ghc.haskell.org/trac/ghc/ticket/12088.

The “type instance T List” declaration actually depends on the “type instance K List” declaration; the latter must be typechecked before the former.  But this dependency is absolutely unclear.  There’s a long discussion on the thread.  Bottom line: we don’t know a solid automated way to spot this kind of problem, so  I think we are going to ask for programmer assistance.  In this case, we’d put a “separator” after the “type instance K List” decl, to explain that it must be done first:

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

Currently you have to write $(return []) to get the separator, but I think we’ll add a special separator.

Simon


From: Glasgow-haskell-users [mailto:glasgow-haskell-users-bounces at haskell.org] On Behalf Of David Menendez
Sent: 23 September 2016 05:48
To: glasgow-haskell-users at haskell.org Mailing List <Glasgow-haskell-users at haskell.org>
Subject: Type families in kind signatures with TypeInType

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<mailto:dave at zednenem.com>>
<http://www.eyrie.org/~zednenem/<https://na01.safelinks.protection.outlook.com/?url=http:%2f%2fwww.eyrie.org%2f~zednenem%2f&data=01%7C01%7Csimonpj%40microsoft.com%7C740be9e2f66146e93b1308d3e36cdcda%7C72f988bf86f141af91ab2d7cd011db47%7C1&sdata=r83909O38f2c%2feaujupnsW%2fSy23XLouk2unQBGTCB8w%3d>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20160923/77f338e0/attachment.html>