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

[Simon Peyton-Jones]

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 at gmail.com]
Sent: 31 August 2012 13:45
To: Simon Peyton-Jones
Cc: glasgow-haskell-users at 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120831/6e2f0bda/attachment-0001.htm>