I tried this with the release candidate. I can go pull a more recent version and try again. On Thu, Aug 30, 2012 at 11:04 PM, Richard Eisenberg wrote:

This looks related to bug #7128. In the response to that (fixed, closed) bug report, Simon PJ said that functional dependencies involving kinds are supported. Are you compiling with a version of 7.6 updated since that bug fix?

Richard

On Aug 30, 2012, at 10:38 PM, Edward Kmett wrote:

If I define the following

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-} module Indexed.Test where

class IMonad (m :: (k -> *) -> k -> *) where ireturn :: a x -> m a x

infixr 5 :- data Thrist :: ((i,i) -> *) -> (i,i) -> * where Nil :: Thrist a '(i,i) (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

instance IMonad Thrist where ireturn a = a :- Nil

Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like

class IMonad k m where ireturn :: a x -> m a x

However, there doesn't appear to be a way to say that the kind k should be determined by m.

I tried doing:

class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x

Surprisingly (to me) this compiles and generates the correct constraints for IMonad:

ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x ghci> :info IMonad class IMonad k m | m -> k where ireturn :: a x -> m a x

But when I add

ghci> :{ Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where Prelude| Nil :: Thrist a '(i,i) Prelude| (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k) Prelude| :}

and attempt to introduce the instance, I crash:

ghci> instance IMonad Thrist where ireturn a = a :- Nil ghc: panic! (the 'impossible' happened) (GHC version 7.6.0.20120810 for x86_64-apple-darwin): lookupVarEnv_NF: Nothing

Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug

Moreover, attempting to compile them in separate modules leads to a different issue.

Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core.

Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.

-Edward _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

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. Also, does it ever make sense for the kind of a kind variable mentioned in a type not to get a functional dependency on the type? e.g. should class Foo (m :: k -> *) always be class Foo (m :: k -> *) | m -> k ? Honest question. I can't come up with a scenario, but you might have one I don't know. -Edward On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones wrote:

With the code below, I get this error message with HEAD. And that looks right to me, no?****

The current 7.6 branch gives the same message printed less prettily.****

** **

If I replace the defn of irt with****

irt :: a '(i,j) -> Thrist a '(i,j)****

irt ax = ax :- Nil****

** **

then it typechecks.****

** **

Simon****

** **

** **

Knett.hs:20:10:****

Couldn't match type `x' with '(i0, k0)****

`x' is a rigid type variable bound by****

the type signature for irt :: a x -> Thrist k a x at Knett.hs:19:8****

Expected type: Thrist k a x****

Actual type: Thrist k a '(i0, k0)****

In the expression: ax :- Nil****

In an equation for `irt': irt ax = ax :- Nil****

simonpj@cam-05-unx:~/tmp$****

** **

** **

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, ****

RankNTypes, TypeOperators, DefaultSignatures, DataKinds, ****

FlexibleInstances, UndecidableInstances #-}****

** **

module Knett where****

** **

class IMonad (m :: (k -> *) -> k -> *) | m -> k where ****

ireturn :: a x -> m a x****

** **

infixr 5 :-****

** **

data Thrist :: ((i,i) -> *) -> (i,i) -> * where****

Nil :: Thrist a '(i,i)****

(:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)****

** **

-- instance IMonad Thrist where****

-- ireturn a = a :- Nil****

** **

irt :: a x -> Thrist a x****

irt ax = ax :- Nil****

** **

** **

*From:* glasgow-haskell-users-bounces@haskell.org [mailto: glasgow-haskell-users-bounces@haskell.org] *On Behalf Of *Edward Kmett *Sent:* 31 August 2012 03:38 *To:* glasgow-haskell-users@haskell.org *Subject:* PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?****

** **

If I define the following****

** **

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}* ***

module Indexed.Test where****

** **

class IMonad (m :: (k -> *) -> k -> *) where ****

ireturn :: a x -> m a x****

** **

infixr 5 :-****

data Thrist :: ((i,i) -> *) -> (i,i) -> * where****

Nil :: Thrist a '(i,i)****

(:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)****

** **

instance IMonad Thrist where****

ireturn a = a :- Nil****

** **

Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like****

** **

class IMonad k m where****

ireturn :: a x -> m a x****

** **

However, there doesn't appear to be a way to say that the kind k should be determined by m. ****

** **

I tried doing:****

** **

class IMonad (m :: (k -> *) -> k -> *) | m -> k where ****

ireturn :: a x -> m a x****

** **

Surprisingly (to me) this compiles and generates the correct constraints for IMonad:****

** **

ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs****

ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x****

ghci> :info IMonad****

class IMonad k m | m -> k where****

ireturn :: a x -> m a x****

** **

But when I add ****

** **

