Skip to content

Unresolved type family kind bug(?)

The following code:

{-# Language TypeInType #-}
{-# Language TypeFamilies #-}
module Main where
import Data.Kind
type family Knd (h :: k) :: Type
type family Foo (h :: k) (d :: Knd h) :: Type
data X
type instance Knd X = Type
type instance Foo X (d :: Type) = X

Produces the following error on the Foo X instance:

    • Expected kind ‘Knd X’, but ‘(d :: Type)’ has kind ‘*’
    • In the second argument of ‘Foo’, namely ‘(d :: Type)’
      In the type instance declaration for ‘Foo’
    |
    | type instance Foo X (d ∷ Type) = X
    |                     ^^^^^^^^^^

Which is unexpected because Knd X is defined to be Type on the line above.

Inserting an empty TH splice forces it to resolve. I.e, this works:

{-# Language TypeInType #-}
{-# Language TypeFamilies #-}
{-# Language TemplateHaskell #-}
module Main where
import Data.Kind
type family Knd (h :: k) :: Type
type family Foo (h :: k) (d :: Knd h) :: Type
data X
type instance Knd X = Type
pure []
type instance Foo X (d :: Type) = X

I've seen this happen with GHC v8.6.{3,4}

Edited by Liam Goodacre
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information