Kind Inference fails when working with TypeFamilies of levity polymorphic kind
Summary
This code (usecase) used to typecheck on GHC 8.10.7, but it no longer works on either GHC 9.4.6 or GHC 9.7.20230527, here is a minimal example of the issue:
{-# LANGUAGE MagicHash, TypeFamilyDependencies, DataKinds #-}
module Test where
import Data.Kind (Type)
import GHC.Exts ( Int#, TYPE, RuntimeRep )
type FooKind :: RuntimeRep -> Type
type family FooKind rep = r | r -> rep where
FooKind rep = TYPE rep
type Foo :: forall (rep :: RuntimeRep). FooKind rep
type family Foo where
Foo = Int#
t :: () -> Foo
t _ = 42#
• Couldn't match a lifted type with an unlifted type
When matching types
Foo :: FooKind LiftedRep
Int# :: TYPE 'IntRep
• In the expression: 42#
In an equation for ‘t’: t _ = 42#typecheck(-Wdeferred-type-errors)
It seems that rep is too eager to resolve to LiftedRep, strangely, enabling PartialTypeSignatures and simply giving a wildcard type annotation to Foo in t fixes the inference problem.
t :: () -> (Foo :: _)
t _ = 42#
Now this typechecks correctly.
Edited by Ben Gamari