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

[Richard Eisenberg]

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 at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

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