## Levity polymorphism checks are inadequate

Ben found

```
{-# LANGUAGE PolyKinds, TypeFamilies, MagicHash, DataKinds, TypeInType, RankNTypes #-}
import GHC.Exts
import GHC.Types
type family Boxed (a :: k) :: *
type instance Boxed Char# = Char
type instance Boxed Char = Char
class BoxIt (a :: TYPE lev) where
boxed :: a -> Boxed a
instance BoxIt Char# where boxed x = C# x
instance BoxIt Char where boxed = id
hello :: forall (lev :: Levity). forall (a :: TYPE lev). BoxIt a => a -> Boxed a
hello x = boxed x
{-# NOINLINE hello #-}
main :: IO ()
main = do
print $ boxed 'c'#
print $ boxed 'c'
print $ hello 'c'
print $ hello 'c'#
```

This is plainly wrong because we have a polymorphic function `boxed`

that is being passed both boxed and unboxed arguments.

You do get a Lint error with `-dcore-lint`

.

But the original problem is with the type signature for `boxed`

. We should never have a levity-polymorphic type to the left of an arrow. To the right yes, but to the left no. I suppose we could check that in `TcValidity`

.

See also #11471 (closed)