Re: [GHC] #15549: Core Lint error with EmptyCase (was: Core Lint error with empty closed type family)

21 Aug 2018

      #15549: Core Lint error with EmptyCase
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.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:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Never mind, empty closed type families have nothing to do with this.
 Here's an even more minimal way to reproduce the Core Lint error:

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

 import Data.Proxy
 import Data.Void

 data family Sing (a :: k)
 data instance Sing (z :: Void)

 type family Rep a
 class SGeneric a where
   sTo :: forall (r :: Rep a). Sing r -> Proxy a

 type instance Rep Void = Void
 instance SGeneric Void where
   sTo x = case x of
 }}}
 {{{
 $ /opt/ghc/8.4.3/bin/ghc Bug.hs -dcore-lint
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
 *** Core Lint errors : in result of Simplifier ***
 Bug.hs:19:7: warning:
     [in body of lambda with binder x_ayn :: Sing r_azJ]
     Kind application error in
       coercion ‘(Sing (D:R:RepVoid[0]) <r_azJ>_N)_R’
       Function kind = forall k. k -> *
       Arg kinds = [(Void, *), (r_azJ, Rep Void)]
     Fun: Void
          (r_azJ, Rep Void)
 Bug.hs:19:7: warning:
     [in body of lambda with binder x_ayn :: Sing r_azJ]
     Kind application error in coercion ‘D:R:SingVoidz0[0] <r_azJ>_N’
       Function kind = Void -> *
       Arg kinds = [(r_azJ, Rep Void)]
     Fun: Void
          (r_azJ, Rep Void)
 Bug.hs:19:7: warning:
     [in body of lambda with binder x_ayn :: Sing r_azJ]
     Kind application error in coercion ‘D:R:SingVoidz0[0] <r_azJ>_N’
       Function kind = Void -> *
       Arg kinds = [(r_azJ, Rep Void)]
     Fun: Void
          (r_azJ, Rep Void)
 <no location info>: warning:
     In the type ‘R:SingVoidz r_azJ’
     Kind application error in type ‘R:SingVoidz r_azJ’
       Function kind = Void -> *
       Arg kinds = [(r_azJ, Rep Void)]
     Fun: Void
          (r_azJ, Rep Void)
 <no location info>: warning:
     In the type ‘R:SingVoidz r_azJ’
     Kind application error in type ‘R:SingVoidz r_azJ’
       Function kind = Void -> *
       Arg kinds = [(r_azJ, Rep Void)]
     Fun: Void
          (r_azJ, Rep Void)
 *** Offending Program ***
 $csTo_azH :: forall (r :: Rep Void). Sing r -> Proxy Void
 [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_azH
   = \ (@ (r_azJ :: Rep Void)) (x_ayn :: Sing r_azJ) ->
       case x_ayn
            `cast` ((Sing
                       (D:R:RepVoid[0]) <r_azJ>_N)_R ; D:R:SingVoidz0[0]
 <r_azJ>_N
                    :: (Sing r_azJ :: *) ~R# (R:SingVoidz r_azJ :: *))
       of nt_s14C {
       }
 }}}

 However, `EmptyCase` does appear to play an important role. If I change
 the implementation of `sTo` to this:

 {{{#!hs
 instance SGeneric Void where
   sTo x = x `seq` undefined
 }}}

 Then the Core Lint error goes away, and the generated Core for `sTo`
 instead becomes:

 {{{
 $csTo_r2IT :: forall (r :: Rep Void). Sing r -> Proxy Void
 [GblId, Arity=1, Caf=NoCafRefs]
 $csTo_r2IT
   = \ (@ (r_a1F4 :: Rep Void)) (x_X1DH :: Sing r_a1F4) ->
       break<0>(x_X1DH)
       case x_X1DH
            `cast` ((Sing
                       (Bug.D:R:RepVoid[0])
                       (Sym (Coh <r_a1F4>_N
                                 (Bug.D:R:RepVoid[0]))))_R ;
 Bug.D:R:SingVoidz0[0] (Sym (Coh (Sym (Coh <r_a1F4>_N
 (Bug.D:R:RepVoid[0])))
 (Bug.D:R:RepVoid[0])))
                    :: (Sing r_a1F4 :: *)
                       ~R# (Bug.R:SingVoidz (r_a1F4 |> Bug.D:R:RepVoid[0])
 :: *))
       of {
       }
 }}}

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