{-# OPTIONS -fglasgow-exts #-}

-- The illustration of the unsoundness of GADT that existed in their
-- very first implementation in GHC (Sep 2004). 
-- That implementation supported irrefutable pattern matching with
-- GADT (so GADT could look just like the regular ADT).
-- That leads to unsoundness as this code demonstrates.
-- Using GHC HEAD as of Sep 2004, the code typechecked, compiled, 
-- and, when run, gave "Segmentation fault".
--
-- The code was e-mailed to a few people on
-- Mon, 13 Sep 2004 14:33:07 -0700 (PDT).
--
-- Simon Peyton-Jones has fixed the problem almost immediately, by
-- prohibiting irrefutable pattern-match with GADTs.
-- That means that GADTs are NOT the generalization of the ordinary
-- algebraic data types: ADT support irrefutable pattern-match but
-- GADTs do not.

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