Hi Simon,<br><br>For instance:<br><br><blockquote style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex; font-family: courier new,monospace;" class="gmail_quote">data Su n<br>data Fin n where FSu :: Fin n -> Fin (Su n)<br>
-- equivalent to data Fin n = forall m. n ~ Su m => FSu (Fin m)<br><br>data a :=: b where Refl :: a :=: a<br><br>type instance Rep (Fin n) = forall m. (n :=: Su m, Fin m)<br></blockquote><br>But I think I found the answer in the meantime: this would quickly leave GHC trying to prove things such as (forall m. ... ~ forall m1. ...), which I guess is undecidable in general.<br>
<br><br>Cheers,<br>Pedro<br><br><div class="gmail_quote">2011/4/4 Simon Peyton-Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>></span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div link="blue" vlink="purple" lang="EN-GB">
<div>
<p class="MsoNormal"><span style="font-size:11.0pt;color:#1F497D">Can you give an example of what you’d like to write, but can’t?<br>
<br>
Simon</span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;color:#1F497D"> </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 style="font-size:10.0pt" lang="EN-US">From:</span></b><span style="font-size:10.0pt" lang="EN-US"> <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>José Pedro Magalhães<br>
<b>Sent:</b> 04 April 2011 10:53<br>
<b>To:</b> GHC users<br>
<b>Cc:</b> Steven Keuchel<br>
<b>Subject:</b> Re: [Haskell] Polymorphic types in RHS of type instances</span></p>
</div>
</div><div><div></div><div class="h5">
<p class="MsoNormal"> </p>
<p class="MsoNormal" style="margin-bottom:12.0pt">Hi,<br>
<br>
[Moving to <a href="mailto:glasgow-haskell-users@haskell.org" target="_blank">glasgow-haskell-users@haskell.org</a>]<br>
<br>
I would also like to know the answer to this question. While I can imagine it has something to do with type checking/inference, it is not immediately clear to me where the problem lies.<br>
<br>
<br>
Thanks,<br>
Pedro</p>
<div>
<p class="MsoNormal">On Sat, Feb 5, 2011 at 12:25, Steven Keuchel <<a href="mailto:steven.keuchel@gmail.com" target="_blank">steven.keuchel@gmail.com</a>> wrote:</p>
<p class="MsoNormal">Hi list,<br>
<br>
I was wondering why GHC doesn't allow usage of polymorphic types in<br>
the right-hand side of type instance declarations for type families.<br>
The GHC user guide states: "The right-hand side of a type instance<br>
must be a monotype (i.e., it may not include foralls) [...]", but it<br>
doesn't state the reason.<br>
<br>
I stumbled upon this limitation when I was trying to generically<br>
calculate Johann's and Ghani's interpreter (transformers) for nested<br>
data types from their "Initial Algebra Semantics is Enough!" paper.<br>
<br>
Cheers,<br>
Steven<br>
<br>
_______________________________________________<br>
Haskell mailing list<br>
<a href="mailto:Haskell@haskell.org" target="_blank">Haskell@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell" target="_blank">http://www.haskell.org/mailman/listinfo/haskell</a></p>
</div>
<p class="MsoNormal"> </p>
</div></div></div>
</div>
</div>
</blockquote></div><br>