ghci> :{****

Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where****

Prelude| Nil :: Thrist a '(i,i)****

Prelude| (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)****

Prelude| :}****

** **

and attempt to introduce the instance, I crash:****

** **

ghci> instance IMonad Thrist where ireturn a = a :- Nil****

ghc: panic! (the 'impossible' happened)****

(GHC version 7.6.0.20120810 for x86_64-apple-darwin):****

lookupVarEnv_NF: Nothing****

** **

Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug*** *

** **

Moreover, attempting to compile them in separate modules leads to a different issue. ****

** **

Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core.****

** **

Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?****

** **

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.****

** **

-Edward****

This works, though it'll be all sorts of fun to try to scale up. {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances, TypeFamilies #-} module Indexed.Test where class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x type family Fst (a :: (p,q)) :: p type instance Fst '(p,q) = p type family Snd (a :: (p,q)) :: q type instance Snd '(p,q) = q infixr 5 :- data Thrist :: ((i,i) -> *) -> (i,i) -> * where Nil :: Thrist a '(i,i) (:-) :: (Snd ij ~ Fst jk, Fst ij ~ Fst ik, Snd jk ~ Snd ik) => a ij -> Thrist a jk -> Thrist a ik instance IMonad Thrist where ireturn a = a :- Nil I know Agda has to jump through some hoops to make the refinement work on pairs when they do eta expansion. I wonder if this could be made less painful. On Fri, Aug 31, 2012 at 8:55 AM, Edward Kmett wrote:

Hrmm. This seems to work manually for getting product categories to work. Perhaps I can do the same thing for thrists.

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs, TypeFamilies #-} module Product where

import Prelude hiding (id,(.))

class Category k where id :: k a a (.) :: k b c -> k a b -> k a c

type family Fst (a :: (p,q)) :: p type instance Fst '(p,q) = p

type family Snd (a :: (p,q)) :: q type instance Snd '(p,q) = q

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where (:*) :: x (Fst a) (Fst b) -> y (Snd a) (Snd b) -> (x * y) a b

instance (Category x, Category y) => Category (x * y) where id = id :* id (xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

On Fri, Aug 31, 2012 at 8:44 AM, Edward Kmett wrote:

...

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.

Also, does it ever make sense for the kind of a kind variable mentioned in a type not to get a functional dependency on the type?

e.g. should

class Foo (m :: k -> *)

always be

class Foo (m :: k -> *) | m -> k

?

Honest question. I can't come up with a scenario, but you might have one I don't know.

-Edward

On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones < simonpj@microsoft.com> wrote:

...

With the code below, I get this error message with HEAD. And that looks right to me, no?****

The current 7.6 branch gives the same message printed less prettily.****

** **

If I replace the defn of irt with****

irt :: a '(i,j) -> Thrist a '(i,j)****

irt ax = ax :- Nil****

** **

then it typechecks.****

** **

Simon****

** **

** **

Knett.hs:20:10:****

Couldn't match type `x' with '(i0, k0)****

`x' is a rigid type variable bound by****

the type signature for irt :: a x -> Thrist k a x at Knett.hs:19:8****

Expected type: Thrist k a x****

Actual type: Thrist k a '(i0, k0)****

In the expression: ax :- Nil****

In an equation for `irt': irt ax = ax :- Nil****

simonpj@cam-05-unx:~/tmp$****

** **

** **

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, ****

RankNTypes, TypeOperators, DefaultSignatures, DataKinds, ** **

FlexibleInstances, UndecidableInstances #-}****

** **

module Knett where****

** **

class IMonad (m :: (k -> *) -> k -> *) | m -> k where ****

ireturn :: a x -> m a x****

** **

infixr 5 :-****

** **

data Thrist :: ((i,i) -> *) -> (i,i) -> * where****

Nil :: Thrist a '(i,i)****

(:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)****

** **

-- instance IMonad Thrist where****

-- ireturn a = a :- Nil****

** **

irt :: a x -> Thrist a x****

irt ax = ax :- Nil****

** **

** **

*From:* glasgow-haskell-users-bounces@haskell.org [mailto: glasgow-haskell-users-bounces@haskell.org] *On Behalf Of *Edward Kmett *Sent:* 31 August 2012 03:38 *To:* glasgow-haskell-users@haskell.org *Subject:* PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?****

** **

If I define the following****

** **

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-} ****

module Indexed.Test where****

** **

class IMonad (m :: (k -> *) -> k -> *) where ****

ireturn :: a x -> m a x****

** **

infixr 5 :-****

data Thrist :: ((i,i) -> *) -> (i,i) -> * where****

Nil :: Thrist a '(i,i)****

(:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)****

** **

instance IMonad Thrist where****

ireturn a = a :- Nil****

** **

Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like****

** **

class IMonad k m where****

ireturn :: a x -> m a x****

** **

However, there doesn't appear to be a way to say that the kind k should be determined by m. ****

** **

I tried doing:****

** **

class IMonad (m :: (k -> *) -> k -> *) | m -> k where ****

ireturn :: a x -> m a x****

** **

Surprisingly (to me) this compiles and generates the correct constraints for IMonad:****

** **

ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs****

ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x****

ghci> :info IMonad****

class IMonad k m | m -> k where****

ireturn :: a x -> m a x****

** **

But when I add ****

** **

ghci> :{****

Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where****

Prelude| Nil :: Thrist a '(i,i)****

Prelude| (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)****

Prelude| :}****

** **

and attempt to introduce the instance, I crash:****

** **

ghci> instance IMonad Thrist where ireturn a = a :- Nil****

ghc: panic! (the 'impossible' happened)****

(GHC version 7.6.0.20120810 for x86_64-apple-darwin):****

lookupVarEnv_NF: Nothing****

** **

Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug* ***

** **

Moreover, attempting to compile them in separate modules leads to a different issue. ****

** **

Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core.****

** **

Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?****

** **

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.****

** **

-Edward****

I ran into this same issue in my own experimentation: if a type variable x has a kind with only one constructor K, GHC does not supply the equality x ~ K y for some fresh type variable y. Perhaps it should. I too had to use similar workarounds to what you have come up with. One potential problem is the existence of the Any type, which inhabits every kind. Say x gets unified with Any. Then, we would have Any ~ K y, which is an inconsistent coercion (equating two types with distinct ground head types). However, because the RHS is a promoted datatype, we know that this coercion can never be applied to a term. Because equality is homogeneous (i.e. ~ can relate only two types of the same kind), I'm not convinced the existence of Any ~ K y is so bad. (Even with heterogeneous equality, it might work out, given that there is more than one type constructor that results in *...) Regarding the m -> k fundep: my experiments suggest that this dependency is implied when you have (m :: k), but I guess not when you have k appear in the kind of m in a more complicated way. Currently, there are no kind-level functions, so it appears that m -> k could be implied whenever k appears anywhere in the kind of m. If (when!) there are kind-level functions, we'll have to be more careful. Richard On Aug 31, 2012, at 9:06 AM, Edward Kmett wrote:

This works, though it'll be all sorts of fun to try to scale up.

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances, TypeFamilies #-} module Indexed.Test where

class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x

type family Fst (a :: (p,q)) :: p type instance Fst '(p,q) = p

type family Snd (a :: (p,q)) :: q type instance Snd '(p,q) = q

infixr 5 :- data Thrist :: ((i,i) -> *) -> (i,i) -> * where Nil :: Thrist a '(i,i) (:-) :: (Snd ij ~ Fst jk, Fst ij ~ Fst ik, Snd jk ~ Snd ik) => a ij -> Thrist a jk -> Thrist a ik

instance IMonad Thrist where ireturn a = a :- Nil

I know Agda has to jump through some hoops to make the refinement work on pairs when they do eta expansion. I wonder if this could be made less painful.

On Fri, Aug 31, 2012 at 8:55 AM, Edward Kmett wrote: Hrmm. This seems to work manually for getting product categories to work. Perhaps I can do the same thing for thrists.

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs, TypeFamilies #-} module Product where

import Prelude hiding (id,(.))

class Category k where id :: k a a (.) :: k b c -> k a b -> k a c

type family Fst (a :: (p,q)) :: p type instance Fst '(p,q) = p

type family Snd (a :: (p,q)) :: q type instance Snd '(p,q) = q

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where (:*) :: x (Fst a) (Fst b) -> y (Snd a) (Snd b) -> (x * y) a b

