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 <e...@cis.upenn.edu>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
>
>
>
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
