Modify a couple of error messages slightly
[ghc.git] / testsuite / tests / gadt / doaitse.hs
1 {-# LANGUAGE GADTs, ExistentialQuantification, ScopedTypeVariables,
2 RankNTypes #-}
3
4 -- Here's an example from Doaitse Swiestra (Sept 06)
5 -- which requires use of scoped type variables
6 --
7 -- It's a cut-down version of a larger program
8 --
9 -- It's also one which was sensitive to syntactic order
10 -- in GHC 6.4; but not in 6.6
11
12 module ShouldCompile where
13
14 data Exists f = forall a . Exists (f a)
15
16 data Ref env a where
17 Zero :: Ref (a,env') a
18 Suc :: Ref env' a -> Ref (x,env') a
19
20 data Find env final = Find (forall a . Ref env a -> Maybe (Ref final a))
21
22 data Equal a b where
23 Eq :: Equal a a
24
25 sym :: Equal a b -> Equal b a
26 sym Eq = Eq
27
28 match' :: Ref env' a -> Ref env'' a -> Bool
29 match' _ _ = True
30
31 match :: Ref env a -> Ref env b -> Maybe (Equal a b)
32 match Zero Zero = Just Eq
33 match (Suc x)(Suc y) = match x y
34 match _ _ = Nothing
35
36 -- Notice the essential type sig for the argument to Exists
37 f1 :: forall env. (Exists (Ref env)) -> Exists (Find env)
38 f1 (Exists (ref1 :: Ref env b))
39 = Exists ( Find (\ ref2 -> case match ref2 ref1 of
40 Just Eq -> Just Zero
41 _ -> Nothing
42 ):: Find env (b,())
43 )
44
45
46 -- same as 'f1' except that 'ref1' and 'ref2' are swapped in the
47 -- application of 'match'
48 f2 :: forall env. (Exists (Ref env)) -> Exists (Find env)
49 f2 (Exists (ref1 :: Ref env b))
50 = Exists (Find (\ ref2 -> case match ref1 ref2 of
51 Just Eq -> Just Zero
52 _ -> Nothing
53 ) :: Find env (b,())
54 )
55