faking universal quantification in constraints

[Nicolas Frisby]

I built a (really ugly) dictionary for (Int ~ Char) using
Data.Constraints.Forall. I'm fairly confident it could be generalized
to a polymorphic coercion (a ~ b).

  http://hpaste.org/67180

I cheated with overlapping instances, but you left me no choice ;).
Anyone who pulls this kind of stunt is definitely trying to subvert
it; so I vote "trustworthy".

I'm adopting Data.Constraints.Forall for my local experimentation.
Thanks for pointing it out.

On Tue, Apr 17, 2012 at 4:15 PM, Nicolas Frisby
<nicolas.frisby at gmail.com> wrote:
> Great! I'll take a whack at it ;)
>
> On Tue, Apr 17, 2012 at 4:07 PM, Edward Kmett <ekmett at gmail.com> wrote:
>>
>>
>> On Mon, Apr 16, 2012 at 6:57 PM, Nicolas Frisby <nicolas.frisby at gmail.com>
>> wrote:
>>>
>>> I'm simulating skolem variables in order to fake universal
>>> quantification in constraints via unsafeCoerce.
>>>
>>>  http://hpaste.org/67121
>>>
>>> I'm not familiar with various categories of types from the run-time's
>>> perspective, but I'd be surprised if there were NOT a way to use this
>>> code to create run-time errors.
>>>
>>> Is there a way to make it safer? Perhaps by making Skolem act more
>>> like GHC's Any type? Or perhaps like the -> type? I'd like to learn
>>> about the varieties of types from the run-time's perspective.
>>
>>
>> FWIW- I have a version of this concept packaged up in the constraints
>> package.
>>
>> I had a small example that abused flexible instances and MPTCs to cause the
>> single Skolem version of my code to fail.
>>
>> However, when I refined it to use two Skolem variables I wasn't able to
>> derive sufficient Oleggery to break it. That said, an absence of a
>> counter-example isn't a proof that it can't exist.
>>
>> http://hackage.haskell.org/packages/archive/constraints/0.3/doc/html/src/Data-Constraint-Forall.html
>>