-- Anyone have know how unsafe this is (in terms of run-time errors)?

-- Is there a way to make it safer (e.g. GHC's Any type)?

-- Godspeed, Dimitrios.

{-# LANGUAGE ConstraintKinds, RankNTypes, GADTs, ScopedTypeVariables,
  KindSignatures, FlexibleInstances, UndecidableInstances, EmptyDataDecls #-}

{-# LANGUAGE MultiParamTypeClasses #-}

module Forall_S (Dict(..), Forall_S(..)) where

import GHC.Prim (Constraint)
import Unsafe.Coerce (unsafeCoerce)

data Dict :: Constraint -> * where
  Dict :: con => Dict con

class Forall_S (con :: * -> Constraint) where
  forall_S :: ((forall a. Dict (con a)) -> x) -> x

-- we fake universal quantification using an approximation of a skolem constant
-- (i.e. Skolem is not exported)
data Skolem
instance con Skolem => Forall_S con where
  forall_S k = k (generalise Dict) where
    generalise :: Dict (con Skolem) -> Dict (con a)
    generalise = unsafeCoerce