Type families in kind signatures with TypeInType

[David Menendez]

On Fri, Sep 23, 2016 at 3:19 AM, Simon Peyton Jones <simonpj at microsoft.com>
wrote:

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

Interesting. Is this case also an example, or is it a non-feature?

class C t where
    type K t :: Type
    type T t :: K t -> Type

    m :: t -> T t a

min.hs:21:17: error:
    • Type constructor ‘K’ cannot be used here
        (it is defined and used in the same recursive group)
    • In the kind ‘K t -> Type’
Failed, modules loaded: none.

GHC accepts this if K t is moved outside of C.


> 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.
>
>
Yes, this works. Thanks.

It would be disappointing if this is the best we can do, but I guess other
dependent languages don’t need to deal with open type families and
everything being potentially mutually recursive.

-- 
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/81a9ae60/attachment.html>