LiftImplies.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StaticPointers #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# OPTIONS_GHC -Wall -fno-warn-orphans #-}

module Main where

import Control.Distributed.Closure
import Data.Typeable
import Unsafe.Coerce (unsafeCoerce)

{-------------------------------------------------------------------------------
  Evil magic to make it possible to define implications of static constraints
-------------------------------------------------------------------------------}

newtype C c a = C { unC :: c => a }

getEvidence :: (forall repc. repc -> a) -> C c a
getEvidence = unsafeCoerce

withEvidence :: C (Static c) a -> (StaticRep c -> a)
withEvidence = unsafeCoerce

data StaticRep c = forall repc. SR {
      staticRepSuper :: !repc
    , staticRepDict  :: !(Closure (Dict c))
    }

withStaticInstance :: forall c. Closure (Dict c) -> Dict (Static c)
withStaticInstance = \cl -> case unclosure cl of
                              Dict -> unC aux1 cl
  where
    aux1 :: C c (Closure (Dict c) -> Dict (Static c))
    aux1 = getEvidence aux2

    aux2 :: repc -> Closure (Dict c) -> Dict (Static c)
    aux2 repc cl = withEvidence (C (Dict :: Dict (Static c))) (SR repc cl)

liftImplies :: forall c c'. Typeable c
            => Closure (Dict c -> Dict c')
            -> Dict (Static c) -> Dict (Static c')
liftImplies f Dict = withStaticInstance (f `cap` (closureDict :: Closure (Dict c)))

{-------------------------------------------------------------------------------
  Test case
-------------------------------------------------------------------------------}

instance Static (Ord Int) where
  closureDict = closure (static Dict)

instance Static (Serializable Int) where
  closureDict = closure (static Dict)

ordImpliesEq :: Dict (Ord a) -> Dict (Eq a)
ordImpliesEq Dict = Dict

cmp :: Dict (Eq a) -> a -> a -> Bool
cmp Dict x y = x == y

test :: Bool
test =
  let ds :: Dict (Static (Ord Int))
      ds = Dict

      ds' :: Dict (Static (Eq Int))
      ds' = liftImplies (closure (static ordImpliesEq)) ds

  in case ds' of
       Dict -> unclosure (closure (static cmp)
         `cap` closureDict
         `cap` (cpure closureDict (1234 :: Int))
         `cap` (cpure closureDict (1234 :: Int))
         )

main :: IO ()
main = print test