[GHC] #15343: Implicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind)

[GHC]

#15343: Implicitly quantifying a kind variable causes GHC 8.6 to panic
(coercionKind)
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  high           |         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 panics on GHC 8.6 and later:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

 import Data.Kind
 import Data.Type.Equality

 data family Sing :: forall k. k -> Type
 data SomeSing :: Type -> Type where
   SomeSing :: Sing (a :: k) -> SomeSing k

 class SingKind k where
   type Demote k :: Type
   fromSing :: Sing (a :: k) -> Demote k
   toSing   :: Demote k -> SomeSing k

 data instance Sing (z :: a :~~: b) where
   SHRefl :: Sing HRefl

 instance SingKind (a :~~: b) where
   type Demote (a :~~: b) = a :~~: b
   fromSing SHRefl = HRefl
   toSing HRefl    = SomeSing SHRefl

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

 (~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)
                    (p :: forall (z :: Type) (y :: z). (a :~~: y) ~> Type)
                    (r :: a :~~: b).
             Sing r
          -> Apply p HRefl
          -> Apply p r
 (~>:~~:) SHRefl pHRefl = pHRefl

 type family Why (a :: j) (e :: a :~~: (y :: z)) :: Type where
   Why a (_ :: a :~~: y)  = y :~~: a

 data    WhySym (a :: j) :: forall   (y :: z). (a :~~: y) ~> Type
 -- data WhySym (a :: j) :: forall z (y :: z). (a :~~: y) ~> Type
 -- The version above does NOT panic
 type instance Apply (WhySym a) e = Why a e

 hsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).
         a :~~: b -> b :~~: a
 hsym eq = case toSing eq of
             SomeSing (singEq :: Sing r) ->
               (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
 }}}

 {{{
 $ /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.20180627 for x86_64-unknown-linux):
         coercionKind
   Nth:3
       (Inst {co_a1jI} (Coh <k_a1js[sk:1]>_N (Nth:0 (Sym {co_a1jI}))))
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in
 ghc:Outputable
         pprPanic, called at compiler/types/Coercion.hs:1887:9 in
 ghc:Coercion
 }}}

 As noted in the comments, replacing `WhySym` with a version that
 explicitly quantifies `z` avoids the panic.

 This is a regression from GHC 8.4.3, in which the program simply errored:

 {{{
 $ /opt/ghc/8.4.3/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:56:38: error:
     • Expected kind ‘forall z (y :: z). (a1 :~~: y) ~> *’,
         but ‘WhySym a’ has kind ‘forall (y :: z0).
                                  TyFun (a1 :~~: y) * -> *’
     • In the type ‘(WhySym a)’
       In the expression: (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
       In a case alternative:
           SomeSing (singEq :: Sing r)
             -> (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
     • Relevant bindings include
         singEq :: Sing a2 (bound at Bug.hs:55:23)
         eq :: a1 :~~: b (bound at Bug.hs:54:6)
         hsym :: (a1 :~~: b) -> b :~~: a1 (bound at Bug.hs:54:1)
    |
 56 |               (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
    |                                      ^^^^^^^^
 }}}

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