GADT instance

1.hs

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
module Test where

import Data.Singletons
import Data.Singletons.TH
import Foreign
import Foreign.Storable 

import System.IO.Unsafe (unsafePerformIO)
import Unsafe.Coerce

data M = A | B deriving (Eq, Show)

genSingletons [''M]

-- | Foreign type
data F = F M (Either Int String)

typeF :: F -> M
typeF (F x _) = x

-- | Raw pointer of a haskell side
data SPtr

-- | foreign data
newtype S a = S { unS :: Ptr (V a) }

uns :: S a -> Ptr SPtr
uns = castPtr . unS

s :: Ptr SPtr -> S a
s = S . castPtr

-- | unknown type in runtime
data SomeS = SomeS (forall (a :: M) . S a)

withSomeS :: SomeS -> (forall a . S a -> b) -> b
withSomeS = undefined

typeOf :: S a -> M
typeOf = unsafePerformIO . fmap typeF . deRefStablePtr . castPtrToStablePtr . castPtr . unS


cast :: M -> SomeS -> S b
cast ty (SomeS z)
  | ty == typeOf z = s . uns $ z
  | otherwise = error "cast: Type failure."


class MkVal a b | a -> b where
  mkVal :: a -> IO (S b)

instance MkVal Int A where
  mkVal i = fmap (S . castPtr . castStablePtrToPtr) $ newStablePtr (F A (Left i))

instance MkVal String B where
  mkVal s = fmap (S . castPtr . castStablePtrToPtr) $ newStablePtr (F B (Right s))

data V :: M -> * where
  V1 :: Int -> V A
  V2 :: String -> V B

instance Storable (V a) where
  sizeOf _ = 0
  alignment _ = 0
  poke = error "not interesting"
  peek s  = case typeOf (S s) of
    A -> do (F _ (Left i)) <- deRefStablePtr (castPtrToStablePtr  $ castPtr s) 
            return $ unsafeCoerce $ V1 i
    B -> do (F _ (Right s)) <- deRefStablePtr (castPtrToStablePtr $ castPtr s) 
            return $ unsafeCoerce $ V2 s

foo :: S a -> V a
foo = unsafePerformIO . peek . unS

{-
test =
   inner . SomeS =<< mkVal 1
  where 
   inner z = do
     let y = cast A z
     in case foo s of
          T1 _ (
	  -}