#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]