Kind polymorphism and unboxed types: bad things are happening

changed weight to 5

added Ttask Trac import TypeInType typechecker labels

Bother. There are worms under this stone. Is this OK?

type family F a :: k
type instance F Int = Int#
type instance F Bool = Int

This looks very bad to me. Now the runtime representation of (F a) might be boxed or unboxed. Eeek. And indeed Type.typePrimRep assumes that any AppTy is a boxed pointer; and any TyConApp whose tycon is not primitive is also a boxed pointer.

So if we can have type families with a poly-kinded result, then we can't allow kind variables to be instantiated with TYPE Unlifted (or anything levity polymorphic). Sigh.

And if we have type constructors like State# :: TYPE Lifted -> TYPE Unlifted, which we do, then similar problems occur if we have

type instance F Char = State#

because now (F Char Int) has a zero-width representation. So we can't allow that kind variable to be instantiated with * -> # either.

This is what Note [The kind invariant] was all about, and we have been quietly ignoring it.

I think we must allow type families to have a poly-kinded result. So do we have to impose (painful to specify, painful to implement) restrictions on how kind variables can be instantiated.

Ironically, we have just loosened this up; see #11120 (closed) #11471 (closed), first bullet, and #11465 (closed).

I'm really not sure what to do here.

I wrote this code to try to get a seg-fault or something:

import GHC.Exts
import Data.Proxy

type family F a :: k

type instance F Int = Int#

f :: Proxy a -> F a -> F a
f _ x = x

