[GHC] #15419: GHC 8.6.1 regression (buildKindCoercion)

19 Jul 2018


      #15419: GHC 8.6.1 regression (buildKindCoercion)
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  highest        |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.5
  (Type checker)                     |
           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:
-------------------------------------+-------------------------------------
 The following program typechecks on GHC 8.4.1, but panics on GHC 8.6.1 and
 HEAD:

 {{{#!hs
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Bug where

 import Data.Kind

 data family Sing :: forall k. k -> Type
 data TyFun :: Type -> Type -> Type
 type a ~> b = TyFun a b -> Type
 infixr 0 ~>
 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

 data instance Sing :: forall a b. (a, b) -> Type where
   STuple2 :: Sing x -> Sing y -> Sing '(x, y)
 newtype instance Sing (f :: k1 ~> k2) =
   SLambda { applySing :: forall t. Sing t -> Sing (f `Apply` t) }

 -----

 newtype Par1 p = Par1 p
 newtype K1 c p = K1 c
 data (f :*: g) p = f p :*: g p

 data instance Sing :: forall p. Par1 p -> Type where
   SPar1 :: Sing x -> Sing ('Par1 x)
 data instance Sing :: forall k c (p :: k). K1 c p -> Type where
   SK1 :: Sing x -> Sing ('K1 x)
 data instance Sing :: forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
                       (f :*: g) p -> Type where
   (:%*:) :: Sing x -> Sing y -> Sing (x ':*: y)

 class Generic1 (f :: k -> Type) where
   type Rep1 f :: k -> Type
   from1 :: f a -> Rep1 f a
   to1 :: Rep1 f a -> f a

 class PGeneric1 (f :: k -> Type) where
   type From1 (z :: f a)      :: Rep1 f a
   type To1   (z :: Rep1 f a) :: f a

 class SGeneric1 (f :: k -> Type) where
   sFrom1 :: forall (a :: k) (z :: f a).      Sing z -> Sing (From1 z)
   sTo1   :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)

 instance Generic1 ((,) a) where
   type Rep1 ((,) a) = K1 a :*: Par1
   from1 (x, y)          = K1 x :*: Par1 y
   to1 (K1 x :*: Par1 y) = (x, y)

 instance PGeneric1 ((,) a) where
   type From1 '(x, y)              = 'K1 x ':*: 'Par1 y
   type To1   ('K1 x ':*: 'Par1 y) = '(x, y)

 instance SGeneric1 ((,) a) where
   sFrom1 (STuple2 x y)        = SK1 x :%*: SPar1 y
   sTo1   (SK1 x :%*: SPar1 y) = STuple2 x y

 -----

 type family GenericFmap (g :: a ~> b) (x :: f a) :: f b where
   GenericFmap g x = To1 (Fmap g (From1 x))

 class PFunctor (f :: Type -> Type) where
   type Fmap (g :: a ~> b) (x :: f a) :: f b
   type Fmap g x = GenericFmap g 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)
   default sFmap :: forall a b (g :: a ~> b) (x :: f a).
                    ( SGeneric1 f, SFunctor (Rep1 f)
                    , Fmap g x ~ GenericFmap g x )
                 => Sing g -> Sing x -> Sing (Fmap g x)
   sFmap sg sx = sTo1 (sFmap sg (sFrom1 sx))

 -----

 instance PFunctor Par1 where
   type Fmap f ('Par1 x) = 'Par1 (f `Apply` x)
 instance PFunctor (K1 c) where
   type Fmap _ ('K1 x) = 'K1 x
 instance PFunctor (f :*: g) where
   type Fmap h (x ':*: y) = Fmap h x ':*: Fmap h y

 instance SFunctor Par1 where
   sFmap sf (SPar1 sx) = SPar1 (sf `applySing` sx)
 instance SFunctor (K1 c) where
   sFmap _ (SK1 sx) = SK1 sx
 instance (SFunctor f, SFunctor g) => SFunctor (f :*: g) where
   sFmap sh (sx :%*: sy) = sFmap sh sx :%*: sFmap sh sy

 -----

 instance PFunctor ((,) a)
 -- The line below causes the panic
 instance SFunctor ((,) a)
 }}}
 {{{
 $ /opt/ghc/8.6.1/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
 ghc: panic! (the 'impossible' happened)
   (GHC version 8.6.0.20180714 for x86_64-unknown-linux):
         buildKindCoercion
   K1 a_a1Nj :*: Par1
   Rep1 ((,) a_a1Nj)
   *
   a_a1Nj
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in
 ghc:Outputable
         pprPanic, called at compiler/types/Coercion.hs:2069:9 in
 ghc:Coercion
 }}}

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

GHC

GHC

GHC

GHC

GHC

GHC

GHC

tags

participants (1)