<div dir="ltr">Hello,<div><br></div><div>Sorry to chime in, but Richard: could you expand a little bit on what your ongoing work there consists in and what will be possible that wasn't before? You got me quite curious here.</div><div><br></div><div>Thanks!</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jun 25, 2015 at 2:31 PM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Косырев,<br>
<br>
Promoting type/data families isn't a matter of safety, exactly, but a matter of drastically altering the internal type system of GHC to support such things. Happily, my research is all about doing so. You can expect your first example `class C1 a (b :: D I)` to work in GHC 7.12. If you're overly interested, my work is happening at <a href="http://github.com/goldfirere/ghc" rel="noreferrer" target="_blank">github.com/goldfirere/ghc</a> on the `nokinds` branch. But there won't be much (any?) action there for a little while as I'm working on anther project for the next few weeks.<br>
<br>
Your second example, though, is ill-formed: you can't have a type variable of kind `D`, as `D`, by itself, isn't a kind. You could say this, if you wanted, though:<br>
<br>
> class C1 a (b :: D a)<br>
<br>
Do you have an use case for this? I'm always curious to see how Haskellers want to use these advanced features!<br>
<br>
Thanks,<br>
Richard<br>
<div class="HOEnZb"><div class="h5"><br>
On Jun 25, 2015, at 2:44 AM, Kosyrev Serge <_<a href="mailto:deepfire@feelingofgreen.ru">deepfire@feelingofgreen.ru</a>> wrote:<br>
<br>
> Good day!<br>
><br>
> DataKinds doesn't allow promotion of type/data families.<br>
><br>
> However, in the specific case of associated data families -- aren't<br>
> they constrained more, and sufficiently so that the following, for example,<br>
> could be made to work without stepping into dangerous territories:<br>
><br>
> --<br>
> {-# LANGUAGE DataKinds #-}<br>
> {-# LANGUAGE KindSignatures #-}<br>
> {-# LANGUAGE TypeFamilies #-}<br>
> {-# LANGUAGE UnicodeSyntax #-}<br>
><br>
> module M where<br>
><br>
> class C a where<br>
>    data D a ∷ *<br>
><br>
> data I<br>
><br>
> instance C I where<br>
>    data D I<br>
><br>
> class C1 a (b ∷ D I) where<br>
><br>
> -- ..or, maybe, perhaps even the following:<br>
><br>
> class C1 a (b ∷ D) where<br>
><br>
> --<br>
> respectfully,<br>
> Косырев Серёга<br>
> _______________________________________________<br>
> Haskell-Cafe mailing list<br>
> <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
><br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature">Alp Mestanogullari</div>
</div>