Polymorphism over unboxed tuples

[Ryan Scott]

Section 4.2 of the paper Levity Polymorphism [1] makes a bold claim
about polymorphism for unboxed tuples:

  Note that this format respects the computational irrelevance of
nesting of unboxed tuples. For example, these three types all have the
same kind, here written PFP for short:

  type PFP = TYPE '[PtrRep, FloatRep, PtrRep]
  (# Int, (# Float#, Bool #) #)        :: PFP
  (# Int, Float#, Bool #)              :: PFP
  (# (# Int, (# #) #), Float#, Bool #) :: PFP

But in GHC, that isn't the case! Here's proof of it from a recent GHCi session:

  GHCi, version 8.3.20170322: http://www.haskell.org/ghc/  :? for help
  λ> :set -XUnboxedTuples -XMagicHash
  λ> import GHC.Exts
  λ> :kind (# Int, (# Float#, Bool #) #)
  (# Int, (# Float#, Bool #) #) :: TYPE
                                     ('TupleRep '['LiftedRep,
'TupleRep '['FloatRep, 'LiftedRep]])
  λ> :kind (# Int, Float#, Bool #)
  (# Int, Float#, Bool #) :: TYPE
                               ('TupleRep '['LiftedRep, 'FloatRep,
'LiftedRep])
  λ> :kind (# (# Int, (# #) #), Float#, Bool #)
  (# (# Int, (# #) #), Float#, Bool #) :: TYPE
                                            ('TupleRep
                                               '['TupleRep
'['LiftedRep, 'TupleRep '[]], 'FloatRep,
                                                 'LiftedRep])

As you can see, each of these different nestings of unboxed tuples
yields different kinds, so they most certainly do *not* uphold the
property claimed in the paper.

Is this a bug? Or is there some reason that GHC implemented it differently?

Ryan S.
-----
[1] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/levity-1.pdf