What promotes to (* :: BOX) ?

[Simon Peyton-Jones]

For the record, I’m good with going ahead with “Solution 2” on

http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData

if anyone wants to execute on it.

Simon

From: ghc-devs-bounces at haskell.org [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Iavor Diatchki
Sent: 02 April 2013 17:49
To: Richard Eisenberg
Cc: José Pedro Magalhães; ghc-devs
Subject: Re: What promotes to (* :: BOX) ?

Hello,

I've been using an existential quantifier for this.  It
looks weird (and I think we should fix this as discussed) but it is the current workaround:

data MyKind = forall star. T star

-- T :: * -> MyKind

-Iavor



On Tue, Apr 2, 2013 at 7:11 AM, Richard Eisenberg <eir at cis.upenn.edu<mailto:eir at cis.upenn.edu>> wrote:
For more immediate satisfaction (i.e., before we get around to updating GHC in the manner suggested on the wiki page), you have to use a parameterized type and then specialize it to *:

> data Prom2 a = Typic a

Now, we have (Prom2 * :: BOX) with (Typic Int :: Prom2 *).

Unfortunately, we have no kind synonyms, so you have to insert the * parameter every time you want to use the Prom2 kind. As Pedro suggests, this is a known weakness of the current system.

Richard

On Apr 2, 2013, at 8:55 AM, José Pedro Magalhães <jpm at cs.uu.nl<mailto:jpm at cs.uu.nl>> wrote:


Hi Gabor,

See http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData
Comments on that discussion are welcome.


Cheers,
Pedro
On Tue, Apr 2, 2013 at 2:51 PM, Gabor Greif <ggreif at gmail.com<mailto:ggreif at gmail.com>> wrote:
Hi devs!

I guess I found a gap in the promotion mechanism:

> data Prom1 = Symic Symbol

gets promoted to to a kind (Prom1 :: BOX) with (Symic "AAA" :: Prom1).
So far so good.

But how can I define by promotion (Prom2 :: BOX) with (Typic Int :: Prom2) ?

I'd like to write

> data Prom2 = Typic Type

but haven't found such a beast in TypeLits. So my question is
basically, which type-level identifier promotes to (* :: BOX) when
mentioned in a `data` definition?

I am thankful for any hints!

Cheers,

    Gabor

_______________________________________________
ghc-devs mailing list
ghc-devs at haskell.org<mailto:ghc-devs at haskell.org>
http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
ghc-devs at haskell.org<mailto:ghc-devs at haskell.org>
http://www.haskell.org/mailman/listinfo/ghc-devs


_______________________________________________
ghc-devs mailing list
ghc-devs at haskell.org<mailto:ghc-devs at haskell.org>
http://www.haskell.org/mailman/listinfo/ghc-devs

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130403/7ed8374e/attachment-0001.htm>