[Haskell] Re: "Never" GADT Function?

[Lennart Augustsson]

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"
>