Re: [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
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Runtime crash     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I managed to trim this down considerably:

 {{{#!hs
 {-# 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 | Refl <- Refl @FSym
                  `apply` funExt @Type @Type @T1Sym @T2Sym
                                 (const Refl)
      = pure ()
 }}}
 {{{
 $ /opt/ghc/8.6.3/bin/ghc -O0 -fforce-recomp Bug.hs
 [1 of 1] Compiling Main             ( Bug.hs, Bug.o )
 Linking Bug ...
 $ ./Bug

 $ /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
 }}}

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