[GHC] #13910: Inlining a definition causes GHC to panic (repSplitTyConApp_maybe)

1 Jul 2017


      #13910: Inlining a definition causes GHC to panic (repSplitTyConApp_maybe)
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1-rc2
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #13877
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Here is a program which I believe //should// typecheck:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

 import Data.Kind
 import Data.Type.Equality

 data family Sing (a :: k)

 class SingKind k where
   type Demote k = (r :: *) | r -> k
   fromSing :: Sing (a :: k) -> Demote k
   toSing   :: Demote k -> SomeSing k

 data SomeSing k where
   SomeSing :: Sing (a :: k) -> SomeSing k

 withSomeSing :: forall k r
               . SingKind k
              => Demote k
              -> (forall (a :: k). Sing a -> r)
              -> r
 withSomeSing x f =
   case toSing x of
     SomeSing x' -> f x'

 data TyFun :: * -> * -> *
 type a ~> b = TyFun a b -> *
 infixr 0 ~>

 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
 type a @@ b = Apply a b
 infixl 9 @@

 data FunArrow = (:->) | (:~>)

 class FunType (arr :: FunArrow) where
   type Fun (k1 :: Type) arr (k2 :: Type) :: Type

 class FunType arr => AppType (arr :: FunArrow) where
   type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2

 type FunApp arr = (FunType arr, AppType arr)

 instance FunType (:->) where
   type Fun k1 (:->) k2 = k1 -> k2

 $(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter

 instance AppType (:->) where
   type App k1 (:->) k2 (f :: k1 -> k2) x = f x

 instance FunType (:~>) where
   type Fun k1 (:~>) k2 = k1 ~> k2

 $(return [])

 instance AppType (:~>) where
   type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x

 infixr 0 -?>
 type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2

 data instance Sing (z :: a :~: b) where
   SRefl :: Sing Refl

 instance SingKind (a :~: b) where
   type Demote (a :~: b) = a :~: b
   fromSing SRefl = Refl
   toSing Refl = SomeSing SRefl

 (~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p ::
 forall (y :: k). a :~: y ~> Type).
            Sing r
         -> p @@ Refl
         -> p @@ r
 (~>:~:) SRefl pRefl = pRefl

 type WhyReplacePoly (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
                     (y :: t) (e :: from :~: y) = App t arr Type p y
 data WhyReplacePolySym (arr :: FunArrow) (from :: t) (p :: (t -?> Type)
 arr)
   :: forall (y :: t). from :~: y ~> Type
 type instance Apply (WhyReplacePolySym arr from p :: from :~: y ~> Type) x
   = WhyReplacePoly arr from p y x

 replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t -> Type).
            p from
         -> from :~: to
         -> p to
 replace = replacePoly @(:->)

 replaceTyFun :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).
                 p @@ from
              -> from :~: to
              -> p @@ to
 replaceTyFun = replacePoly @(:~>) @_ @_ @_ @p

 replacePoly :: forall (arr :: FunArrow) (t :: Type) (from :: t) (to :: t)
                       (p :: (t -?> Type) arr).
                FunApp arr
             => App t arr Type p from
             -> from :~: to
             -> App t arr Type p to
 replacePoly from eq =
   withSomeSing eq $ \(singEq :: Sing r) ->
     (~>:~:) @t @from @to @r @(WhyReplacePolySym arr from p) singEq from

 type WhyLeibnizPoly (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) (z
 :: t)
   = App t arr Type f a -> App t arr Type f z
 data WhyLeibnizPolySym (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t)
   :: t ~> Type
 type instance Apply (WhyLeibnizPolySym arr f a) z = WhyLeibnizPoly arr f a
 z

 leibnizPoly :: forall (arr :: FunArrow) (t :: Type) (f :: (t -?> Type)
 arr)
                       (a :: t) (b :: t).
                FunApp arr
             => a :~: b
             -> App t arr Type f a
             -> App t arr Type f b
 leibnizPoly = replaceTyFun @t @a @b @(WhyLeibnizPolySym arr f a) id

 leibniz :: forall (t :: Type) (f :: t -> Type) (a :: t) (b :: t).
            a :~: b
         -> f a
         -> f b
 leibniz = replaceTyFun @t @a @b @(WhyLeibnizPolySym (:->) f a) id
 -- The line above is what you get if you inline the definition of
 leibnizPoly.
 -- It causes a panic, however.
 --
 -- An equivalent implementation is commented out below, which does *not*
 -- cause GHC to panic.
 --
 -- leibniz = leibnizPoly @(:->)

 leibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).
                 a :~: b
              -> f @@ a
              -> f @@ b
 leibnizTyFun = leibnizPoly @(:~>) @_ @f
 }}}

 GHC 8.2.1 and HEAD panic on the definition of `leibniz`, however:

 {{{
 $ /opt/ghc/8.2.1/bin/ghci Bug.hs
 GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )
 ghc: panic! (the 'impossible' happened)
   (GHC version 8.2.0.20170623 for x86_64-unknown-linux):
         repSplitTyConApp_maybe
   (f_a5vT[sk:2] |> Sym (Trans
                             (Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N))
                             (D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2]
   (f_a5vT[sk:2] |> Sym (Trans
                             (Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N))
                             (D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2]
   k2_a5l0
   Call stack:
       CallStack (from HasCallStack):
         prettyCurrentCallStack, called at
 compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
         callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in
 ghc:Outputable
         pprPanic, called at compiler/types/Type.hs:1122:5 in ghc:Type

 Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
 }}}

 Interestingly, GHC 8.0.1 and 8.0.2 do not give the same panic—they give
 the panic from #13877:

 {{{
 $ /opt/ghc/8.0.2/bin/ghci Bug.hs
 GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:134:64: error:ghc: panic! (the 'impossible' happened)
   (GHC version 8.0.2 for x86_64-unknown-linux):
         No skolem info: k2_a4KV

 Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
 }}}

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13910
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler