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.