[Haskell] Re: "Never" GADT Function?

[Simon Peyton-Jones]

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 at haskell.org [mailto:haskell-bounces at haskell.org]
On Behalf Of Lennart
| Augustsson
| Sent: 08 January 2005 10:30
| To: Ashley Yakeley
| Cc: haskell at 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 at sf0.comp.nus.edu.sg>,
| >  Martin Sulzmann <sulzmann at 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 at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell