[GHC] #16310: Program fails with "Impossible case alternative" when optimized

12 Feb 2019

      #16310: Program fails with "Impossible case alternative" when optimized
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Runtime crash
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Here's an (unfortunately rather large) program:

 {{{#!hs
 {-# 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`.)

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16310
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler