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

[Edward Kmett]

Also, even after upgrading to HEAD, I'm getting a number of errors like:

[2 of 8] Compiling Indexed.Functor  ( src/Indexed/Functor.hs,
dist/build/Indexed/Functor.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 7.7.20120830 for x86_64-apple-darwin):
tc_fd_tyvar
    k{tv aZ8}
    k{tv l} [sig]
    ghc-prim:GHC.Prim.BOX{(w) tc 347}

I'll try to distill this down to a reasonable test case.

-Edward

On Fri, Aug 31, 2012 at 1:26 PM, Edward Kmett <ekmett at gmail.com> wrote:

> It is both perfectly reasonable and unfortunately useless. :(
>
> The problem is that the "more polymorphic" type isn't any more
> polymorphic, since (ideally) the product kind (a,b) is only inhabited by
> things of the form '(x,y).
>
> The product kind has a single constructor. But there is no way to express
> this at present that is safe.
>
> As it stands, I can fake this to an extent in one direction, by writing
>
> {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
> MultiParamTypeClasses, PolyKinds, TypeFamilies,
>              RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
>              FlexibleInstances, UndecidableInstances #-}
>
> module Kmett where
>
> type family Fst (p :: (a,b)) :: a
> type instance Fst '(a,b) = a
>
> type family Snd (p :: (a,b)) :: b
> type instance Snd '(a,b) = b
>
> data Thrist :: ((i,i) -> *) -> (i,i) -> * where
>   Nil  :: Thrist a '(i,i)
>   (:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =>
>           a ij -> Thrist a '(j,k) -> Thrist a ik
>
> irt :: a x -> Thrist a x
> irt ax = ax :- Nil
>
> and this compiles, but it just pushes the problem down the road, because
> with that I can show that given ij :: (x,y), I can build up a tuple '(Fst
> ij, Snd ij) :: (x,y)
>
> But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later
> when you go to define an indexed bind, and type families are insufficient
> to the task. Right now to get this property I'm forced to fake it with
> unsafeCoerce.
>
> -Edward
>
> On Fri, Aug 31, 2012 at 1:00 PM, Simon Peyton-Jones <simonpj at microsoft.com
> > wrote:
>
>>  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/3ad6e9ae/attachment-0001.htm>