Re: What promotes to (* :: BOX) ?

Hi guys, I'll have a go at implementing 'data kind'. I've been a bit busy lately but things are getting back to normal, and a colleague of mine is willing to help too, so hopefully we can get it done. -Iavor On Wed, Apr 3, 2013 at 4:24 AM, Simon Peyton-Jones wrote:

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@haskell.org [mailto:ghc-devs-bounces@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 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 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 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@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs****

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs****

** **

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs****

** **