<br><br><div class="gmail_quote">On Thu, Apr 10, 2008 at 4:20 AM, Manuel M T Chakravarty <<a href="mailto:chak@cse.unsw.edu.au">chak@cse.unsw.edu.au</a>> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
the five signatures<br>
<br>
forall a. S a<br>
forall b. S b<br>
forall a b. S (a, b)<br>
Int<br>
S Int<br>
</blockquote><div><br>By alpha-convertible I mean the usual thing from lambda calculus, they are identical modulo the names of bound variables.<br>So only the first two are alpha-convertible to each other.<br><br>If you involve any kind of reduction the equivalence test is no longer trivial.<br>
<br>All I'm asking for really, is to be able to paste in the type that was inferred as the signature, without the compiler complaining.<br><br> -- Lennart<br><br></div></div><br>