Opened 15 months ago

Closed 14 months ago

Last modified 10 months ago

#11471 closed bug (fixed)

Kind polymorphism and unboxed types: bad things are happening

Reported by: bgamari Owned by: goldfire
Priority: normal Milestone: 8.0.1
Component: Compiler (Type checker) Version: 7.10.3
Keywords: TypeInType, LevityPolymorphism Cc: ekmett
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: dependent/should_fail/T11471
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D1891
Wiki Page:

Description

This Note, found in TyCoRep, needs to be updated to reflect TypeInType. It should not reference OpenKind.

Change History (30)

comment:1 Changed 15 months ago by simonpj

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 comment:19, first bullet, and #11465.

I'm really not sure what to do here.

comment:2 Changed 15 months ago by simonpj

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.

comment:3 Changed 15 months ago by simonpj

Summary: Note [The kind invariant] in TyCoRep needs to be updatedKind polymorphism and unboxed types: bad things are happening

comment:4 Changed 15 months ago by bgamari

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

Last edited 15 months ago by bgamari (previous) (diff)

comment:5 in reply to:  4 Changed 15 months ago by simonpj

Keywords: LevityPolymorphism added
Type: taskbug

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

comment:6 Changed 15 months ago by goldfire

Re comment:2: 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.

comment:7 Changed 15 months ago by simonpj

Owner: set to goldfire

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

comment:8 Changed 15 months ago by goldfire

We have a Levity wiki page: NoSubKinds

It needs an update.

comment:9 Changed 15 months ago by rwbarton

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

comment:10 Changed 15 months ago by goldfire

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.

comment:11 Changed 15 months ago by simonpj

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

comment:12 Changed 15 months ago by bgamari

For the record, the current plan (implemented in Phab: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 comment:9. 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.

Last edited 15 months ago by bgamari (previous) (diff)

comment:13 Changed 15 months ago by rwbarton

So under comment:7 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 comment:10 (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.

comment:14 Changed 15 months ago by goldfire

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.

comment:15 Changed 15 months ago by goldfire

Differential Rev(s): Phab:D1891

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

comment:16 Changed 15 months ago by ekmett

Cc: ekmett added

comment:17 Changed 14 months ago by Richard Eisenberg <eir@…>

In d8c64e86/ghc:

Address #11471 by putting RuntimeRep in kinds.

See Note [TYPE] in TysPrim. There are still some outstanding
pieces in #11471 though, so this doesn't actually nail the bug.

This commit also contains a few performance improvements:

* Short-cut equality checking of nullary type syns

* Compare types before kinds in eqType

* INLINE coreViewOneStarKind

* Store tycon binders separately from kinds.

This resulted in a ~10% performance improvement in compiling
the Cabal package. No change in functionality other than
performance. (This affects the interface file format, though.)

This commit updates the haddock submodule.

comment:18 Changed 14 months ago by simonpj

Terrific. So what happens with the examples in comment:1 and comment:2? Can we add tests for them?

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

Ben, might you do these things?

comment:19 Changed 14 months ago by bgamari

Sure.

comment:20 Changed 14 months ago by bgamari

Owner: changed from goldfire to bgamari

comment:21 Changed 14 months ago by goldfire

Owner: changed from bgamari to goldfire

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.

comment:22 Changed 14 months ago by bgamari

The RuntimeRep rework has been merged to ghc-8.0.

comment:23 Changed 14 months ago by Richard Eisenberg <eir@…>

In f602f4a6/ghc:

Fix printing of "kind" vs. "type"

This is as reported in #11471, though it's not the focus of that
ticket.

test case: polykinds/KindVType

comment:24 Changed 14 months ago by Richard Eisenberg <eir@…>

In 5d98b8bf/ghc:

Clean up some pretty-printing in errors.

It turns out that there were some pretty egregious mistakes
in the code that suggested -fprint-explicit-kinds, which are
fixed. This commit also reorders a bunch of error messages,
which I think is an improvement.

This also adds the test case for #11471, which is what
triggered the cleanup in TcErrors. Now that #11473 is done,
there is nothing more outstanding for #11471.

test case: dependent/should_fail/T11471

comment:25 Changed 14 months ago by goldfire

Status: newmerge
Test Case: dependent/should_fail/T11471

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.

comment:27 Changed 14 months ago by bgamari

Milestone: 8.0.1
Resolution: fixed
Status: mergeclosed

comment:28 Changed 14 months ago by RyanGlScott

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?

comment:29 Changed 14 months ago by goldfire

comment:28 introduces two new, mostly-unrelated bugs. I've spun them off into #11722 and #11723.

comment:30 Changed 10 months ago by Simon Peyton Jones <simonpj@…>

In dc62a22/ghc:

Wibble error message for #11471

I'm not quite sure why this changed with my two recent commits,
but it /has/ changed (in a benign way) so I'm accepting it.
Maybe it wasn't me anyway... but life is short and I'm not inclined
to dig further.
Note: See TracTickets for help on using tickets.