[Haskell-cafe] Re: irrefutable patterns for existential types / GADTs

[apfelmus at quantentunnel.de]

>> {-# 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