[GHC] #15549: Core Lint error with EmptyCase

[GHC]

#15549: Core Lint error with EmptyCase
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.8.1
       Component:  Compiler (Type    |              Version:  8.4.3
  checker)                           |             Keywords:  TypeFamilies,
      Resolution:                    |  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14729            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Another program, identified in
 https://ghc.haskell.org/trac/ghc/ticket/15725#comment:7, which may suffer
 from the same problems as described in this ticket:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}

 module Bug where

 import Data.Kind (Type)

 newtype Identity a = Identity a
 newtype Par1 a = Par1 a

 data family Sing :: forall k. k -> Type
 data instance Sing :: forall k. k -> Type

 type family Rep1 (f :: Type -> Type) :: Type -> Type
 type instance Rep1 Identity = Par1

 type family From1 (z :: f a) :: Rep1 f a
 type instance From1 ('Identity x) = 'Par1 x

 und :: a
 und = und

 f :: forall (a :: Type) (x :: Identity a).  Sing x
 f = g
     where g :: forall (a :: Type) (f :: Type -> Type) (x :: f a). Sing x
           g = seq (und :: Sing (From1 x)) und
 }}}
 {{{
 *** Core Lint errors : in result of Simplifier ***
 Bug.hs:25:1: warning:
     [in body of lambda with binder x_a19R :: Identity a_a19Q]
     Kind application error in
       coercion ‘(Sing
                    (D:R:Rep1Identity[0] <a_a19Q>_N) <From1 x_a19R>_N)_R’
       Function kind = forall k. k -> *
       Arg kinds = [(Par1 a_a19Q, *),
                    (From1 x_a19R, Rep1 Identity a_a19Q)]
     Fun: Par1 a_a19Q
          (From1 x_a19R, Rep1 Identity a_a19Q)
 Bug.hs:25:1: warning:
     [in body of lambda with binder x_a19R :: Identity a_a19Q]
     Kind application error in
       coercion ‘D:R:Singk0[0] <Par1 a_a19Q>_N <From1 x_a19R>_N’
       Function kind = Par1 a_a19Q -> *
       Arg kinds = [(From1 x_a19R, Rep1 Identity a_a19Q)]
     Fun: Par1 a_a19Q
          (From1 x_a19R, Rep1 Identity a_a19Q)
 Bug.hs:25:1: warning:
     [in body of lambda with binder x_a19R :: Identity a_a19Q]
     Kind application error in
       coercion ‘D:R:Singk0[0] <Par1 a_a19Q>_N <From1 x_a19R>_N’
       Function kind = Par1 a_a19Q -> *
       Arg kinds = [(From1 x_a19R, Rep1 Identity a_a19Q)]
     Fun: Par1 a_a19Q
          (From1 x_a19R, Rep1 Identity a_a19Q)
 <no location info>: warning:
     In the type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’
     Kind application error in
       type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’
       Function kind = forall k -> k -> *
       Arg kinds = [(Par1 a_a19Q, *),
                    (From1 x_a19R, Rep1 Identity a_a19Q)]
     Fun: Par1 a_a19Q
          (From1 x_a19R, Rep1 Identity a_a19Q)
 <no location info>: warning:
     In the type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’
     Kind application error in
       type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’
       Function kind = forall k -> k -> *
       Arg kinds = [(Par1 a_a19Q, *),
                    (From1 x_a19R, Rep1 Identity a_a19Q)]
     Fun: Par1 a_a19Q
          (From1 x_a19R, Rep1 Identity a_a19Q)
 }}}

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