I think the issue is this. We have Strip :: forall k. * -> k When you say type instance Strip (Maybe a) = Maybe GHC infers the kind arguments (as with all hidden argument) to get type instance Strip (*->*) (Maybe a) = Maybe It would be fine to have another type instance like this type instance Strip (Maybe a) = Int which would turn into type instance Strip * (Maybe a) = Maybe In all cases, an occurrence of (Strip <kind> <type>) will match one of the "type instances" only if, well, it matches, including the kind. Does that answer the question. I would love someone to write some user guidance notes about this kind of thing, perhaps as a new sub-page of http://www.haskell.org/haskellwiki/GHC/Type_system Simon From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On Behalf Of José Pedro Magalhães Sent: 30 October 2012 10:29 To: GHC users Subject: Kind refinement in type families with PolyKinds Hi all, I'm wondering why the following does not work: {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeOperators #-} module Bug where -- Type equality data a :=: b where Refl :: a :=: a -- Applying a type to a list of arguments type family Apply (t :: k) (ts :: [*]) :: * type instance Apply t '[] = t type instance Apply (f :: * -> *) (t ': ts) = f t -- Stripping a type from all its arguments type family Strip (t :: *) :: k type instance Strip (Maybe a) = Maybe -- Reapplying a stripped type is the identity x :: Apply (Strip (Maybe a)) (a ': '[]) :=: Maybe a x = Refl If I ask GHCi for the kind of `Strip (Maybe Int)`, I get `k`, whereas I would expect `* -> *`. That explains why the `Apply` type family is not reduced further. I understand that this might be related to GADTs not being allowed to refine kinds; the following datatype fails to compile with the error "`D1' cannot be GADT-like in its *kind* arguments": data DStrip :: k -> * where D1 :: DStrip Maybe But then, shouldn't the type instance for `Strip` above trigger the same error? Thanks, Pedro