GHC 8.6.1 regression (buildKindCoercion)

The following program typechecks on GHC 8.4.1, but panics on GHC 8.6.1 and HEAD:

{-# 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

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	highest
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture