<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">2014-12-09 2:35 GMT+01:00 Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span>:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="word-wrap:break-word"><div>While it's true that Maybe's kind is (* -> *), there still may be a better answer to your question, which asks, "Is there a way to get a polykinded promoted type?" Maybe isn't polykinded, but it's also not promoted. With</div><div><br></div><div>data Proxy a = P</div><div><br></div><div>we get (Proxy :: k -> *). But that's not promoted either. On the other hand we have ('Just :: k -> Maybe k), which is promoted and polykinded, but maybe not what you want.</div><div><br></div><div>Does this help?</div></div></blockquote></div><br>Hello,<br><br>In fact my problem occurs when I try to describe (Iso)morphisms:<br><div style="margin-left:40px">type Cons1 (e :: k1) (n :: k2) = Product e n<br>type Nil1 = Void<br><br>type Cons2 e n = Just (Product e n)<br>type Nil2 = Nothing<br><br>data List3 a = Nil3 | Cons3 a (List3 a)<br><br>type family List1_List2 a where<br>  List1_List2 (Cons1 a b) = Cons2 a (List1_List2 b)<br>  List1_List2 Nil1 = Nil2<br><br>type family List2_List1 a where<br>  List2_List1 (Cons2 a b) = Cons1 a (List2_List1 b)<br>  List2_List1 Nil2 = Nil1<br><br>type family List2_List3 a where<br>  List2_List3 (Cons2 a b) = Cons3 a (List2_List3 b)<br>  List2_List3 Nil2 = Nil3<br><br>type family List3_List2 a where<br>  List3_List2 (Cons3 a b) = Cons2 a (List3_List2 b)<br>  List3_List2 Nil3 = Nil2<br><br>type List1_List3 a = List2_List3 (List1_List2 a)<br>type List3_List1 a = List2_List1 (List3_List2 a)<br></div><br>There is an Isomorphism between List1 and List2 (List1_List2 (List2_List1 a) == a and List2_List1 (List1_List2 a) == a) but not between List3 and the others due to it's * kind.<br><br></div><div class="gmail_extra">Thanks,<br></div><div class="gmail_extra">Regards.<br></div></div>