Re: [GHC] #14174: GHC panic with TypeInType and type family

2 Nov 2017

      #14174: GHC panic with TypeInType and type family
-------------------------------------+-------------------------------------
        Reporter:  dfeuer            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.2.3
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 This might be another occurrence of this bug:

 {{{#!hs
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Bug where

 import Data.Kind

 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

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

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

 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

 type family ElimBool (p :: Bool -> Type)
                      (z :: Bool)
                      (pFalse :: p False)
                      (pTrue  :: p True)
                      :: p z where
   -- Commenting out the line below makes the panic go away
   ElimBool p z pFalse pTrue = ElimBoolPoly (:->) p z pFalse pTrue

 type family ElimBoolTyFun (p :: Bool ~> Type)
                           (z :: Bool)
                           (pFalse :: p @@ False)
                           (pTrue  :: p @@ True)
                           :: p @@ z where
   ElimBoolTyFun p z pFalse pTrue = ElimBoolPoly (:~>) p z pFalse pTrue

 type family ElimBoolPoly (arr :: FunArrow)
                          (p :: (Bool -?> Type) arr)
                          (z :: Bool)
                          (pFalse :: App Bool arr Type p False)
                          (pTrue  :: App Bool arr Type p True)
                          :: App Bool arr Type p z where
   ElimBoolPoly _ _ False pFalse _     = pFalse
   ElimBoolPoly _ _ True  _      pTrue = pTrue
 }}}

 {{{
 $ /opt/ghc/8.2.1/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
 ghc: panic! (the 'impossible' happened)
   (GHC version 8.2.1 for x86_64-unknown-linux):
         piResultTy
   k0_a1Zd[tau:1]
   z_aS3[sk:1]
   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:948:35 in ghc:Type
 }}}

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