You should be able to even write neverT (BoolT x) = x neverT (IntT x) = False -- neverT = undefined -- also possible cause as a temporary type assumptions we'll add in Bool=Char (or Int=Char in case of the second clause which effectively equals False, the always false constraint. Note that under the False assumption we can give any type to the result expression. I don't know whether this is supported in GHC, at least, it works in Chameleon (which also supports GADTs and a bit more). Here's the Chameleon code. data T a = (a=Bool) => BoolT a | (a=Int) => IntT a neverT :: T Char -> x neverT (BoolT x) = x neverT (IntT x) = False Chameleon is available via http://www.comp.nus.edu.sg/~sulzmann/chameleon (look for Existentially Quantified Type Classes) A new update is coming soon. Martin Ashley Yakeley writes:

OK, so I've been playing around with GADTs in the CVS GHC. Consider this:

data T a where BoolT :: T Bool IntT :: T Int

neverT :: T Char -> x

Is it possible to write neverT without using undefined? Such functions are occasionally useful, especially when GADTs are being used as type witnesses.

Then again, I suppose it's the same situation for types with no constructors.

-- Ashley Yakeley, Seattle WA

_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell