Opened 7 months ago

Closed 7 months ago

Last modified 7 months ago

#16310 closed bug (wontfix)

Program fails with "Impossible case alternative" when optimized

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.3
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Runtime crash Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Here's an (unfortunately rather large) program:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Main (main) where

import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..))
import Unsafe.Coerce (unsafeCoerce)

main :: IO ()
main = print $ traversableComposition @(M1 U1) @() @() @() @U1 @U1
                                      sPureFun sPureFun (SM1 SU1)

-----

sPureFun :: forall f a. SApplicative f => Sing (PureSym0 :: a ~> f a)
sPureFun = singFun1 @PureSym0 sPure

data family Sing (a :: k)
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b

data (.@#@$$$) :: forall a b c. (b ~> c) -> (a ~> b) -> a ~> c
type instance Apply (f .@#@$$$ g) x = Apply f (Apply g x)

newtype instance Sing (f :: k1 ~> k2) =
  SLambda (forall t. Sing t -> Sing (Apply f t))

type SingFunction1 f = forall t. Sing t -> Sing (Apply f t)
singFun1 :: forall f. SingFunction1 f -> Sing f
singFun1 f = SLambda f

type SingFunction2 f = forall t. Sing t -> SingFunction1 (Apply f t)
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun2 f = SLambda (\x -> singFun1 (f x))

-----

data U1 p = U1
data instance Sing (z :: U1 p) where
  SU1 :: Sing 'U1

newtype M1 f p = M1 (f p)
data instance Sing (z :: M1 f p) where
  SM1 :: Sing x -> Sing ('M1 x)
data M1Sym0 :: forall k (f :: k -> Type) (p :: k). f p ~> M1 f p
type instance Apply M1Sym0 x = 'M1 x

newtype Compose f g x = Compose (f (g x))
data ComposeSym0 :: forall k1 k2 (f :: k2 -> Type) (g :: k1 -> k2) (x :: k1).
                    f (g x) ~> Compose f g x
type instance Apply ComposeSym0 x = 'Compose x
data instance Sing (z :: Compose f g a) where
  SCompose :: Sing x -> Sing ('Compose x)

instance (PFunctor f, PFunctor g) => PFunctor (Compose f g) where
  type Fmap h ('Compose x) = 'Compose (Fmap (FmapSym1 h) x)
instance (SFunctor f, SFunctor g) => SFunctor (Compose f g) where
  sFmap :: forall a b (h :: a ~> b) (x :: Compose f g a).
           Sing h -> Sing x -> Sing (Fmap h x)
  sFmap sh (SCompose sx) = SCompose (sFmap (singFun1 @(FmapSym1 h) (sFmap sh)) sx)

instance (PApplicative f, PApplicative g) => PApplicative (Compose f g) where
  type Pure x = 'Compose (Pure (Pure x))
  type 'Compose h <*> 'Compose x = 'Compose (Fmap (<*>@#@$) h <*> x)
instance (SApplicative f, SApplicative g) => SApplicative (Compose f g) where
  sPure sx = SCompose (sPure (sPure sx))
  SCompose sh %<*> SCompose sx = SCompose (sFmap (singFun2 @(<*>@#@$) (%<*>)) sh %<*> sx)

instance PFunctor U1 where
  type Fmap _ _ = 'U1
instance SFunctor U1 where
  sFmap _ _ = SU1
instance VFunctor U1 where
  fmapCompose _ _ SU1 = Refl

instance PFunctor f => PFunctor (M1 f) where
  type Fmap g ('M1 x) = 'M1 (Fmap g x)
instance SFunctor f => SFunctor (M1 f) where
  sFmap sg (SM1 sx) = SM1 (sFmap sg sx)
instance VFunctor f => VFunctor (M1 f) where
  fmapCompose sg sh (SM1 x) | Refl <- fmapCompose sg sh x = Refl

instance PApplicative U1 where
  type Pure _ = 'U1
  type _ <*> _ = 'U1
instance SApplicative U1 where
  sPure _ = SU1
  _ %<*> _ = SU1
instance VApplicative U1 where
  applicativeHomomorphism _ _ = Refl
  applicativeFmap _ _ = Refl

instance PTraversable U1 where
  type Traverse _ _ = Pure 'U1
instance STraversable U1 where
  sTraverse _ _ = sPure SU1
instance VTraversable U1 where
  traversableComposition :: forall p q r (f :: Type -> Type) (g :: Type -> Type)
                                   (h :: p ~> f q) (i :: q ~> g r) (x :: U1 p).
                            (VApplicative f, VApplicative g)
                         => Sing h -> Sing i -> Sing x
                         ->     Traverse (ComposeSym0 .@#@$$$ FmapSym1 i .@#@$$$ h) x
                            :~: 'Compose (Fmap (TraverseSym1 i) (Traverse h x))
  traversableComposition _ si _
    | Refl <- applicativeHomomorphism @f sTraverseI sU1q
    , Refl <- applicativeFmap @f sTraverseI (sPure sU1q)
    = Refl
    where
      sTraverseI :: Sing (TraverseSym1 i :: U1 q ~> g (U1 r))
      sTraverseI = singFun1 (sTraverse si)

      sU1q :: Sing ('U1 :: U1 q)
      sU1q = SU1

instance PTraversable f => PTraversable (M1 f) where
  type Traverse g ('M1 x) = Fmap M1Sym0 (Traverse g x)
instance STraversable f => STraversable (M1 f) where
  sTraverse sg (SM1 sx) = sFmap (singFun1 @M1Sym0 SM1) (sTraverse sg sx)
instance VTraversable f => VTraversable (M1 f) where
  traversableComposition :: forall p q r (cf :: Type -> Type) (cg :: Type -> Type)
                                   (h :: p ~> cf q) (i :: q ~> cg r) (x :: M1 f p).
                            (VApplicative cf, VApplicative cg)
                         => Sing h -> Sing i -> Sing x
                         ->     Traverse (ComposeSym0 .@#@$$$ FmapSym1 i .@#@$$$ h) x
                            :~: 'Compose (Fmap (TraverseSym1 i) (Traverse h x))
  traversableComposition sh si (SM1 (sfp :: Sing fp))
    | Refl <- traversableComposition sh si sfp
    , Refl <- fmapCompose @cf (singFun1 @(FmapSym1 M1Sym0) (sFmap sM1Fun))
                              sTraverseIFun sTraverseHIp
    , Refl <- --     Fmap (FmapSym1 M1Sym0 .@#@$$$ TraverseSym1 i) (Traverse h fp)
              -- :~: Fmap (TraverseSym1 i .@#@$$$ M1Sym0) (Traverse h fp)
              Refl @FmapSym0
                `apply` funExt @(f q) @(cg (M1 f r))
                               @(FmapSym1 M1Sym0 .@#@$$$ TraverseSym1 i)
                               @(TraverseSym1 i .@#@$$$ M1Sym0)
                               lemma
                `apply` Refl @(Traverse h fp)
    , Refl <- fmapCompose @cf sTraverseIFun sM1Fun sTraverseHIp
    = Refl
    where
      lemma :: forall (z :: f q). Sing z
            -> Fmap M1Sym0 (Traverse i z) :~: Traverse i (Apply M1Sym0 z)
      lemma _ = Refl

      sM1Fun :: forall z. Sing (M1Sym0 :: f z ~> M1 f z)
      sM1Fun = singFun1 SM1

      sTraverseHIp :: Sing (Traverse h fp)
      sTraverseHIp = sTraverse sh sfp

      sTraverseIFun :: forall hk. STraversable hk
                    => Sing (TraverseSym1 i :: hk q ~> cg (hk r))
      sTraverseIFun = singFun1 (sTraverse si)

-----

class PFunctor (f :: Type -> Type) where
  type Fmap (g :: a ~> b) (x :: f a) :: f b
data FmapSym0 :: forall f a b. (a ~> b) ~> f a ~> f b
data FmapSym1 :: forall f a b. (a ~> b) -> f a ~> f b
type instance Apply  FmapSym0 f    = FmapSym1 f
type instance Apply (FmapSym1 f) x = Fmap f x
class SFunctor (f :: Type -> Type) where
  sFmap :: forall a b (g :: a ~> b) (x :: f a).
           Sing g -> Sing x -> Sing (Fmap g x)
class (PFunctor f, SFunctor f) => VFunctor f where
  fmapCompose :: forall a b c (g :: b ~> c) (h :: a ~> b) (x :: f a).
                 Sing g -> Sing h -> Sing x
              -> Fmap g (Fmap h x) :~: Fmap (g .@#@$$$ h) x

class PFunctor f => PApplicative f where
  type Pure (x :: a) :: f a
  type (g :: f (a ~> b)) <*> (x :: f a) :: f b
infixl 4 <*>
data PureSym0 :: forall (f :: Type -> Type) a. a ~> f a
type instance Apply PureSym0 x = Pure x
data (<*>@#@$)  :: forall (f :: Type -> Type) a b. f (a ~> b) ~> f a ~> f b
data (<*>@#@$$) :: forall (f :: Type -> Type) a b. f (a ~> b) -> f a ~> f b
type instance Apply  (<*>@#@$)  f    = (<*>@#@$$) f
type instance Apply ((<*>@#@$$) f) x = f <*> x
class SFunctor f => SApplicative f where
  sPure :: forall a (x :: a).
           Sing x -> Sing (Pure x :: f a)

  (%<*>) :: forall a b (g :: f (a ~> b)) (x :: f a).
            Sing g -> Sing x -> Sing (g <*> x)
class (PApplicative f, SApplicative f, VFunctor f) => VApplicative f where
  applicativeHomomorphism :: forall a b (g :: a ~> b) (x :: a).
                             Sing g -> Sing x
                          -> (Pure g <*> Pure x) :~: (Pure (g `Apply` x) :: f b)
  applicativeFmap :: forall a b (g :: a ~> b) (x :: f a).
                     Sing g -> Sing x
                  -> Fmap g x :~: (Pure g <*> x)

class PFunctor t => PTraversable t where
  type Traverse (g :: a ~> f b) (x :: t a) :: f (t b)
data TraverseSym1 :: forall t f a b. (a ~> f b) -> t a ~> f (t b)
type instance Apply (TraverseSym1 f) x = Traverse f x
class SFunctor t => STraversable t where
  sTraverse :: forall f a b (g :: a ~> f b) (x :: t a).
               SApplicative f
            => Sing g -> Sing x -> Sing (Traverse g x)
class (PTraversable t, STraversable t, VFunctor t) => VTraversable t where
  traversableComposition :: forall a b c (f :: Type -> Type) (g :: Type -> Type)
                                   (h :: a ~> f b) (i :: b ~> g c) (x :: t a).
                            (VApplicative f, VApplicative g)
                         => Sing h -> Sing i -> Sing x
                         ->     Traverse (ComposeSym0 .@#@$$$ FmapSym1 i .@#@$$$ h) x
                            :~: 'Compose (Fmap (TraverseSym1 i) (Traverse h x))

-----

funExt :: forall a b (f :: a ~> b) (g :: a ~> b).
          (forall (x :: a). Sing x
                         -> Apply f x :~: Apply g x)
       -> f :~: g
funExt _ = axiom

apply :: f :~: g -> a :~: b -> Apply f a :~: Apply g b
apply Refl Refl = Refl

axiom :: a :~: b
axiom = unsafeCoerce Refl

When compiled without optimization, this program prints "Refl", as you would expect:

$ /opt/ghc/8.6.3/bin/ghc -O0 Bug.hs -fforce-recomp
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )
Linking Bug ...
$ ./Bug 
Refl

However, when compiled with optimizations, it starts failing at runtime!

$ /opt/ghc/8.6.3/bin/ghc -O Bug.hs -fforce-recomp
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )
Linking Bug ...

$ ./Bug 
Bug: Impossible case alternative

This behavior can be observed on all versions of GHC from 8.2.2 to HEAD.

Interestingly, this program passes -dcore-lint on GHC 8.4.4 through HEAD, but on GHC 8.2.2, it fails -dcore-lint:

$ /opt/ghc/8.6.3/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )
Linking Bug ...

$ /opt/ghc/8.2.2/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
    In a case alternative: (Refl cobox_a1UV :: (FmapSym0 :: (TyFun
                                                               (f1_X2dk b_a2aC
                                                                ~> g_a2aF (M1 f1_X2dk c_a2aD))
                                                               (f_a2aE (f1_X2dk b_a2aC)
                                                                ~> f_a2aE (g_a2aF (M1
                                                                                     f1_X2dk
                                                                                     c_a2aD)))
                                                             -> *))
                                               ~#
                                               (FmapSym0 :: (TyFun
                                                               (f1_X2dk b_a2aC
                                                                ~> g_a2aF (M1 f1_X2dk c_a2aD))
                                                               (f_a2aE (f1_X2dk b_a2aC)
                                                                ~> f_a2aE (g_a2aF (M1
                                                                                     f1_X2dk
                                                                                     c_a2aD)))
                                                             -> *)))
    No alternatives for a case scrutinee in head-normal form: ($WRefl
                                                                 @ Any @ Any)
                                                              `cast` (((:~:)
                                                                         (UnsafeCo nominal Any (f b
                                                                                                ~> g (M1
                                                                                                        f
                                                                                                        c)))
                                                                         (UnsafeCo nominal Any (FmapSym1
                                                                                                  M1Sym0
                                                                                                .@#@$$$ TraverseSym1
                                                                                                          i))
                                                                         (UnsafeCo nominal Any (TraverseSym1
                                                                                                  i
                                                                                                .@#@$$$ M1Sym0)))_R
                                                                      :: ((Any :~: Any) :: *)
                                                                         ~R#
                                                                         (((FmapSym1 M1Sym0
                                                                            .@#@$$$ TraverseSym1
                                                                                      i_a2aH)
                                                                           :~: (TraverseSym1 i_a2aH
                                                                                .@#@$$$ M1Sym0)) :: *))

(The full Core Lint error is absolutely enormous, so I'll post it as a separate attachment.)

The one thing about this program that might be considered strange is the use of axiom = unsafeCoerce Refl. I believe this should be a perfectly safe use of unsafeCoerce, but nevertheless, there is always the possibility that GHC is doing something unsightly when optimizing it. As one curiosity, if you mark axiom as NOINLINE, then the program produces a different result:

$ /opt/ghc/8.6.3/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )
Linking Bug ...

$ ./Bug 

The program simply prints a newline, for some odd reason. (It doesn't appear to throw an exception either, since echo $? yields 0.)

Attachments (1)

ghc-8.2.2.dump-core-lint (165.4 KB) - added by RyanGlScott 7 months ago.
Result of running /opt/ghc/8.2.2/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint

Download all attachments as: .zip

Change History (8)

Changed 7 months ago by RyanGlScott

Attachment: ghc-8.2.2.dump-core-lint added

Result of running /opt/ghc/8.2.2/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint

comment:1 Changed 7 months ago by RyanGlScott

Upon further searching, the most likely reason why this fails Core Lint in GHC 8.2.2 but not in later versions is due to commit 6b52b4c832f888f7741a4ba0fec1fdac10244f6d, which removed the very Core Lint check that fires in 8.2.

comment:2 Changed 7 months ago by RyanGlScott

I managed to trim this down considerably:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Main (main) where

import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..))
import Unsafe.Coerce (unsafeCoerce)

data family Sing :: k -> Type
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b

funExt :: forall a b (f :: a ~> b) (g :: a ~> b).
          (forall (x :: a). Sing x
                         -> Apply f x :~: Apply g x)
       -> f :~: g
funExt _ = axiom

apply :: f :~: g -> a :~: b -> Apply f a :~: Apply g b
apply Refl Refl = Refl

axiom :: forall a b. a :~: b
axiom = unsafeCoerce (Refl @a)

type family F (a :: Type ~> Type)
data FSym :: (Type ~> Type) ~> Type
type instance Apply FSym a = F a

data T1Sym :: Type ~> Type
data T2Sym :: Type ~> Type
type instance Apply T1Sym a = a
type instance Apply T2Sym a = a

main :: IO ()
main = print (Refl @FSym `apply` funExt @Type @Type @T1Sym @T2Sym (const Refl))
$ /opt/ghc/8.6.3/bin/ghc -O0 -fforce-recomp Bug.hs
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )
Linking Bug ...
$ ./Bug
Refl

$ /opt/ghc/8.6.3/bin/ghc -O -fforce-recomp Bug.hs
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )
Linking Bug ...
$ ./Bug 
Bug: Impossible case alternative
Last edited 7 months ago by RyanGlScott (previous) (diff)

comment:3 Changed 7 months ago by RyanGlScott

Marking apply as NOINLINE works around the issue.

comment:4 Changed 7 months ago by RyanGlScott

Resolution: wontfix
Status: newclosed

After some thought, I've come to the conclusion that this isn't a bug. Here is what is happening. GHC scrutinizes a $WRefl of type T1Sym :~: T2Sym. GHC, in its infinite wisdom, recognizes that T1Sym and T2Sym are distinct data types, and therefore cannot possibly be equal. Therefore, SimplUtils.mkCase transforms this into case ($WRefl :: T1Sym :~: T2Sym) of {}, since the Refl case is "unreachable". However, due to our crafty use of unsafeCoerce, we do actually enter this case, and disaster strikes.

I've come to the conclusion that axiom, much like unsafePerformIO, requires careful use of NOINLINE in order to use in a safe fashion. The fact that apply must be marked as NOINLINE reflects this reality.

comment:5 Changed 7 months ago by simonpj

unsafeCoerce is certainly dangerous, as its name suggests! Here axiom seems to claim that for all types a and b, the two are equal. That might lead to a seg-faolt; here it leads to "unreachable" code being reached.

Or is there more to it than that?

comment:6 Changed 7 months ago by goldfire

Well, axiom is being used to prove functional extensionality, which is generally safe. But perhaps it would be better to put the use of unsafeCoerce in funExt directly. I wonder if that quells the problem.

comment:7 in reply to:  6 Changed 7 months ago by RyanGlScott

Replying to goldfire:

But perhaps it would be better to put the use of unsafeCoerce in funExt directly. I wonder if that quells the problem.

Alas, defining funExt _ = unsafeCoerce (Refl @f) does no good—it still produces Impossible case alternative when ran.

Note: See TracTickets for help on using tickets.