[Haskell] Re: "Never" GADT Function?

Ashley Yakeley ashley at semantic.org
Sat Jan 8 04:08:00 EST 2005

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"

Ashley Yakeley, Seattle WA

Ashley Yakeley, Seattle WA

More information about the Haskell mailing list