Core Lint error with EmptyCase
The following program gives a Core Lint error on GHC 8.2.2 and later:
{-# 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.
Trac metadata
Trac field | Value |
---|---|
Version | 8.4.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |