faking universal quantification in constraints

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
-- 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