Kinds of type synonym arguments

[Simon Peyton Jones]

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