Kinds of type synonym arguments

[Ömer Sinan Ağacan]

Oh sorry, I just mean that currently boxed tuples don't accept unboxed types:

    λ> :k ( Int#, Int )

    <interactive>:1:3: error:
        • Expecting a lifted type, but ‘Int#’ is unlifted
        • In the type ‘(Int#, Int)’

But unboxed variant of exactly the same thing is accepted:

    λ> :k (# Int#, Int #)
    (# Int#, Int #) :: #

I was hoping make these two the same by adding levity arguments and making type
arguments depend on levity arguments, just like how unboxed tuple types are
implemented (as described in Note [Unboxed tuple levity vars]).

The changes in tuple DataCon and TyCon generation is fairly simple (in fact I
just implemented that part) but the rest of the compiler started panicking. So
my question is, is there a reason for not doing this, because otherwise I'd
like to fix panics etc. and make this change.

2015-12-15 18:08 GMT-05:00 Simon Peyton Jones <simonpj at microsoft.com>:
> What is "this" that you propose to implement?  Is there a wiki page that describes the design?
>
> Simon
>
> | -----Original Message-----
> | From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Ömer Sinan
> | Agacan
> | Sent: 15 December 2015 23:06
> | To: Richard Eisenberg <eir at cis.upenn.edu>
> | Cc: ghc-devs <ghc-devs at haskell.org>
> | Subject: Re: Kinds of type synonym arguments
> |
> | Hi Richard,
> |
> | Now that we have levity arguments I'm wondering if we should go ahead and
> | implement this. The code is already there - unboxed tuples have levity
> | arguments and then type arguments depend on the levity arguments, so this
> | works:
> |
> |     λ> :k (# Int, Int# #)
> |     (# Int, Int# #) :: #
> |
> | But this doesn't because boxed tuples are not implemented that way:
> |
> |     λ> :k ( Int, Int# )
> |
> |     <interactive>:1:8: error:
> |         • Expecting a lifted type, but ‘Int#’ is unlifted
> |         • In the type ‘(Int, Int#)’
> |
> | The implementation looked fairly simple so I just tried to lift this
> | restriction (I basically merged the code that generates TyCons and DataCons
> | for
> | unboxed and boxed tuples in WiredInTys), but some other parts of the compiler
> | started to panic. Should I investigate this further or are there any problems
> | with this that we need to solve first?
> |
> | If there's a problem with this I think we should at least add a NOTE in
> | TysWiredIn. Note [Unboxed tuple levity vars] explains how levity vars are
> | used
> | in unboxed tuples, but there's no comments or notes about why we don't do the
> | same for boxed tuples.
> |
> | Also, I was wondering if OpenKind is deprecated now. Can I assume that levity
> | arguments do that work now and we no longer need OpenKind?
> |
> | Thanks
> |
> | 2015-12-06 21:45 GMT-05:00 Richard Eisenberg <eir at cis.upenn.edu>:
> | > I think this is a consequence of the rule that we never abstract over types
> | of kind #. But I believe this should work with my branch:
> | >
> | >> type Tuple (a :: TYPE v1) (b :: TYPE v2) = (# a, b #)
> | >
> | > The user would have to request that the synonym be used over both * and #,
> | but the synonym should work. The need to request the special treatment might
> | be lifted, but we'd have to think hard about where we want the generality by
> | default and where we want simpler behavior by default.
> | >
> | > Richard
> | >
> | > On Dec 6, 2015, at 1:55 PM, Ömer Sinan Ağacan <omeragacan at gmail.com> wrote:
> | >
> | >> In this program:
> | >>
> | >>    {-# LANGUAGE MagicHash, UnboxedTuples #-}
> | >>
> | >>    module Main where
> | >>
> | >>    import GHC.Prim
> | >>    import GHC.Types
> | >>
> | >>    type Tuple a b = (# a, b #)
> | >>
> | >>    main = do
> | >>      let -- x :: Tuple Int# Float#
> | >>          x :: (# Int#, Float# #)
> | >>          x = (# 1#, 0.0# #)
> | >>
> | >>      return ()
> | >>
> | >> If I use the first type declaration for 'x' I'm getting this error
> | message:
> | >>
> | >>    Expecting a lifted type, but ‘Int#’ is unlifted
> | >>
> | >> Indeed, if I look at the kinds of arguments of 'Tuple':
> | >>
> | >>    λ:7> :k Tuple
> | >>    Tuple :: * -> * -> #
> | >>
> | >> It's star. I was wondering why is this not 'OpenKind'(or whatever the
> | >> super-kind of star and hash). Is there a problem with this? Is this a bug?
> | >> Or is this simply because type synonyms are implemented before OpenKinds?
> | >> _______________________________________________
> | >> ghc-devs mailing list
> | >> ghc-devs at haskell.org
> | >>
> | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell.
> | org%2fcgi-bin%2fmailman%2flistinfo%2fghc-
> | devs&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce7184dc9345c4f9123c308
> | d305a4631f%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=sYBDmz3zltvhkRvFsuo1h
> | OiBLqO6Qsu7N0zpzUK7iPY%3d
> | >>
> | >
> | _______________________________________________
> | ghc-devs mailing list
> | ghc-devs at haskell.org
> | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell.
> | org%2fcgi-bin%2fmailman%2flistinfo%2fghc-
> | devs%0a&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce7184dc9345c4f9123c
> | 308d305a4631f%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=A4khlPGkSRO%2f4S%2
> | bv%2fUxEiJj9DewPXVbsuX7GAzHB0FQ%3d