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

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 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

...

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@gmail.com] *Sent:* 31 August 2012 13:45 *To:* Simon Peyton-Jones *Cc:* glasgow-haskell-users@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.****