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