blob: b6c0bf572e803c6de90ab1268986de6f73f55a32 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
{-# LANGUAGE GADTs #-}
module ShouldCompile where
data Rep t where
Rint :: Rep Int
Rchar :: Rep Char
Runit :: Rep ()
Rpair :: Rep a -> Rep b -> Rep (a,b)
Rsum :: Rep a -> Rep b -> Rep (Either a b)
Rcon :: String -> Rep t -> Rep t
data Equal a b where
Eq :: Equal c c
test :: Rep a -> Rep b -> Maybe (Equal a b)
test Rint Rint = return Eq
test Rchar Rchar = return Eq
test Runit Runit = return Eq
test (Rpair x y) (Rpair a b)
= do { Eq <- test x a; Eq <- test y b; return Eq }
test (Rsum x y) (Rsum a b)
= do { Eq <- test x a; Eq <- test y b; return Eq }
test (Rcon s1 x) (Rcon s2 y)
= if s1==s2 then test x y else Nothing
test _ _ = Nothing
f :: Equal a b -> a -> b -> b
f Eq x y = x
|
