Core Lint error with sneaky use of levity polymorphism in kinds
#14180 says that levity polymorphism in kinds isn't possible right now. Actually, this is only half true: it's possible if you leverage a backdoor. This backdoor is known as type synonyms:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UnboxedTuples #-}
{-# OPTIONS_GHC -dcore-lint #-}
module Bug where
import Data.Kind
type UT = (##) -> Type
data S :: UT where
MkS :: S '(##)
This program, when compiled with GHC 8.0 or later, will produce a Core Lint error. Here is the error on 8.10.2:
$ /opt/ghc/8.10.2/bin/ghc Bug.hs -dno-typeable-binds
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of CorePrep ***
Bug.hs:12:3: warning:
Kind application error in type ‘a_au1 ~# '()’
Function kind = forall k0 k1. k0 -> k1 -> TYPE ('TupleRep '[])
Arg kinds = [((# #), TYPE ('TupleRep '[])),
((# #), TYPE ('TupleRep '[])), (a_au1, (# #)), ('(), (# #))]
Forall: k0_10
*
((# #), TYPE ('TupleRep '[]))
In the type of a binder: MkS
In the type ‘forall (a :: (# #)). (a ~# '()) -> S a’
Substitution: [TCvSubst
In scope: InScope {a_au1 $WMkS}
Type env: []
Co env: []]
Bug.hs:12:3: warning:
Kind application error in type ‘a_au1 ~# '()’
Function kind = forall k0 k1. k0 -> k1 -> TYPE ('TupleRep '[])
Arg kinds = [((# #), TYPE ('TupleRep '[])),
((# #), TYPE ('TupleRep '[])), (a_au1, (# #)), ('(), (# #))]
Forall: k1_11
*
((# #), TYPE ('TupleRep '[]))
In the type of a binder: MkS
In the type ‘forall (a :: (# #)). (a ~# '()) -> S a’
Substitution: [TCvSubst
In scope: InScope {a_au1 $WMkS}
Type env: []
Co env: []]
Bug.hs:11:1: warning:
Kind application error in type ‘a_au1 ~# '()’
Function kind = forall k0 k1. k0 -> k1 -> TYPE ('TupleRep '[])
Arg kinds = [((# #), TYPE ('TupleRep '[])),
((# #), TYPE ('TupleRep '[])), (a_au1, (# #)), ('(), (# #))]
Forall: k0_10
*
((# #), TYPE ('TupleRep '[]))
In the RHS of MkS :: forall (a :: (# #)). (a ~# '()) -> S a
In the body of lambda with binder a_au1 :: (# #)
In the body of lambda with binder eta_B1 :: a_au1 ~# '()
Substitution: [TCvSubst
In scope: InScope {a_au1 $WMkS MkS}
Type env: []
Co env: []]
Bug.hs:11:1: warning:
Kind application error in type ‘a_au1 ~# '()’
Function kind = forall k0 k1. k0 -> k1 -> TYPE ('TupleRep '[])
Arg kinds = [((# #), TYPE ('TupleRep '[])),
((# #), TYPE ('TupleRep '[])), (a_au1, (# #)), ('(), (# #))]
Forall: k1_11
*
((# #), TYPE ('TupleRep '[]))
In the RHS of MkS :: forall (a :: (# #)). (a ~# '()) -> S a
In the body of lambda with binder a_au1 :: (# #)
In the body of lambda with binder eta_B1 :: a_au1 ~# '()
Substitution: [TCvSubst
In scope: InScope {a_au1 $WMkS MkS}
Type env: []
Co env: []]
*** Offending Program ***
$WMkS [InlPrag=INLINE[0]] :: S '()
[GblId[DataConWrapper], Caf=NoCafRefs, Str=m, Unf=OtherCon []]
$WMkS = MkS @ '() @~ (<'()>_N :: '() ~# '())
MkS :: forall (a :: (# #)). (a ~# '()) -> S a
[GblId[DataCon],
Arity=1,
Caf=NoCafRefs,
Str=<L,U>m,
Unf=OtherCon []]
MkS
= \ (@ (a_au1 :: (# #))) (eta_B1 :: a_au1 ~# '()) ->
MkS @ a_au1 @~ (eta_B1 :: a_au1 ~# '())
*** End of Offense ***
<no location info>: error:
Compilation had errors
Note that if you tried to inline the UT
type synonym's definition, like so:
data S :: (##) -> Type where
MkS :: S '(##)
Then GHC's typechecker would reject it:
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:11: error:
• Expecting a lifted type, but ‘(# #)’ is unlifted
• In the kind ‘(# #) -> Type’
In the data type declaration for ‘S’
|
11 | data S :: (##) -> Type where
| ^^^^
This is because (->)
has different typing rules depending on whether it is used in a type or kind position, as explained here. In a type position, (->)
is levity polymorphic in its arguments, but in a kind position, it is not. GHC treats the RHS of a type synonyms as a type position, so it happy accepts type UT = (##) -> Type
. When UT
is later used in a kind position like data S :: UT
, however, things go awry.
One way to fix this bug would be to fix #14180. But that would likely be a lot of work, so perhaps there is a way to at least cause this program not to typecheck in the meantime?