<div><br></div><br><div class="gmail_quote">On Mon, Apr 16, 2012 at 6:57 PM, Nicolas Frisby <span dir="ltr">&lt;<a href="mailto:nicolas.frisby@gmail.com">nicolas.frisby@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I&#39;m simulating skolem variables in order to fake universal<br>
quantification in constraints via unsafeCoerce.<br>
<br>
 ¬†<a href="http://hpaste.org/67121" target="_blank">http://hpaste.org/67121</a><br>
<br>
I&#39;m not familiar with various categories of types from the run-time&#39;s<br>
perspective, but I&#39;d be surprised if there were NOT a way to use this<br>
code to create run-time errors.<br>
<br>
Is there a way to make it safer? Perhaps by making Skolem act more<br>
like GHC&#39;s Any type? Or perhaps like the -&gt; type? I&#39;d like to learn<br>
about the varieties of types from the run-time&#39;s perspective.<br></blockquote><div><br></div><div>FWIW- I have a version of this concept packaged up in the constraints package.<div><br></div><div>I had a small example that abused flexible instances and MPTCs to cause the single Skolem version of my code to fail.</div>
<div><br></div><div>However, when I refined it to use two Skolem variables I wasn&#39;t able to derive sufficient Oleggery to break it.¬†That said, an absence of a counter-example isn&#39;t a proof that it can&#39;t exist.</div>
<div><br></div><div><a href="http://hackage.haskell.org/packages/archive/constraints/0.3/doc/html/src/Data-Constraint-Forall.html">http://hackage.haskell.org/packages/archive/constraints/0.3/doc/html/src/Data-Constraint-Forall.html</a></div>
<div><br></div></div></div>