data B :: TYPE ('BoxedRep l) where
  T :: B
  F :: B

$WT :: B = CCS_DONT_CARE T! [coercionToken#];

$WF :: B = CCS_DONT_CARE F! [coercionToken#];

T :: forall {l :: Levity}. (l ~# 'Lifted) -> B =
    \r [eta_B0] T [coercionToken#];

F :: forall {l :: Levity}. (l ~# 'Lifted) -> B =
    \r [eta_B0] F [coercionToken#];

data B :: TYPE ('BoxedRep l) where
  T :: B
  F :: B

data Foo = Foo (B @'Unlifted)

fooT :: Foo
fooT = Foo T

    • Couldn't match a lifted type with an unlifted type
      Expected: B @'Unlifted
        Actual: B @'Lifted

data B :: forall l. TYPE ('BoxedRep l) where
  T :: B @l

    • Quantified type's kind mentions quantified type variable
        type: ‘forall (l :: Levity). B’
      where the body of the forall has this kind: ‘TYPE ('BoxedRep l)’

data B :: forall l. TYPE ('BoxedRep l) where
  T :: () -> B @l

data B :: forall l. TYPE ('BoxedRep l) where
  T :: () ~ () => B @l

type Lev a = () ~ () => a
class Bounded (a :: TYPE r) where
  minBound, maxBound :: Lev a