Same question. Do you expect the code below to type-check? I have stripped it down to essentials. Currently it’s rejected with Couldn't match type `a' with '(,) k k1 b0 d0 And that seems reasonable, doesn’t it? After all, in the defn of bidStar, (:*) returns a value of type Star x y ‘(a,c) ‘(b,d) which is manifestly incompatible with the claimed, more polymorphic type. And this is precisely the same error as comes from your class/instance example below, and for precisely the same reason. I must be confused. Simon {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-} module Product where data Star :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where (:*) :: x a b -> y c d -> Star x y '(a,c) '(b,d) bidStar :: Star T T a a bidStar = bidT :* bidT data T a b = MkT bidT :: T a a bidT = MkT From: Edward Kmett [mailto:ekmett@gmail.com] Sent: 31 August 2012 13:45 To: Simon Peyton-Jones Cc: glasgow-haskell-users@haskell.org Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency? Hrmm. This seems to render product kinds rather useless, as there is no way to refine the code to reflect the knowledge that they are inhabited by a single constructor. =( For instance, there doesn't even seem to be a way to make the following code compile, either. {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-} module Product where import Prelude hiding (id,(.)) class Category k where id :: k a a (.) :: k b c -> k a b -> k a c data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d) instance (Category x, Category y) => Category (x * y) where id = id :* id (xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg) This all works perfectly fine in Conor's SHE, (as does the thrist example) so I'm wondering where the impedence mismatch comes in and how to gain knowledge of this injectivity to make it work.