bad = f (undefined :: Proxy Int#) 3#

But instead I got some truly bizarre error messages

Foo.hs:15:10: error:
    • Expected kind ‘Proxy Int#’,
        but ‘undefined :: Proxy Int#’ has kind ‘Proxy Int#’
    • In the first argument of ‘f’, namely ‘(undefined :: Proxy Int#)’
      In the expression: f (undefined :: Proxy Int#) 3#
      In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3#

Foo.hs:15:35: error:
    • Couldn't match a lifted type with an unlifted type
      When matching types
        F Int# :: *
        Int# :: #
    • In the second argument of ‘f’, namely ‘3#’
      In the expression: f (undefined :: Proxy Int#) 3#
      In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3#

We get a bit more of a clue with -fprint-explicit-kinds

Foo.hs:15:10: error:
    • Expected kind ‘Proxy * Int#’,
        but ‘undefined :: Proxy Int#’ has kind ‘Proxy # Int#’
    • In the first argument of ‘f’, namely ‘(undefined :: Proxy Int#)’
      In the expression: f (undefined :: Proxy Int#) 3#
      In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3#

Foo.hs:15:35: error:
    • Couldn't match a lifted type with an unlifted type
      When matching types
        F * Int# :: *
        Int# :: #
    • In the second argument of ‘f’, namely ‘3#’
      In the expression: f (undefined :: Proxy Int#) 3#
      In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3#

but clearly life is not good here.

changed title from Note [The kind invariant] in TyCoRep needs to be updated to Kind polymorphism and unboxed types: bad things are happening

You also might be interested in [https://phabricator.haskell.org/D1807#53426]. I was quite surprised to find that nothing blew up here.

mentioned in issue #11473 (closed)

Replying to [ticket:11471#comment:114456 bgamari]:

You also might be interested in [https://phabricator.haskell.org/D1807#53426]. I was quite surprised to find that nothing blew up here.

Eeek. See #11473 (closed).

Trac metadata

Trac field	Value
Type	Task → Bug

added Tbug label and removed Ttask TypeInType labels

Re ticket:11471#comment:114454: Try with -fprint-explicit-coercions. Here's what I think is happening, though I don't have a fresh enough build locally to check:

foo :: Proxy a -> F a -> F a becomes foo :: forall k2 (a :: *). Proxy * a -> F k2 a -> F k2 a. Note that F is not polymorphic in the kind of a, which defaults to *. We also know that k2 must be either * or #, because F k2 a :: k2 is an argument of an arrow. GHC wisely defaults it to *, leading to the second error.

Once we clean up kind errors with coercions, I think the error messages will improve. There's also clearly the word kind appearing where type should in the first message. But these errors are legitimate.

As for the larger issue, we'll need to discuss.

assigned to @rae

Richard and I developed a plan this afternoon.

Principle: the kind of a type tells you its runtime representation (both width and pointer-hood).

Currently we have

data Levity = Lifted | Unlifted

With this new principle we would have

data Levity
  = L    -- Lifted, boxed, represented by a pointer
  | UB   -- Unlifted, boxed, represented by a pointer
  | UV   -- Unboxed, zero width
  | UW32 -- Unboxed, represented by a 32 bit word
  | UW64 -- Unboxed, represented by a 64 bit word
  | UF32 -- Unboxed, represented by a 32 bit float
  | UF64 -- Unboxed, represented by a 64 bit float
  ...etc...

Pretty much one case for each constructor in PrimRep.

And that's it really. Now typePrimRep just takes the kind, and converts it to a PrimRep.

This is a nice generalisation, and (we think) solves the problem.

We need a Levity wiki page!!

We have a Levity wiki page: NoSubKinds

It needs an update.

mentioned in issue #11549 (closed)

By the way, I know the name of the extension is TypeInType, but might it not make more sense to have a separate Levity constructor for kinds? Say * :: TYPE T. While the values of Int are things like 1 :: Int, and they are lifted and boxed, the "values" of * are things like Int :: *, and... Int is not really represented by anything at runtime. But if it was, it wouldn't necessarily be a lifted, boxed pointer. Maybe you want lazy evaluation on the value level, but strict evaluation on the type level, along with a totally different runtime representation for types.

I don't know of any reason why you would want to abstract over specifically (regular types of kind * + kinds). It seems to me that in such cases it would make just as much sense to allow unboxed types as well. On the other hand, I do realize that the name * is a lot more convenient than writing forall (a :: RuntimeRep). ... (TYPE a), and maybe that is the real issue...?

I actually quite like this idea. I do think it's too late for 8.0. And the long-term plan is to make Type (that is, *) and TypeRep to be the same thing. So * :: * really will make sense! But perhaps if this idea came along earlier, we would have adopted it.

I'm afraid I don't understand the idea of ticket:11471#comment:115631. I'm happy that Richard says he likes it, but what precisely is the suggestion?

For the record, the current plan (implemented in D1891) looks like this,

data RuntimeRep = PtrRep Levity   -- ^ represented by a pointer
                | VecRep VecCount VecElem   -- ^ a SIMD vector type
                | VoidRep         -- ^ erased entirely
                | IntRep          -- ^ signed, word-sized value
                | WordRep         -- ^ unsigned, word-sized value
                | Int64Rep        -- ^ signed, 64-bit value (on 32-bit only)
                | Word64Rep       -- ^ unsigned, 64-bit value (on 32-bit only)
                | AddrRep         -- ^ A pointer, but /not/ to a Haskell value
                | FloatRep        -- ^ a 32-bit floating point number
                | DoubleRep       -- ^ a 64-bit floating point number
                | UnboxedTupleRep -- ^ An unboxed tuple; this doesn't specify a concrete rep

data VecCount = Vec2 | Vec4 | Vec8 | Vec16 | Vec32 | Vec64

data VecElem = Int8ElemRep  | Int16ElemRep  | Int32ElemRep  | Int64ElemRep
             | Word8ElemRep | Word16ElemRep | Word32ElemRep | Word64ElemRep
             | FloatElemRep | DoubleElemRep

data Levity = Lifted
            | Unlifted

data TYPE (rep :: RuntimeRep) :: TYPE ('PtrRep 'Lifted)

Simon says,

I'm afraid I don't understand the idea of ticket:11471#comment:115631. I'm happy that Richard says he likes it, but what precisely is the suggestion?

I think Reid was suggesting that TYPE 'Lifted :: TYPE 'TypeRep or something along those lines (where TypeRep would look very similar to VoidRep). This reflects the fact types (e.g. Int) have no runtime representation.

So under ticket:11471#comment:114619 as I understand it * is a synonym for TYPE L. We can make a table

  1  ::    Int   and     Int  :: * = TYPE L
  2# ::    Int#  and     Int# ::     TYPE UW64
3.0# :: Double#  and  Double# ::     TYPE UF64
 Int ::    *     and     *    :: * = TYPE L

The last line is given to us by TypeInType. But to me the thing Int seems at least as different from the thing 1 as the things 1, 2# and 3.0# are from each other. So, the suggestion is to add another constructor T to RuntimeRep and replace the last line with

 Int ::    *     and     *    ::     TYPE T

We could define a synonym type Kind = TYPE T and then * :: Kind.

The motivation is basically: By merging the type and kind levels, TypeInType means that we no longer need to distinguish types and kinds. That is great for implementing, say, kind coercions because we don't need to duplicate the language of coercions to the kind level any more. (Feel free to substitute your own, better examples.) However, now that this RuntimeRep story has emerged, it seems we could get the best of both worlds, by defining * = TYPE L, and Kind = TYPE T. Now we can abstract over the difference between types and kinds when we want to, by working with TYPE t. Or we can distinguish between types and kinds when that makes sense, by using * and Kind.

I don't have any great examples for the latter. Maybe if you define a type family whose result is intended to be a kind (since you use it to classify a type elsewhere) you would want to be able to enforce that on clients who may define their own instances. Or maybe the typing rule for a coercion should be that the type s ~ t of coercions is well-formed only if s :: TYPE r and t :: TYPE r for the same r, and you don't want to allow coercing between values and types. (But see the end of this comment.)

Note that one could perhaps retain even more of the type/kind/sort/etc. hierarchy by adding a parameter to T. The parameter r would contain information about the representation of the "values" (types) classified by types of kind TYPE (T r). Or in symbols,

    if     C :: K = TYPE r, (i.e., the type C has representation r)
    then   K :: TYPE (T r),

or in short TYPE r :: TYPE (T r). I'm not sure how this would interact with type constructors though (with kinds built from (->)). This probably has something to do with the indexed TypeRep story also, which I haven't been paying any attention to.

These suggestions apply to an unspecified extension of Haskell that might want to treat the type level in an arbitrary way. If there's a specific plan for "GHC Haskell" to identify types with their TypeReps as mentioned in ticket:11471#comment:115773 (I guess this means there is some way to refer to a type at the value level, so now it really makes sense to write functions of type * -> *, etc.) then there is probably not much reason to take this route, indeed.

And also, I thought of this: what type would Bool have? It surely must have type *. But then would it not work as a kind anymore? So perhaps this isn't really such a good idea. In any case, I don't believe there is any serious consideration of implementing Reid's plan... just musing about alternatives.

As the differential states, there are still some performance issues to be worked out.

Trac metadata

Trac field	Value
Differential revisions	- → D1891

mentioned in commit d8c64e86

Terrific. So what happens with the examples in ticket:11471#comment:114453 and ticket:11471#comment:114454? Can we add tests for them?

Also does this fix #11473 (closed)? Can we add a test for that?

Ben, might you do these things?

Sure.

assigned to @bgamari and unassigned @rae

assigned to @rae and unassigned @bgamari

I'm still on this, actually. The RuntimeRep stuff was just a necessary stop along the way. The actual fix should be quite simple to put in on top of this all.

Ben, if you want to add tests, I won't stop you, but I don't imagine they will pass.

The RuntimeRep rework has been merged to ghc-8.0.

mentioned in commit f602f4a6

mentioned in commit 5d98b8bf

In the end, there wasn't much to do here other than the RuntimeRep stuff. Still worth merging that last commit, but it's not all that important.

Trac metadata

Trac field	Value
Test case	- → dependent/should_fail/T11471

added 1 deleted label

Merged #11471 (closed) as 6247d27f. Merged #11471 (closed) as 496c210b.

closed

changed milestone to %8.0.1

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

I'm a bit confused as to how unboxed tuples fit into this scheme. I bring this up since this now crashes on GHC HEAD:

{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UnboxedTuples #-}
module Main where

import Data.Typeable
import GHC.Exts

main :: IO ()
main = print $ typeOf (Proxy :: Proxy (# Int, Int #))

$ /opt/ghc/head/bin/ghc -O2 -fforce-recomp Example.hs
[1 of 1] Compiling Main             ( Example.hs, Example.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.1.20160317 for x86_64-unknown-linux):
        tyConRep (#,#)

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

(Previously, this was rejected with an error message, since you couldn't put an unlifted type as the argument of Proxy.)

I notice that there's a single constructor of RuntimeRep for unboxed tuples (UnboxedTupleRep). Does this mean something like this should be allowed?

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
module Example where

import Data.Typeable
import GHC.Exts

data Wat (a :: TYPE 'UnboxedTupleRep) = Wat a

Currently, that fails to compile due to a separate GHC panic:

$ /opt/ghc/head/bin/ghc -O2 -fforce-recomp Example.hs
[1 of 1] Compiling Example          ( Example.hs, Example.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.1.20160317 for x86_64-unknown-linux):
        unboxed tuple PrimRep

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

But wouldn't this be dangerous anyway? After all, unboxed tuples are supposed to represent arguments on the stack, so couldn't unboxed tuple polymorphic potentially lead to the RTS miscalculating how much data to read? Or am I misreading this?

ticket:11471#comment:117929 introduces two new, mostly-unrelated bugs. I've spun them off into #11722 (closed) and #11723 (closed).

mentioned in commit dc62a222

mentioned in issue #12369 (closed)

added Ttask TypeInType labels

added Pnormal label

Trac field	Value
Version	7.10.3
Type	Task
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

Kind polymorphism and unboxed types: bad things are happening

Child items 0

Activity