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

 

 

Ah, that’s quite different!  We should do strongly-connected-component analysis of the associated-type declarations within a single class declaration…. but we don’t currently do that.   No difficulty in principle, I think.

 

You could open a ticket.   (Do include a link to this email thread and to #12088)

 

Simon

 

 

From: d4ve.menendez@gmail.com [mailto:d4ve.menendez@gmail.com] On Behalf Of David Menendez
Sent: 23 September 2016 19:51
To: Simon Peyton Jones <simonpj@microsoft.com>
Cc: glasgow-haskell-users@haskell.org Mailing List <Glasgow-haskell-users@haskell.org>
Subject: Re: Type families in kind signatures with TypeInType

 

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

 

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@zednenem.com>
<http://www.eyrie.org/~zednenem/>