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

[oleg at pobox.com]

It seems that irrefutable pattern match with existentials is safe. The
fact that irrefutable pattern match with GADT is unsafe has been
demonstrated back in September 2004.

Let us consider the following regular existential data type

> data TFoo where
>    Foo :: Show a => a -> TFoo
>    Bar :: Int -> TFoo

Despite the 'where' syntax, it is NOT GADT; it is just a regular data
type. We can write

> test_foo vf = case vf of ~(Foo x) -> body

Now, if 'x' does not occur in `body', we could have just as well written 
	test_foo vf = body
If `x' does occur in body and the scrutinee is not of the form `Foo',
then 'x' is undefined, and so 'body' bottoms out when it demands the
value of 'x'. No surprise, and no concern here.

Let is now consider a GADT

> data GTFoo a where
>     GFoo :: GTFoo Int
>     GBar :: GTFoo Bool
>
> test_gfoo :: GTFoo a -> a
> test_gfoo vf = case vf of GFoo -> (1::Int)


It can be faithfully emulated as follows

> -- the data constructors Em_GFoo and Em_GBar must be hidden!
> data EmulateGTFoo a = Em_GFoo | Em_GBar
>
> em_gfoo :: EmulateGTFoo Int
> em_gfoo = Em_GFoo
> em_gbar :: EmulateGTFoo Bool
> em_gbar = Em_GBar

The constructors Em_GFoo and Em_GBar should be hidden. The user should
use `smart' constructors em_gfoo and em_gbar, which not only set the
correct type (Int vs Bool) but also produce the witness, viz. Em_GFoo
or Em_GBar.

Now, the test_gfoo function should be written as

> tesd_emulate_gfoo :: EmulateGTFoo a -> a 
> tesd_emulate_gfoo vf = case vf of Em_GFoo -> unsafeCoerce (1::Int)

So, we test for evidence, Em_GFoo, and if it is presented, we proceed
with unsafeCoerce, which generalizes Int to the desired type 'a'. We
know this generalization is safe because the evidence Em_GFoo told us
that 'a' was really Int. The similarity with Dynamics is uncanny.

Now, had we used an irrefutable match instead, we would have
proceeded with unsafeCoerce without checking for the evidence. 

The following code, written back in Sep 13, 2004, shows that the above
is not an empty concern. The code did indeed typecheck, with the
version of GHC (tidt-branch CVS branch) that existed at that
time. Running the code produced the result one'd expect when reading
an Int as a Bool. I think the code below was the reason GHC prohibited
irrefutable GADT pattern matching since.


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