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.menen...@gmail.com [mailto:d4ve.menen...@gmail.com] On Behalf Of
David Menendez
Sent: 23 September 2016 19:51
To: Simon Peyton Jones <simo...@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
<simo...@microsoft.com<mailto:simo...@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 <d...@zednenem.com<mailto:d...@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%7C89f26f5e599e49b96e0c08d3e3e29e26%7C72f988bf86f141af91ab2d7cd011db47%7C1&sdata=c8g6ahf%2F8lun%2BPBof97s03XbePVwT4Buh6ef2bDSjLg%3D&reserved=0>>
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
