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...