[GHC] #15549: Core Lint error with empty closed type family

[GHC]

#15549: Core Lint error with empty closed type family
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
  (Type checker)                     |
           Keywords:  TypeFamilies,  |  Operating System:  Unknown/Multiple
  TypeInType                         |
       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 gives a Core Lint error on GHC 8.2.2 and later:

 {{{#!hs
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Bug where

 import Data.Kind
 import Data.Void

 data family Sing (a :: k)

 data V1 :: Type -> Type
 data instance Sing (z :: V1 p)

 class Generic a where
   type Rep a :: Type -> Type
   to :: Rep a x -> a

 class PGeneric a where
   type To (z :: Rep a x) :: a

 class SGeneric a where
   sTo :: forall x (r :: Rep a x). Sing r -> Sing (To r :: a)

 -----

 instance Generic Void where
   type Rep Void = V1
   to x = case x of {}

 type family EmptyCase (a :: j) :: k where

 instance PGeneric Void where
   type To x = EmptyCase x

 instance SGeneric Void where
   sTo x = case x of
 }}}
 {{{
 $ /opt/ghc/8.4.3/bin/ghc Bug.hs -dcore-lint -fforce-recomp
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
 *** Core Lint errors : in result of Simplifier ***
 Bug.hs:38:7: warning:
     [in body of lambda with binder x_aZ8 :: Sing r_a12q]
     Kind application error in
       coercion ‘(Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R’
       Function kind = forall k. k -> *
       Arg kinds = [(V1 x_a12p, *), (r_a12q, Rep Void x_a12p)]
     Fun: V1 x_a12p
          (r_a12q, Rep Void x_a12p)
 Bug.hs:38:7: warning:
     [in body of lambda with binder x_aZ8 :: Sing r_a12q]
     Kind application error in
       coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
       Function kind = V1 x_a12p -> *
       Arg kinds = [(r_a12q, Rep Void x_a12p)]
     Fun: V1 x_a12p
          (r_a12q, Rep Void x_a12p)
 Bug.hs:38:7: warning:
     [in body of lambda with binder x_aZ8 :: Sing r_a12q]
     Kind application error in
       coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
       Function kind = V1 x_a12p -> *
       Arg kinds = [(r_a12q, Rep Void x_a12p)]
     Fun: V1 x_a12p
          (r_a12q, Rep Void x_a12p)
 <no location info>: warning:
     In the type ‘R:SingV1z x_a12p r_a12q’
     Kind application error in type ‘R:SingV1z x_a12p r_a12q’
       Function kind = forall p -> V1 p -> *
       Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
     Fun: V1 x_a12p
          (r_a12q, Rep Void x_a12p)
 <no location info>: warning:
     In the type ‘R:SingV1z x_a12p r_a12q’
     Kind application error in type ‘R:SingV1z x_a12p r_a12q’
       Function kind = forall p -> V1 p -> *
       Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
     Fun: V1 x_a12p
          (r_a12q, Rep Void x_a12p)
 *** Offending Program ***

 <elided>

 $csTo_a12n :: forall x (r :: Rep Void x). Sing r -> Sing (To r)
 [LclId,
  Arity=1,
  Str=<L,U>x,
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
          Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
 $csTo_a12n
   = \ (@ x_a12p)
       (@ (r_a12q :: Rep Void x_a12p))
       (x_aZ8 :: Sing r_a12q) ->
       case x_aZ8
            `cast` ((Sing
                       (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R ;
 D:R:SingV1z0[0]
 <x_a12p>_N <r_a12q>_N
                    :: (Sing r_a12q :: *) ~R# (R:SingV1z x_a12p r_a12q ::
 *))
       of nt_s13T {
       }
 }}}

 GHC 8.0.2 does not appear to suffer from this Core Lint error.

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