[GHC] #16310: Program fails with "Impossible case alternative" when optimized
GHC
ghc-devs at haskell.org
Tue Feb 12 19:10:15 UTC 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
More information about the ghc-tickets
mailing list