instance (Category x, Category y) => Category (x * y) where id = id :* id (xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

On Fri, Aug 31, 2012 at 8:44 AM, Edward Kmett wrote: 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.

Also, does it ever make sense for the kind of a kind variable mentioned in a type not to get a functional dependency on the type?

e.g. should

class Foo (m :: k -> *)

always be

class Foo (m :: k -> *) | m -> k

?

Honest question. I can't come up with a scenario, but you might have one I don't know.

-Edward

On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones wrote: With the code below, I get this error message with HEAD. And that looks right to me, no?

The current 7.6 branch gives the same message printed less prettily.

If I replace the defn of irt with

irt :: a '(i,j) -> Thrist a '(i,j)

irt ax = ax :- Nil

then it typechecks.

Simon

Knett.hs:20:10:

Couldn't match type `x' with '(i0, k0)

`x' is a rigid type variable bound by

the type signature for irt :: a x -> Thrist k a x at Knett.hs:19:8

Expected type: Thrist k a x

Actual type: Thrist k a '(i0, k0)

In the expression: ax :- Nil

In an equation for `irt': irt ax = ax :- Nil

simonpj@cam-05-unx:~/tmp$

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds,

RankNTypes, TypeOperators, DefaultSignatures, DataKinds,

FlexibleInstances, UndecidableInstances #-}

module Knett where

class IMonad (m :: (k -> *) -> k -> *) | m -> k where

ireturn :: a x -> m a x

infixr 5 :-

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

Nil :: Thrist a '(i,i)

(:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

-- instance IMonad Thrist where

-- ireturn a = a :- Nil

irt :: a x -> Thrist a x

irt ax = ax :- Nil

From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On Behalf Of Edward Kmett Sent: 31 August 2012 03:38 To: glasgow-haskell-users@haskell.org Subject: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

If I define the following

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}

module Indexed.Test where

class IMonad (m :: (k -> *) -> k -> *) where

ireturn :: a x -> m a x

infixr 5 :-

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

Nil :: Thrist a '(i,i)

(:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

instance IMonad Thrist where

ireturn a = a :- Nil

Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like

class IMonad k m where

ireturn :: a x -> m a x

However, there doesn't appear to be a way to say that the kind k should be determined by m.

I tried doing:

class IMonad (m :: (k -> *) -> k -> *) | m -> k where

ireturn :: a x -> m a x

Surprisingly (to me) this compiles and generates the correct constraints for IMonad:

ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs

ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x

ghci> :info IMonad

class IMonad k m | m -> k where

ireturn :: a x -> m a x

But when I add

ghci> :{

Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where

Prelude| Nil :: Thrist a '(i,i)

Prelude| (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

Prelude| :}

and attempt to introduce the instance, I crash:

ghci> instance IMonad Thrist where ireturn a = a :- Nil

ghc: panic! (the 'impossible' happened)

(GHC version 7.6.0.20120810 for x86_64-apple-darwin):

lookupVarEnv_NF: Nothing

Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug

Moreover, attempting to compile them in separate modules leads to a different issue.

Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core.

Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.

-Edward

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

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 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. Also, does it ever make sense for the kind of a kind variable mentioned in a type not to get a functional dependency on the type? e.g. should class Foo (m :: k -> *) always be class Foo (m :: k -> *) | m -> k ? Honest question. I can't come up with a scenario, but you might have one I don't know. -Edward On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones mailto:simonpj@microsoft.com> wrote: With the code below, I get this error message with HEAD. And that looks right to me, no? The current 7.6 branch gives the same message printed less prettily. If I replace the defn of irt with irt :: a '(i,j) -> Thrist a '(i,j) irt ax = ax :- Nil then it typechecks. Simon Knett.hs:20:10: Couldn't match type `x' with '(i0, k0) `x' is a rigid type variable bound by the type signature for irt :: a x -> Thrist k a x at Knett.hs:19:8 Expected type: Thrist k a x Actual type: Thrist k a '(i0, k0) In the expression: ax :- Nil In an equation for `irt': irt ax = ax :- Nil simonpj@cam-05-unx:~/tmp$ {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-} module Knett where class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x infixr 5 :- data Thrist :: ((i,i) -> *) -> (i,i) -> * where Nil :: Thrist a '(i,i) (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k) -- instance IMonad Thrist where -- ireturn a = a :- Nil irt :: a x -> Thrist a x irt ax = ax :- Nil From: glasgow-haskell-users-bounces@haskell.orgmailto:glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.orgmailto:glasgow-haskell-users-bounces@haskell.org] On Behalf Of Edward Kmett Sent: 31 August 2012 03:38 To: glasgow-haskell-users@haskell.orgmailto:glasgow-haskell-users@haskell.org Subject: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency? If I define the following {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-} module Indexed.Test where class IMonad (m :: (k -> *) -> k -> *) where ireturn :: a x -> m a x infixr 5 :- data Thrist :: ((i,i) -> *) -> (i,i) -> * where Nil :: Thrist a '(i,i) (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k) instance IMonad Thrist where ireturn a = a :- Nil Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like class IMonad k m where ireturn :: a x -> m a x However, there doesn't appear to be a way to say that the kind k should be determined by m. I tried doing: class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x Surprisingly (to me) this compiles and generates the correct constraints for IMonad: ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x ghci> :info IMonad class IMonad k m | m -> k where ireturn :: a x -> m a x But when I add ghci> :{ Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where Prelude| Nil :: Thrist a '(i,i) Prelude| (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k) Prelude| :} and attempt to introduce the instance, I crash: ghci> instance IMonad Thrist where ireturn a = a :- Nil ghc: panic! (the 'impossible' happened) (GHC version 7.6.0.20120810 for x86_64-apple-darwin): lookupVarEnv_NF: Nothing Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug Moreover, attempting to compile them in separate modules leads to a different issue. Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core. Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time? I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation. -Edward

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

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

Try translating into System FC! It’s not just a question of what the type checker will pass; we also have to produce a well-typed FC program. Remember that (putting in all the kind abstractions and applications: Thrist :: forall i. ((i,i) -> *) -> (i,i) -> * (:*) :: forall i j k. forall (a: (i,j) -> *). a '(i,j) -> Thrist (j,k) a '(j,k) -> Thrist (i,k) a '(i,k) So consider ‘irt’: irt :: forall i. forall (a : (i,i) -> *). forall (x : (i,i)). a x -> Thrist i a x irt = /\i. /\(a : (i,i) -> *). /\(x: (i,i). \(ax: a x). (:*) ? ? ? ? ax (Nil ...) So, what are the three kind args, and the type arg, to (:*)? It doesn’t seem to make sense... in the body of irt, (:*) produces a result of type Thrist (i,k) a ‘(i,k) but irt’s signature claims to produce a result of type Thrist i a x So irt’s signature is more polymorphic than its body. If we give irt a less polymorphic type signature, all is well irt :: forall p,q. forall (a : ((p,q),(p,q)) -> *). forall (x : ((p,q),(p,q))). a x -> Thrist (p,q) a x Maybe you can explain what you want in System FC? Type inference and the surface language come after that. If it can’t be expressed in FC it’s out of court. Of course we can always beef up System FC. I’m copying Stephanie and Conor who may have light to shed. Simon From: Edward Kmett [mailto:ekmett@gmail.com] Sent: 31 August 2012 18:27 To: Simon Peyton-Jones Cc: glasgow-haskell-users@haskell.orgmailto:glasgow-haskell-users@haskell.org Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency? 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

I'm not Conor, but I'll have a go... On 31/08/12 20:14, Simon Peyton-Jones wrote:

Try translating into System FC! It’s not just a question of what the type checker will pass; we also have to produce a well-typed FC program.

As Edward and others have recognised, the problem here is that FC coercions are not expressive enough to prove eta rules, that is forall x : (a, b) . x ~ (Fst x, Snd x) or more generally, that every element of a single-constructor (record) type is equal to the constructor applied to the projections. It seems like it should be perfectly fine to assert such a thing as an axiom, though: FC doesn't care what your equality proof is, provided it's consistent. Consistency of eta-laws follows from the fact that any inhabitant of the kind must be built with the sole constructor, unless you have Any (as Richard observed), in which case all bets are off. Why did you want Any again?

So consider ‘irt’:

irt :: forall i. forall (a : (i,i) -> *). forall (x : (i,i)).

a x -> Thrist i a x

irt = /\i. /\(a : (i,i) -> *). /\(x: (i,i). \(ax: a x).

(:*) ? ? ? ? ax (Nil ...)

So, what are the three kind args, and the type arg, to (:*)?

Here's my solution: irt = /\i. /\(a : (i,i) -> *). /\(x: (i,i). \(ax: a x). (:*) i i i a (ax |> g1) (Nil i a) |> g2 where g1 : a x ~ a '(Fst x, Snd x) g1 = < a > (eta x) g2 : Thrist i a '(Fst x, Snd x) ~ Thrist i a x g2 = < Thrist i a > (sym (eta x)) are coercions derived from the eta axiom above. Hope this helps, now I should really go on holiday, Adam

*From:*Edward Kmett [mailto:ekmett@gmail.com] *Sent:* 31 August 2012 18:27 *To:* Simon Peyton-Jones *Cc:* glasgow-haskell-users@haskell.org mailto:glasgow-haskell-users@haskell.org *Subject:* Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

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

Forgot to include the reference: [1] B. A. Yorgey et al. "Giving Haskell a Promotion" (http://www.seas.upenn.edu/~sweirich/papers/tldi12.pdf) On Sep 3, 2012, at 3:26 PM, Richard Eisenberg wrote:

On Sep 1, 2012, at 4:25 AM, Adam Gundry wrote:

...

As Edward and others have recognised, the problem here is that FC coercions are not expressive enough to prove eta rules, that is

forall x : (a, b) . x ~ (Fst x, Snd x)

or more generally, that every element of a single-constructor (record) type is equal to the constructor applied to the projections.

It seems like it should be perfectly fine to assert such a thing as an axiom, though, ... unless you have Any (as Richard observed), in which case all bets are off. Why did you want Any again?

I don't necessarily want Any, but Any is already there, in GHC.Exts. (Though, Any has been helpful in other type hackery exploits of mine...) So, any way of introducing eta-coercions will have to respect Any.

Intriguingly, the most recent published formulation of FC [1] leaves room for adding eta rules. The issue is one of consistency: if we have a coercion g : forall k1. forall k2. forall x:(k1,k2). x ~ (Fst x, Snd x) and the existence of Any : forall k.k, can we derive h : Int ~ Bool? In [1], the rules for consistency (from which progress & preservation are proved) apply only to coercions at a base kind, either * or Constraint. So, our eta coercion g is exempt from the consistency check -- it cannot make a system inconsistent. Thus, with or without Any, the coercion g cannot lead to a program that crashes due to a type error.

So, it seems possible to introduce eta coercions into FC for all kinds containing only one type constructor without sacrificing soundness. How the type inference engine/source Haskell triggers the use of these coercions is another matter, but there doesn't seem to be anything fundamentally wrong with the idea.

Richard

I retract my statement. My mistake was that I looked at the definition for consistency in FC -- which correctly is agnostic to non-base-kind coercions -- and applied it only to the set of coercion assumptions, not to any coercion derivable from the assumptions. As Andrea's example shows, by assuming an eta coercion, it is possible to derive an inconsistent coercion. Examining the definition for FC consistency more closely, an eta coercion does not match to the form allowed for coercion assumptions used to prove consistency. The proof, in [1], requires all assumptions to have a type family application on the left-hand side. An eta coercion does not have a type family application on either side, and so the consistency proof in [1] does not apply. In light of this, it would seem that allowing eta coercions while retaining consistency would require some more work. Thanks for pointing out my mistake. Richard [1] S. Weirich et al. "Generative Type Abstraction and Type-level Computation." (http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf) On Sep 3, 2012, at 10:28 PM, Andrea Vezzosi wrote:

On Mon, Sep 3, 2012 at 9:26 PM, Richard Eisenberg wrote:

...

[...] So, it seems possible to introduce eta coercions into FC for all kinds containing only one type constructor without sacrificing soundness. How the type inference engine/source Haskell triggers the use of these coercions is another matter, but there doesn't seem to be anything fundamentally wrong with the idea.

A recent snapshot of ghc HEAD doesn't seem to agree:

{-# LANGUAGE GADTs, KindSignatures, PolyKinds, DataKinds, TypeFamilies, ScopedTypeVariables, TypeOperators #-}

import GHC.Exts import Unsafe.Coerce

data (:=:) :: k -> k -> * where Refl :: a :=: a

trans :: a :=: b -> b :=: c -> a :=: c trans Refl Refl = Refl

type family Fst (x :: (a,b)) :: a type family Snd (x :: (a,b)) :: b

type instance Fst '(a,b) = a type instance Snd '(a,b) = b

eta :: x :=: '(Fst x, Snd x) eta = unsafeCoerce Refl -- ^^^ this is an acceptable way to simulate new coercions, i hope

type family Bad s t (x :: (a,b)) :: * type instance Bad s t '(a,b) = s type instance Bad s t Any = t

refl_Any :: Any :=: Any refl_Any = Refl

cong_Bad :: x :=: y -> Bad s t x :=: Bad s t y cong_Bad Refl = Refl

s_eq_t :: forall (s :: *) (t :: *). s :=: t s_eq_t = cong_Bad (trans refl_Any eta)

subst :: x :=: y -> x -> y subst Refl x = x

coerce :: s -> t coerce = subst s_eq_t

{- GHCi, version 7.7.20120830: http://www.haskell.org/ghc/ :? for help *Main> coerce (4.0 :: Double) :: (Int,Int) (Segmentation fault -}

-- Andrea Vezzosi

On Sep 5, 2012, at 2:21 PM, Edward Kmett wrote:

I noticed that the polykindedness of Any is abused in the GHC.TypeLits to make fundeps determining a kind, but where else is it exploited?

I similarly abused Any to write the singletons library, but it's really a hack to work with kind classes and functions from kinds to types. If these features were directly accessible, the Any hack would no longer be needed. Has anyone out there used Any for another purpose? Richard

On Sun, Sep 16, 2012 at 5:49 PM, Simon Peyton-Jones wrote:

Fixing Any ~~~~~~~ * I think we can fix the Any problem readily by making Any into a type family, that has no instances. We certainly allow equalities with a type *family* application on the left and a type constructor on the right. I have implemented this change already... it seems like a good plan.

Will unsafeCoercing to and from Any still work with this plan? (If not then I can just use data Anything = forall a. Anything a, so it's not a big deal.) -- Your ship was destroyed in a monadic eruption.

I think I was a little hasty below, and need a little help. Making 'Any' an type family, even an injective one, does not work for the use that Richard and Iavor make of it, eg in TypeLits. Here's an example from TypeLits: instance SingE (Any :: Nat) Integer where where SingE :: forall k. k -> * -> Constraint Here Iavor is using Any as a proxy kind argument. He really wants SingE :: forall k. * -> Constraint with kind-indexed instances. But (much as with the Typeable class at the value level) he is giving it a type argument so that he can later say things like SingE (Any :: *->*) v Without this trick we'd need kind application, something like SingE {*->*} v None of this works if Any is a type family, because the type patterns in an instance decl aren't allowed to involve type families (and rightly so; value declarations don't have functions in patterns). Nor can we fix this by introducing some *other* constant, Proxy :: forall k. k, because that suffers from the inconsistency problem that we started with. Another way to say this is as follows. In the value world we have often written typeOf (undefined :: a) using bottom as a proxy type argument. That works in Haskell, but not in a strict, or strongly-normalising language. And at the type level we are (mostly) strongly normalising. The technically-straightforward thing to do is to add kind application, but that's a bit complicated notationally. http://hackage.haskell.org/trac/ghc/wiki/ExplicitTypeApplication Does anyone have any other ideas? Simon | -----Original Message----- | From: Simon Peyton-Jones | Sent: 16 September 2012 16:49 | To: Richard Eisenberg; Andrea Vezzosi | Cc: Adam Gundry; Conor McBride; Stephanie Weirich; glasgow-haskell- | users@haskell.org; Simon Peyton-Jones | Subject: RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a | functional dependency? | | Friends | | Thanks for this useful conversation, by email and at ICFP. Here's my | summary. Please tell me if I'm on the right track. It would be great | if someone wanted to create a page on the GHC wiki to capture the issues | and outcomes. | | Simon | | Eta rules | ~~~~~~ | * We want to add eta-rules to FC. Sticking to pairs for now, that | would amount to | adding two new type functions (Fst, Snd), and three new, built-in | axioms | axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a) | axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a | axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a | Generalising to arbitrary products looks feasible. | | * Adding these axioms would make FC inconsistent, because | axPair * * (Any '(*,*) ) : Any '(*,*) ~ (Fst .., Snd ..) | and that has two different type constructors on each side. | However, I think is readily solved: see below under "Fixing Any" | | * Even in the absence of Any, it's not 100% obvious that adding the | above | eta axioms retains consistency of FC. I believe that Richard is | volunteering | to check this out. Right, Richard? | | Type inference | ~~~~~~~~~ | I'm a little unclear about the implications for inference. One route | might be this. Suppose we are trying to solve a constraint | [W] (a:'(k1,ks)) ~ '( t1, t2 ) | where a is an untouchable type variable. (if it was touchable we'd | simply unify it.) Then we can replace it with a constraint | [W] '(Fst a, Snd a) ~ '( t1, t2) | | Is that it? Or do we need more? I'm a bit concerned about constraints | like | F a ~ e | where a:'(k1,k2), and we have a type instance like F '(a,b) = ... | | Anything else? | | I don't really want to eagerly eta-expand every type variable, because | (a) we'll bloat the constraints and (b) we might get silly error | messages. For (b) consider the insoluble constraint | [W] a~b | where a and b are both skolems of kind '(k1,k2). If we eta-expand both | we'll get two insoluble constraints (Fst a ~ Fst b) and (Snd a ~ Snd b), | and we DEFINITELY don't want to report that as a type error! | | Fixing Any | ~~~~~~~ | * I think we can fix the Any problem readily by making Any into a type | family, | that has no instances. We certainly allow equalities with a type | *family* application on the left and a type constructor on the | right. | I have implemented this change already... it seems like a good | plan. | | * Several people have asked why we need Any at all. Consider this | source program | reverse [] | At what type should we instantiate 'reverse' and the empty list []? | Any type | will do, but we must choose one; FC doesn't have unbound type | variables. | So I instantiate it at (Any *): | reverse (Any *) ([] (Any *)) | | Why is Any poly-kinded? Because the above ambiguity situation | sometimes | arises at other kinds. | | * I'm betting that making Any into a family will mess up Richard's | (entirely separate) | use of (Any k) as a proxy for a kind argument k; because now (Any | k1 ~ Any k2) | does not entail (k1~k2). We need Any to be an *injective* type | family. We want | injective type families anyway, so I guess I should add the | internal machinery | (which is easy). | | I believe that injective type families are fully decomposable, just | like data type families, | correct? To make them available at the source level, we'd just | need to | a) add the syntax injective type family F a :: * | b) check for injectivity when the user adds type instances | Richard, would you like to do that part?

On Sun, Sep 16, 2012 at 5:49 PM, Simon Peyton-Jones wrote:

[...] Type inference ~~~~~~~~~ I'm a little unclear about the implications for inference. One route might be this. Suppose we are trying to solve a constraint [W] (a:'(k1,ks)) ~ '( t1, t2 ) where a is an untouchable type variable. (if it was touchable we'd simply unify it.) Then we can replace it with a constraint [W] '(Fst a, Snd a) ~ '( t1, t2)

