GHC panic with levity polymorphism

I'm using GHC version 8.2.0.20170507

This code fails to compile

{-# LANGUAGE MagicHash #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

module Main where

import GHC.Exts
import Data.Kind
import GHC.Generics

class GUnbox (f :: Type -> Type) (r :: RuntimeRep) where
    type GUnboxed f r :: TYPE r
    gunbox :: f p -> GUnboxed f r

instance (GUnbox f rf, GUnbox g rg) => GUnbox (f :*: g) ('TupleRep '[rf, rg]) where
    type GUnboxed (f :*: g) ('TupleRep '[rf, rg]) = (# GUnboxed f rf, GUnboxed g rg #)
    -- if I remove implementation of `gunbox` it compiles successfully
    gunbox (x :*: y) = (# gunbox x, gunbox y #)

main :: IO ()
main = pure ()

with message:

[1 of 1] Compiling Main             ( Main.hs, .stack-work\dist\f42fcbca\build\Main.o )
ghc.EXE: panic! (the 'impossible' happened)
  (GHC version 8.2.0.20170507 for x86_64-unknown-mingw32):
        isUnliftedType
  GUnboxed g_a21y rg_a21z :: TYPE rg_a21z
  Call stack:
      CallStack (from HasCallStack):
        prettyCurrentCallStack, called at compiler\utils\Outputable.hs:1134:58 in ghc:Outputable
        callStackDoc, called at compiler\utils\Outputable.hs:1138:37 in ghc:Outputable
        pprPanic, called at compiler\types\Type.hs:1954:10 in ghc:Type

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

Trac metadata

Trac field	Value
Version	8.2.1-rc2
Type	Bug
TypeOfFailure	OtherFailure
Priority	high
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system	Windows
Architecture	x86_64 (amd64)

changed milestone to %8.2.1

changed weight to 7

added Tbug Trac import labels

Thanks for the bug report and nice reproducer! Adding goldfire to CC.

Fun example

added TypeInType label

For the record, a more complete callstack is,

ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.2.0.20170704 for x86_64-unknown-linux):
	isUnliftedType
  GUnboxed g_a20x rg_a20y :: TYPE rg_a20y
  Call stack:
      CallStack (from HasCallStack):
        prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
        callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
        pprPanic, called at compiler/types/Type.hs:1954:10 in ghc:Type
        isUnliftedType, called at compiler/coreSyn/CoreUtils.hs:487:27 in ghc:CoreUtils
        needsCaseBinding, called at compiler/coreSyn/MkCore.hs:162:10 in ghc:MkCore
        mk_val_app, called at compiler/coreSyn/MkCore.hs:146:42 in ghc:MkCore
        mkCoreApps, called at compiler/coreSyn/MkCore.hs:154:26 in ghc:MkCore
        mkCoreConApps, called at compiler/coreSyn/MkCore.hs:364:5 in ghc:MkCore
        mkCoreUbxTup, called at compiler/coreSyn/MkCore.hs:370:32 in ghc:MkCore
        mkCoreTupBoxity, called at compiler/deSugar/DsExpr.hs:382:19 in ghc:DsExpr

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

removed TypeInType label

Trac metadata

Trac field	Value
Operating system	Windows → Unknown/Multiple
Architecture	x86_64 (amd64) → Unknown/Multiple

To be clear, I don't think (although could be wrong) this program should compile; afterall, the type of gunbox requires that we represent a levity polymorphic result, which we cannot do. Hence, the real bug here is the panic instead of a proper type error.

Replying to [ticket:13929#comment:138906 bgamari]:

To be clear, I don't think (although could be wrong) this program should compile; afterall, the type of gunbox requires that we represent a levity polymorphic result, which we cannot do. Hence, the real bug here is the panic instead of a proper type error.

I think levity polymorphism paper says you can't have functions with levity-polymorphic parameters, levity-polymorphic results are OK.

This compiles fine:

instance (GUnbox f r) => GUnbox (M1 i t f) r where
    type GUnboxed (M1 i t f) r = GUnboxed f r
    gunbox (M1 x) = gunbox x

But unboxed sum also fails to compile:

instance (GUnbox f rf, GUnbox g rg) => GUnbox (f :+: g) ('SumRep '[rf, rg]) where
    type GUnboxed (f :+: g) ('SumRep '[rf, rg]) = (# GUnboxed f rf | GUnboxed g rg #)
    gunbox (L1 l) = (# gunbox l | #)
    gunbox (R1 r) = (# | gunbox r #)

with the same message.

changed milestone to %8.2.2

I'm afraid this won't be fixed for 8.2.1.

mentioned in commit fa626f3b

Replying to [#13929 (closed) Ben Gamari <ben@…>]:

Can you please elaborate why you think GHC should reject this. This error message doesn't say much

T13929.hs:29:27: error:
    A levity-polymorphic type is not allowed here:
      Type: GUnboxed f rf
      Kind: TYPE rf
    In the type of expression: gunbox x

T13929.hs:29:37: error:
    A levity-polymorphic type is not allowed here:
      Type: GUnboxed g rg
      Kind: TYPE rg
    In the type of expression: gunbox y

As I mentioned in comment 8:

To be clear, I don't think (although could be wrong) this program should compile; afterall, the type of gunbox requires that we represent a levity polymorphic result, which we cannot do. Hence, the real bug here is the panic instead of a proper type error.

I think levity polymorphism paper says you can't have functions with levity-polymorphic parameters, levity-polymorphic results are OK.

It looks to me that the runtime representation of x and y can't be known at compile time -- these arguments are levity-polymorphic, which is problematic. Do you see otherwise?

Replying to [ticket:13929#comment:142406 goldfire]:

It looks to me that the runtime representation of x and y can't be known at compile time -- these arguments are levity-polymorphic, which is problematic. Do you see otherwise?

x, y :: f p where f :: Type -> Type and p :: Type so they are always lifted, right?

The problem is the result type of gunbox x. Namely, we have

class GUnbox (f :: Type -> Type) (r :: RuntimeRep) where
    type GUnboxed f r :: TYPE r
    gunbox :: f p -> GUnboxed f r

and

f :: Type -> Type
p :: Type
x :: f p

therefore

gunbox x :: GUnboxed f rf

Which is levity polymorphic. My understanding is that this wouldn't be the problem if this were at the head of the RHS; however, in this case we need to build an unboxed tuple from it, which is problematic.

In short: returning levity polymorphic things generally isn't a problem. However, the moment we actually need to manipulate such a value we have a problem. I find it helpful to consider why this is from the standpoint of a concrete operational model. You can think of the RuntimeRep of a function's return type as being a description of which machine register(s) the result can be found in. In the case that we have a function like,

($) :: forall (r :: RuntimeRep) (a :: TYPE r) (b :: Type).
       (b -> a) -> b -> a
f $ x = f x

The ($) function never needs to //do// anything with the levity-polymorphic value: it simply sets up the call to f and jumps. In fact, flow of control will never even return to ($) after this jump. Consequently, the code that we generate for ($) can be entirely agnostic to the RuntimeRep that it is used at.

Now let's consider at your function,

gunbox :: (GUnbox f rf, GUnbox g rg)
       => (f :*: g) -> (# GUnboxed f rf, GUnboxed g rg #)
gunbox (x :*: y) = (# gunbox x, gunbox y #)

Specifically, let's consider the case where f ~ Double and g ~ Maybe Int (with instances such that rf ~ DoubleRep and rg ~ LiftedPtrRep). In this case gunbox will need to first evaluate gunbox x, which will save its result in one of the machine's floating point registers. Then it will need to evaluate gunbox y, which will save its result in a pointer register. We can then return, having "constructed" our unboxed tuple. This case was easy as there was no "overlap" between the two registers used to return the result.

However, let's consider another case, where f ~ Double and g ~ Double (therefore rf ~ DoubleRep and rg ~ DoubleRep). In this case gunbox will need to evaluate both gunbox x and gunbox y, but it must take care to move the result of one out of the way before evaluating the other since both will return their result in the same floating point register.

This, of course, means that gunbox would need to behave differently depending upon the RuntimeReps that it was working with. Our code generation strategy does not currently allow for this.

Great explanation in ticket:13929#comment:142435. Yes, my ticket:13929#comment:142406 is wrong.

Replying to [ticket:13929#comment:142435 bgamari]:

Now I see. Thank you for the very thorough explanation!

Replying to [#13929 (closed) Ben Gamari <ben@…>]:

In [changeset:"fa626f3b/ghc" fa626f3b/ghc]: `repository="ghc" revision="fa626f3b" Fix #13929 (closed) by adding another levity polymorphism check

test case: typecheck/should_fail/T13929 `

Have you tested that patch with unboxed sums? See my ticket:13929#comment:138907

Indeed this still fails with the unboxed sum example. Adding a test in D3993.

mentioned in commit d86b237d

assigned to @bgamari

I'll take care of the remaining case.

mentioned in commit 018c40fb

added 1 deleted label

Trac metadata

Trac field	Value
Test case	- → ypecheck/should_fail/T13929

closed

All patches listed above merged to ghc-8.2 as of 78e67391.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	ypecheck/should_fail/T13929 → typecheck/should_fail/T13929

removed 1 deleted label

mentioned in issue #15883 (closed)

added Phigh label