Opened 3 months ago

Last modified 3 days ago

#13929 new bug

GHC panic with levity polymorphism

Reported by: vagarenko Owned by:
Priority: high Milestone: 8.2.2
Component: Compiler Version: 8.2.1-rc2
Keywords: TypeInType, LevityPolymorphism Cc: goldfire, Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (18)

comment:1 Changed 3 months ago by bgamari

Cc: goldfire added

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

comment:2 Changed 3 months ago by Iceland_jack

Cc: Iceland_jack added

Fun example

comment:3 Changed 3 months ago by bgamari

Keywords: TypeInType added

comment:4 Changed 3 months ago by bgamari

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

comment:5 Changed 3 months ago by bgamari

Keywords: LevityPolymorphism added

comment:6 Changed 3 months ago by RyanGlScott

Architecture: x86_64 (amd64)Unknown/Multiple
Operating System: WindowsUnknown/Multiple

comment:7 Changed 3 months ago by 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.

comment:8 in reply to:  7 Changed 3 months ago by vagarenko

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

comment:9 Changed 2 months ago by bgamari

Milestone: 8.2.18.2.2

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

comment:10 Changed 9 days ago by Ben Gamari <ben@…>

In fa626f3/ghc:

Fix #13929 by adding another levity polymorphism check

test case: typecheck/should_fail/T13929

comment:11 in reply to:  10 Changed 9 days ago by vagarenko

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

comment:12 Changed 9 days ago by 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?

comment:13 in reply to:  12 Changed 9 days ago by vagarenko

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

comment:14 Changed 8 days ago by bgamari

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.

comment:15 Changed 7 days ago by goldfire

Great explanation in comment:14. Yes, my comment:12 is wrong.

comment:16 in reply to:  10 Changed 5 days ago by vagarenko

Replying to bgamari:

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

Replying to Ben Gamari <ben@…>:

In fa626f3/ghc:

Fix #13929 by adding another levity polymorphism check

test case: typecheck/should_fail/T13929

Have you tested that patch with unboxed sums? See my comment:8

comment:17 Changed 4 days ago by bgamari

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

Last edited 4 days ago by bgamari (previous) (diff)

comment:18 Changed 3 days ago by Ben Gamari <ben@…>

In d86b237d/ghc:

testsuite: Add unboxed sum to T13929

Test Plan: Validate

Reviewers: austin

Subscribers: rwbarton, thomie

GHC Trac Issues: #13929

Differential Revision: https://phabricator.haskell.org/D3993
Note: See TracTickets for help on using tickets.