Is that it? Or do we need more? I'm a bit concerned about constraints like F a ~ e where a:'(k1,k2), and we have a type instance like F '(a,b) = ...

F a ~ F '(Fst a, Snd a) has to hold, so one does need to expand a for constraints like F a ~ e in this case. One way to think of it is that patterns like '(a,b) are the same as value-level ~(a,b) ones. -- Andrea

On Wed, Sep 19, 2012 at 1:51 PM, Richard Eisenberg wrote:

As for recovering "kind classes" and such once Any is made into a type family: I'm in favor of finding some way to do explicit kind instantiation, making the Any trick obsolete. I'm happy to leave it to others to decide the best concrete syntax.

I'll admit I haven't parsed this entire email thread, but I read enough of it early on that I wanted to avoid Any recently. Returning to find this quote from Richard, perhaps the trick I came up is the one you're after. (Also — what's the general status on this initiative? Has much happened in about a month?) The to my trick key is to use the promotion of this data type.

data KindProxy (k :: *) = KindProxy

I needed it in order to define this family, which counts the number of arguments a kind has.

type family CountArgs (kp :: KindProxy k) :: Nat type instance CountArgs (kp :: *) = Z type instance CountArgs (kp :: kD -> kR) = S (CountArgs ('KindProxy :: KindProxy kR))

The proxy is necessary on the RHS of the second instance, in which I need a type of kind kR, but I wouldn't have any means to build one (without Any) were CountArgs simply of kind (k -> Nat). This usage is comparable to Richard's usage in the singletons library, insomuch as I understand from the Haskell 2012 paper. I'm less familiar with the usage in GHC.TypeLits. At a quick glance, I believe I'd change SingE like so

class SingE (kparam :: KindProxy k) rep | kparam -> rep where fromSing :: Sing (a :: k) -> rep

instance SingE (kparam :: KindProxy Nat) Integer where fromSing (SNat n) = n

instance SingE (kparam :: KindProxy Symbol) String where fromSing (SSym s) = s

However, looking through the rest of that module, I see no point where a proxy is actually required (as it is required in the second case of CountArgs). Maybe I'm just missing it, or maybe Iavor is just interested in *enforcing* the fact that the type is not of consequence? Along those same lines… Iavor had SingE instances declared for (Any :: KindProxy Nat) and (Any :: KindProxy Symbol). I'm not sure why he didn't leave the type polymorphic, as I have. Perhaps it matters for various uses of SingE? I haven't tried using my code with examples, so maybe that's where issues would show up. If it were necessary, the instances could instead be as follows.

instance SingE ('KindProxy :: KindProxy Nat) Integer where fromSing (SNat n) = n

instance SingE ('KindProxy :: KindProxy Symbol) String where fromSing (SSym s) = s

Is this the kind of trick you were after, Richard? It might pollute the code base and interface a bit with KindProxy wrappers, but I've not found that insurmountable. Hopefully that isn't a show stopper for you. HTH

On Oct 11, 2012, at 11:20 PM, Nicolas Frisby wrote:

(Also — what's the general status on this initiative? Has much happened in about a month?)

From my end, nothing. I'm trying to wrap up some other work I'm doing on GHC (ordered overlapping type family instances), and it looks like some of the questions I raised in my last email in this thread are still open.

The to my trick key is to use the promotion of this data type.

...

data KindProxy (k :: *) = KindProxy

Yes, I used this in an earlier version of singletons. Then, Simon told me about Any, and that cleaned up the code considerably. I don't think, though, there was anything fundamentally wrong (other than aesthetics) with KindProxy. Thanks for bringing this up, as I had forgotten about this approach in the intervening months.

I'm less familiar with the usage in GHC.TypeLits.

Iavor and I collaborated on the design of the building blocks of singleton types, as we wanted our work to be interoperable. A recent scan through TypeLits tells me, though, that somewhere along the way, our designs diverged a bit. Somewhere on the to-do list is to re-unify the interfaces, and actually just to import TypeLits into Data.Singletons so the definitions are one and the same. Iavor, I'm happy to talk about the details if you are. Nick, thanks for pushing on this thread! Richard

| Iavor and I collaborated on the design of the building blocks of | singleton types, as we wanted our work to be interoperable. A recent | scan through TypeLits tells me, though, that somewhere along the way, | our designs diverged a bit. Somewhere on the to-do list is to re-unify | the interfaces, and actually just to import TypeLits into | Data.Singletons so the definitions are one and the same. Iavor, I'm | happy to talk about the details if you are. That would be good! Simon