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

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 mailto:eir@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 mailto:jpm@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 mailto:ggreif@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@haskell.orgmailto:ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list ghc-devs@haskell.orgmailto:ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list ghc-devs@haskell.orgmailto:ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

On 4/2/13, Iavor Diatchki wrote:

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

Hi Iavor, thanks for the tip, this works nicely. I only have to restrict (t :: T *) everywhere a MyKind is needed, to get what I want. I tried Richard's solution too (with a universally quantified extra parameter). It appeared to work too, but it needed much more extra annotations. I believe a kind synonym would have helped, but we do not have those, right? Cheers, Gabor

-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