Kinds of type synonym arguments

[Ömer Sinan Ağacan]

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
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>