levity polymorphic types with higher kinds always infers `Lifted`, cannot convince it otherwise

Summary

When trying to use higher kinded levity polymorphic types, ghc always incorrectly infers Type and I cannot convince it otherwise

Steps to reproduce

{-# LANGUAGE UnliftedDatatypes #-}
{-# LANGUAGE UnliftedNewtypes #-}

module Levity where

import Data.Kind (Type)
import GHC.Exts (RuntimeRep (BoxedRep), TYPE, UnliftedType, Levity (Unlifted))

type BoxedType levity = TYPE ('BoxedRep levity)

type Higher :: forall lev k. (k -> BoxedType lev) -> k -> BoxedType lev
data Higher f a where
  MkHigher :: f a -> Higher f a

type I :: forall lev. BoxedType lev -> BoxedType lev
newtype I a = I a

type A :: UnliftedType
data A = MkA

type Wrap :: UnliftedType -> Type
data Wrap a where
  MkWrap :: a -> Wrap a

x :: Wrap (I A)
x = let ul  = I MkA in MkWrap ul

h :: Wrap (Higher @'Unlifted @UnliftedType I A)
h = let ul :: (Higher @'Unlifted @UnliftedType I A)
        ul = MkHigher (I MkA) 
     in MkWrap ul

where h doesn't type check with the following error:

GHCi, version 9.4.4: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /nix/store/nmwcbrq4hysnzl3yz4mgrm45kixdlwp1-hm_ghciconf
[1 of 1] Compiling Levity           ( Levity.hs, interpreted )

Levity.hs:30:14: error:
    • Couldn't match a lifted type with an unlifted type
      When matching types
        f0 :: BoxedType 'Unlifted -> BoxedType 'GHC.Types.Lifted
        I :: BoxedType 'Unlifted -> BoxedType 'Unlifted
      Expected: Higher I A
        Actual: Higher f0 A
    • In the expression: MkHigher (I MkA)
      In an equation for ‘ul’: ul = MkHigher (I MkA)
      In the expression:
        let
          ul :: (Higher @'Unlifted I A)
          ul = MkHigher (I MkA)
        in MkWrap ul
   |
30 |         ul = MkHigher (I MkA) in MkWrap ul
   |              ^^^^^^^^^^^^^^^^

Levity.hs:30:24: error:
    • Couldn't match a lifted type with an unlifted type
      When matching types
        f0 :: BoxedType 'Unlifted -> BoxedType 'GHC.Types.Lifted
        I :: BoxedType 'Unlifted -> BoxedType 'Unlifted
      Expected: f0 A
        Actual: I A
    • In the first argument of ‘MkHigher’, namely ‘(I MkA)’
      In the expression: MkHigher (I MkA)
      In an equation for ‘ul’: ul = MkHigher (I MkA)
   |
30 |         ul = MkHigher (I MkA) in MkWrap ul
   |                        ^^^^^
Failed, no modules loaded.
(0.01 secs,)

Expected behavior

I expect f0 to be inferred as the kind that I allows, namely UnliftedType -> UnliftedType

Environment

• GHC version used: 927, 944, 961

Optional:

• Operating System: NixOS 22.11
• System Architecture: x86_64-linux