<div>If I define the following</div><div><br></div><div><font face="courier new, monospace">{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}</font></div>
<div><font face="courier new, monospace">module Indexed.Test where</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">class IMonad (m :: (k -> *) -> k -> *) </font><span style="font-family:'courier new',monospace">where </span></div>
<div><span style="font-family:'courier new',monospace"> ireturn :: a x -> m a x</span></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">infixr 5 :-</font></div>
<div><font face="courier new, monospace">data Thrist :: ((i,i) -> *) -> (i,i) -> * where</font></div><div><font face="courier new, monospace"> Nil :: Thrist a '(i,i)</font></div><div><font face="courier new, monospace"> (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">instance IMonad Thrist where</font></div><div><font face="courier new, monospace"> ireturn a = a :- Nil</font></div><div>
<font face="courier new, monospace"><br></font></div><div><font face="arial, helvetica, sans-serif">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</font></div>
<div><font face="arial, helvetica, sans-serif"><br></font></div><div><div><div><font face="courier new, monospace">class IMonad k m where</font></div><div><font face="courier new, monospace"> ireturn :: a x -> m a x</font></div>
</div></div><div><br></div><div><font face="arial, helvetica, sans-serif">However, there doesn't appear to be a way to say that the kind k should be determined by m. </font></div><div><font face="arial, helvetica, sans-serif"><br>
</font></div><div><font face="arial, helvetica, sans-serif">I tried doing:</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><div><font face="courier new, monospace">class IMonad (m :: (k -> *) -> k -> *) | m -> k </font><span style="font-family:'courier new',monospace">where </span></div>
<div><span style="font-family:'courier new',monospace"> ireturn :: a x -> m a x</span></div></div><div><br></div><div><font face="arial, helvetica, sans-serif">Surprisingly (to me) this compiles and generates the correct constraints for IMonad:</font></div>
<div><br></div><div><div><font face="courier new, monospace">ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs</font></div><div><div><font face="courier new, monospace">ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x</font></div>
<div><font face="courier new, monospace">ghci> :info IMonad</font></div><div><font face="courier new, monospace">class IMonad k m | m -> k where</font></div><div><font face="courier new, monospace"> ireturn :: a x -> m a x</font></div>
</div><div><br></div><div>But when I add </div><div><br></div><div><font face="courier new, monospace">ghci> :{</font></div><div><font face="courier new, monospace">Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where</font></div>
<div><font face="courier new, monospace">Prelude| Nil :: Thrist a '(i,i)</font></div><div><font face="courier new, monospace">Prelude| (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)</font></div>
<div><font face="courier new, monospace">Prelude| :}</font></div><div><span style="font-family:'courier new',monospace"><br></span></div><div><div>and attempt to introduce the instance, I crash:</div></div><div><span style="font-family:'courier new',monospace"><br>
</span></div><div><span style="font-family:'courier new',monospace">ghci> instance IMonad Thrist where ireturn a = a :- Nil</span></div><div><font face="courier new, monospace">ghc: panic! (the 'impossible' happened)</font></div>
<div><font face="courier new, monospace"> (GHC version 7.6.0.20120810 for x86_64-apple-darwin):</font></div><div><font face="courier new, monospace"><span class="Apple-tab-span" style="white-space:pre"> </span>lookupVarEnv_NF: Nothing</font></div>
<div><br></div><div><font face="courier new, monospace">Please report this as a GHC bug: <a href="http://www.haskell.org/ghc/reportabug">http://www.haskell.org/ghc/reportabug</a></font></div></div><div><font face="courier new, monospace"><br>
</font></div><div>Moreover, attempting to compile them in separate modules leads to a different issue. </div><div><br></div><div>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.</div>
<div><br></div><div>Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?</div><div><br></div><div>I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.</div>
<div><br></div><div>-Edward</div>