Ticket #4139: GADTNonExhaustive.hs

File GADTNonExhaustive.hs, 1.4 KB (added by blarsen, 4 years ago)

A simple evaluator that demonstrates spurious non-exhaustive pattern match warnings

Line 
1{-# LANGUAGE GADTs, KindSignatures #-}
2{-# OPTIONS -Wall #-}
3module GADTNonExhaustive where
4
5data Expr :: * -> * where
6  Const :: Const a -> Expr a
7  Pair  :: Expr a -> Expr b -> Expr (a, b)
8  Fst   :: Expr (a, b) -> Expr a
9  Snd   :: Expr (a, b) -> Expr b
10
11data Const :: * -> * where
12  ConstInt :: Int -> Const Int
13  ConstFloat :: Float -> Const Float
14
15eval :: Expr a -> a
16eval expr =
17  case expr of
18    Const c -> evalConst c
19    Pair l r -> evalPair l r
20    Fst e -> evalFst e
21    Snd e -> evalSnd e
22
23evalConst :: Const a -> a
24evalConst c =
25  case c of
26    ConstInt i -> i
27    ConstFloat f -> f
28
29evalPair :: Expr a -> Expr b -> (a, b)
30evalPair l r = (eval l, eval r)
31
32evalFst :: Expr (a, b) -> a
33evalFst expr =
34  case expr of
35    -- The `Const' case is in fact impossible, as any Const
36    -- constructor matched against is type-incorrect.  However, GHC
37    -- warns about non-exhaustive pattern matches if the following
38    -- line is commented.  This behavior is observed with 6.10.4,
39    -- 6.12.1, 6.12.2, and 6.12.3.  I have not tested other versions.
40    Const _c -> error "Impossible!"
41    Pair l _r -> eval l
42    Fst e -> fst $ evalFst e
43    Snd e -> fst $ evalSnd e
44
45evalSnd :: Expr (a, b) -> b
46evalSnd expr =
47  case expr of
48    -- Same deal here as in evalFst.
49    Const _c -> error "Impossible!"
50    Pair _l r -> eval r
51    Fst e -> snd $ evalFst e
52    Snd e -> snd $ evalSnd e