Program fails with "Impossible case alternative" when optimized
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 ReflWhen 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
ReflHowever, 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 alternativeThis 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.)
Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |