[GHC] #16188: GHC HEAD-only panic (buildKindCoercion)

[GHC]

#16188: GHC HEAD-only panic (buildKindCoercion)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.8.1
       Component:  Compiler (Type    |              Version:  8.7
  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:  #16204            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 It's unclear to me if this is the same issue or not, but in this slightly
 modified version of the original program:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wincomplete-patterns #-}
 module Bug where

 import Data.Kind (Type)
 import Data.Type.Bool (type (&&))
 import Data.Type.Equality ((:~:)(..))

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

 data instance Sing :: Bool -> Type where
   SFalse :: Sing False
   STrue  :: Sing True

 (%&&) :: forall (x :: Bool) (y :: Bool).
          Sing x -> Sing y -> Sing (x && y)
 SFalse %&& _ = SFalse
 STrue  %&& a = a

 data RegExp :: Type -> Type where
   App :: RegExp t -> RegExp t -> RegExp t

 data instance Sing :: forall t. RegExp t -> Type where
   SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2)

 data ReNotEmptySym0 :: forall t. RegExp t ~> Bool
 type instance Apply ReNotEmptySym0 r = ReNotEmpty r

 type family ReNotEmpty (r :: RegExp t) :: Bool where
   ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2

 sReNotEmpty :: forall t (r :: RegExp t).
                Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool)
 sReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2

 blah :: forall (t :: Type) (re :: RegExp t).
         Sing re -> (ReNotEmpty re :~: True) -> ()
 blah (SApp sre1 sre2) Refl
   = case (sReNotEmpty sre1, sReNotEmpty sre2) of
       (STrue, STrue) -> ()
 }}}

 You actually get different pattern-match coverage checker warnings on GHC
 8.6 and HEAD! GHC 8.6 compiles with no warnings, whereas on GHC HEAD you
 get:

 {{{
 $ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:49:5: warning: [-Wincomplete-patterns]
     Pattern match(es) are non-exhaustive
     In a case alternative: Patterns not matched: (SFalse, _)
    |
 49 |   = case (sReNotEmpty sre1, sReNotEmpty sre2) of
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
 ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 8.7.20190114 for x86_64-unknown-linux):
         buildKindCoercion
   Any
   ReNotEmpty re2_a1mg
   Bool
   t_a1ma
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in
 ghc:Outputable
         pprPanic, called at compiler/types/Coercion.hs:2427:9 in
 ghc:Coercion
 }}}

 It could just be that the types have become so screwed up (due to the
 explanation in comment:2) that the coverage checker becomes confused, but
 I thought this was worth pointing out nonetheless.

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