#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