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. =( Wait. When you say “This seems to render produce kinds useless”, are you saying that in the code I wrote, you think irt should compile?? I reproduce it below for completeness. Simon {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-} module Knett where data Thrist :: ((i,i) -> *) -> (i,i) -> * where Nil :: Thrist a '(i,i) (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k) irt :: a x -> Thrist a x irt ax = ax :- Nil