[GHC] #15588: Panic when abusing kind inference

[GHC]

#15588: Panic when abusing kind inference
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.5
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 When I say

 {{{#!hs
 {-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
              AllowAmbiguousTypes #-}

 import Data.Proxy
 import Data.Type.Equality
 import Data.Type.Bool
 import Data.Kind

 data SameKind :: forall k. k -> k -> Type
 type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n
 where
    IfK (_ :: Proxy True)  f _ = f
    IfK (_ :: Proxy False) _ g = g

 y :: forall ck (c :: ck). ck :~: Proxy True -> ()
 y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
              x = undefined
          in ()
 }}}

 HEAD says

 {{{
 ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 8.7.20180827 for x86_64-apple-darwin):
         ASSERT failed!
   Bad coercion hole co_a3iZ: If
                                j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]
                              a_a3gV[sk:3]
                              nominal
                              If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3]
 ~# a_a3jj[sk:3]
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in
 ghc:Outputable
         pprPanic, called at compiler/utils/Outputable.hs:1219:5 in
 ghc:Outputable
         assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in
 ghc:TcMType

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

 It's as yet unclear whether the program should be accepted. My best guess
 is that it should, but that (even with this panic fixed) GHC isn't up to
 the task.

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