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. =( <div><br></div><div><div>For instance, there doesn't even seem to be a way to make the following code compile, either.</div>
<div><br></div><div><br></div><div><div><font face="courier new, monospace">{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}</font></div><div><font face="courier new, monospace">module Product where</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">import Prelude hiding (id,(.))</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">class Category k where</font></div>
<div><font face="courier new, monospace"> id :: k a a</font></div><div><font face="courier new, monospace"> (.) :: k b c -> k a b -> k a c</font></div><div><font face="courier new, monospace"><br></font></div><div>
<font face="courier new, monospace">data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where</font></div><div><font face="courier new, monospace"> (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">instance (Category x, Category y) => Category (x * y) where</font></div><div><font face="courier new, monospace"> id = id :* id</font></div>
<div><font face="courier new, monospace"> (xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)</font></div><div><br></div><div><div>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.</div>
<div></div></div><div><br></div><div>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? </div><div><br></div><div>e.g. should</div><div><br></div>
<div>class Foo (m :: k -> *)</div><div><br></div><div>always be</div><div><br></div><div>class Foo (m :: k -> *) | m -> k</div><div><br></div><div>?</div><div><br></div><div>Honest question. I can't come up with a scenario, but you might have one I don't know.</div>
<div><br></div><div>-Edward</div><br><div class="gmail_quote">On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div lang="EN-GB" link="blue" vlink="purple">
<div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">With the code below, I get this error message with HEAD. And that looks right to me, no?<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">The current 7.6 branch gives the same message printed less prettily.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">If I replace the defn of irt with<u></u><u></u></span></p>
<p class="MsoNormal" style="text-indent:36.0pt"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">irt :: a '(i,j) -> Thrist a '(i,j)<u></u><u></u></span></p>
<p class="MsoNormal" style="text-indent:36.0pt"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">irt ax = ax :- Nil<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">then it typechecks.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">Simon<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">Knett.hs:20:10:<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"> Couldn't match type `x' with '(i0, k0)<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"> `x' is a rigid type variable bound by<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"> the type signature for irt :: a x -> Thrist k a x at Knett.hs:19:8<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"> Expected type: Thrist k a x<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"> Actual type: Thrist k a '(i0, k0)<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"> In the expression: ax :- Nil<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"> In an equation for `irt': irt ax = ax :- Nil<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">simonpj@cam-05-unx:~/tmp$<u></u><u></u></span></p><div class="im">
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds,
<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"> RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"> FlexibleInstances, UndecidableInstances #-}<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
</div><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">module Knett where<u></u><u></u></span></p><div class="im">
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">class IMonad (m :: (k -> *) -> k -> *) | m -> k where
<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"> ireturn :: a x -> m a x<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
</div><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">infixr 5 :-<u></u><u></u></span></p><div class="im">
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">data Thrist :: ((i,i) -> *) -> (i,i) -> * where<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"> Nil :: Thrist a '(i,i)<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"> (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
</div><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">-- instance IMonad Thrist where<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">-- ireturn a = a :- Nil<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">irt :: a x -> Thrist a x<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">irt ax = ax :- Nil<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #b5c4df 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US" style="font-size:10.0pt;font-family:"Tahoma","sans-serif"">From:</span></b><span lang="EN-US" style="font-size:10.0pt;font-family:"Tahoma","sans-serif""> <a href="mailto:glasgow-haskell-users-bounces@haskell.org" target="_blank">glasgow-haskell-users-bounces@haskell.org</a> [mailto:<a href="mailto:glasgow-haskell-users-bounces@haskell.org" target="_blank">glasgow-haskell-users-bounces@haskell.org</a>]
<b>On Behalf Of </b>Edward Kmett<br>
<b>Sent:</b> 31 August 2012 03:38<br>
<b>To:</b> <a href="mailto:glasgow-haskell-users@haskell.org" target="_blank">glasgow-haskell-users@haskell.org</a><br>
<b>Subject:</b> PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?<u></u><u></u></span></p>
</div>
</div><div><div class="h5">
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<p class="MsoNormal">If I define the following<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">module Indexed.Test where</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">class IMonad (m :: (k -> *) -> k -> *) where </span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> ireturn :: a x -> m a x</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">infixr 5 :-</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">data Thrist :: ((i,i) -> *) -> (i,i) -> * where</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> Nil :: Thrist a '(i,i)</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">instance IMonad Thrist where</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> ireturn a = a :- Nil</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Arial","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</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">class IMonad k m where</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> ireturn :: a x -> m a x</span><u></u><u></u></p>
</div>
</div>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Arial","sans-serif"">However, there doesn't appear to be a way to say that the kind k should be determined by m. </span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Arial","sans-serif"">I tried doing:</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">class IMonad (m :: (k -> *) -> k -> *) | m -> k where </span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> ireturn :: a x -> m a x</span><u></u><u></u></p>
</div>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Arial","sans-serif"">Surprisingly (to me) this compiles and generates the correct constraints for IMonad:</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs</span><u></u><u></u></p>
</div>
<div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">ghci> :info IMonad</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">class IMonad k m | m -> k where</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> ireturn :: a x -> m a x</span><u></u><u></u></p>
</div>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">But when I add <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">ghci> :{</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">Prelude| Nil :: Thrist a '(i,i)</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">Prelude| (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">Prelude| :}</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<div>
<p class="MsoNormal">and attempt to introduce the instance, I crash:<u></u><u></u></p>
</div>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">ghci> instance IMonad Thrist where ireturn a = a :- Nil</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">ghc: panic! (the 'impossible' happened)</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> (GHC version 7.6.0.20120810 for x86_64-apple-darwin):</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span><span style="font-family:"Courier New"">
</span></span><span style="font-family:"Courier New"">lookupVarEnv_NF: Nothing</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">Please report this as a GHC bug: <a href="http://www.haskell.org/ghc/reportabug" target="_blank">http://www.haskell.org/ghc/reportabug</a></span><u></u><u></u></p>
</div>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Moreover, attempting to compile them in separate modules leads to a different issue. <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">-Edward<u></u><u></u></p>
</div>
</div></div></div>
</div>
</div>
</blockquote></div><br></div></div>