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?