{-# OPTIONS -fglasgow-exts #-}
module Main where
import Data.IORef
data T a where Li:: Int -> T Int Lb:: Bool -> T Bool La:: a -> T a
writeInt:: T a -> IORef a -> IO () writeInt v ref = case v of ~(Li x) -> writeIORef ref (1::Int)
readBool:: T a -> IORef a -> IO () readBool v ref = case v of ~(Lb x) -> readIORef ref >>= (print . not)
tt::T a -> IO () tt v = case v of ~(Li x) -> print "OK"
main = do tt (La undefined) ref <- newIORef undefined writeInt (La undefined) ref readBool (La undefined) ref
This code is more intricate than data Eq a b where Refl :: Eq a a coerce :: Eq a b -> a -> b coerce ~Refl x = x but I think it amounts to exactly the same thing: ref and x are forced to a particular type witnessed by the GADT. But I think that something still can be squeezed out, strictness is not absolutely necessary (see upcoming mail on this thread). Regards, apfelmus