GHC deliberately rejects programs with unreachable code, as Ashley says, because a) they often are programmer errors b) I can't think of a time when they'd be useful. I don't see what's wrong with neverT :: T Char -> x neverT = error "urk" After all, since you can't construct a value of type (T Char) there's not much point in pattern-matching on it. Simon | -----Original Message----- | From: haskell-bounces@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of Lennart | Augustsson | Sent: 08 January 2005 10:30 | To: Ashley Yakeley | Cc: haskell@haskell.org | Subject: Re: [Haskell] Re: "Never" GADT Function? | | Well, this compiles: | | data T a where | BoolT :: T Bool | IntT :: T Int | | neverT' :: T a -> x | neverT' BoolT = error "Bool" | neverT' IntT = error "Int" | | neverT :: T Char -> x | neverT = neverT' | | But it uses error for the unreachable cases, maybe not what you want. | | -- Lennart | | Ashley Yakeley wrote: | > In article <16863.36246.132716.788213@sf0.comp.nus.edu.sg>, | > Martin Sulzmann <sulzmann@comp.nus.edu.sg> wrote: | > | > You should be able to even write | > | > neverT (BoolT x) = x | > neverT (IntT x) = False | > | > Actually I didn't put in any arguments to my constructors. Apart from | > that I agree: this should compile, but doesn't: | > | > data T a where | > BoolT :: T Bool | > IntT :: T Int | > | > neverT :: T Char -> x | > neverT BoolT = "hello" | > neverT IntT = 37 | > | > Pick.hs:11:9: | > Inaccessible case alternative: Can't match types `Bool' and `Char' | > When checking the pattern: BoolT | > In the definition of `neverT': neverT BoolT = "hello" | > | | _______________________________________________ | Haskell mailing list | Haskell@haskell.org | http://www.haskell.org/mailman/listinfo/haskell