It is both perfectly reasonable and unfortunately useless. :(<div><br></div><div>The problem is that the "more polymorphic" type isn't any more polymorphic, since (ideally) the product kind <font face="courier new, monospace">(a,b)</font> is only inhabited by things of the form <font face="courier new, monospace">'(x,y)</font><font face="arial, helvetica, sans-serif">.</font></div>
<div><br></div><div>The product kind has a single constructor. But there is no way to express this at present that is safe.</div><div><br></div><div>As it stands, I can fake this to an extent in one direction, by writing</div>
<div><font face="courier new, monospace"><br></font></div><div><div><font face="courier new, monospace">{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, TypeFamilies,</font></div>
<div><font face="courier new, monospace"> RankNTypes, TypeOperators, DefaultSignatures, DataKinds,</font></div><div><font face="courier new, monospace"> FlexibleInstances, UndecidableInstances #-}</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">module Kmett where</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">type family Fst (p :: (a,b)) :: a</font></div>
<div><font face="courier new, monospace">type instance Fst '(a,b) = a</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">type family Snd (p :: (a,b)) :: b</font></div>
<div><font face="courier new, monospace">type instance Snd '(a,b) = b</font></div><div><font face="courier new, monospace"><br></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"> (:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =></font></div><div><font face="courier new, monospace"> a ij -> Thrist a '(j,k) -> Thrist a ik</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">irt :: a x -> Thrist a x</font></div><div><font face="courier new, monospace">irt ax = ax :- Nil</font></div><div><br></div>
<div class="gmail_quote">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)</div><div class="gmail_quote">
<br></div><div class="gmail_quote">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.</div>
<div class="gmail_quote"><br></div><div class="gmail_quote">-Edward</div><div class="gmail_quote"><br></div><div class="gmail_quote">On Fri, Aug 31, 2012 at 1:00 PM, Simon Peyton-Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span> wrote:</div>
<div class="gmail_quote"><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><div class="im">
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">Same question. Do you expect the code below to type-check? I have stripped it down to essentials. Currently it’s rejected with
<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"> Couldn't match type `a' with '(,) k k1 b0 d0<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">And that seems reasonable, doesn’t it? After all, in the defn of bidStar, (:*) returns a value of type
<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d"> Star x y ‘(a,c) ‘(b,d)<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">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. <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">I must be confused.<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>
</div><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">module Product where<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">data Star :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * 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"> (:*) :: x a b -> y c d -> Star x y '(a,c) '(b,d)<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">bidStar :: Star T T a a<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">bidStar = bidT :* bidT<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">data T a b = MkT<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">bidT :: T a a<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1f497d">bidT = MkT<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"><u></u> <u></u></span></p>
</div><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""> Edward Kmett [mailto:<a href="mailto:ekmett@gmail.com" target="_blank">ekmett@gmail.com</a>]
<br></span></p><div class="im">
<b>Sent:</b> 31 August 2012 13:45<br>
<b>To:</b> Simon Peyton-Jones<br>
<b>Cc:</b> <a href="mailto:glasgow-haskell-users@haskell.org" target="_blank">glasgow-haskell-users@haskell.org</a><br>
</div><b>Subject:</b> Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?<u></u><u></u><p></p>
</div>
</div><div class="im">
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">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. =( <u></u><u></u></p>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<div>
<p class="MsoNormal">For instance, there doesn't even seem to be a way to make the following code compile, either.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><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"">{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">module Product 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"">import Prelude hiding (id,(.))</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 Category k where</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> id :: k a a</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> (.) :: k b c -> k a b -> k a c</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"">data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)</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 (Category x, Category y) => Category (x * y) where</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> id = id :* id</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New""> (xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<div>
<p class="MsoNormal">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.<u></u><u></u></p>
</div>
</div>
</div>
</div>
</div></div>
</div>
</div>
</blockquote></div><br></div>