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"