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