Skip to content

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information