PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Simon Peyton-Jones]

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


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120831/3866573d/attachment.htm>