#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)
Change History (8)
Changed 7 months ago by
Attachment: | ghc-8.2.2.dump-core-lint added |
---|
comment:1 Changed 7 months ago by
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
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
comment:4 Changed 7 months ago by
Resolution: | → wontfix |
---|---|
Status: | new → closed |
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
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 follow-up: 7 Changed 7 months ago by
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 Changed 7 months ago by
Replying to goldfire:
But perhaps it would be better to put the use of
unsafeCoerce
infunExt
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.
Result of running
/opt/ghc/8.2.2/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint