[Haskell] Re: "Never" GADT Function?
lennart at augustsson.net
Sat Jan 8 05:29:51 EST 2005
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.
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
> Inaccessible case alternative: Can't match types `Bool' and `Char'
> When checking the pattern: BoolT
> In the definition of `neverT': neverT BoolT = "hello"
More information about the Haskell