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