#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]) _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] _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] _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=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]) _N)_R ; D:R:SingVoidz0[0]
_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 _N
(Bug.D:R:RepVoid[0]))))_R ;
Bug.D:R:SingVoidz0[0] (Sym (Coh (Sym (Coh _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
