faking universal quantification in constraints

[Nicolas Frisby]

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.

I know Dimitrios Vytiniotis is trying to implement these legitimately
in GHC, but I don't know much about that project's status, nor any
documentation indicating how to try it out in GHC HEAD (e.g. what's
the syntax?). Is there a page on the GHC wiki or something to check
that sort of thing?

I wonder how far this Forall_S trick can take me in the interim
towards Vytiniotis' objective functionality when paired with a
(totally safe) class for implication.

> class Implies (ante :: Constraint) (conc :: Constraint) where
>   impliesD :: Dict ante -> Dict conc

Thanks,
Nick