blob: 02237b515497e2d8c2b8db7dc833f6d6976a3bd0 (
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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
{-# LANGUAGE GADTs, ExistentialQuantification, ScopedTypeVariables,
RankNTypes #-}
-- Here's an example from Doaitse Swiestra (Sept 06)
-- which requires use of scoped type variables
--
-- It's a cut-down version of a larger program
--
-- It's also one which was sensitive to syntactic order
-- in GHC 6.4; but not in 6.6
module ShouldCompile where
data Exists f = forall a . Exists (f a)
data Ref env a where
Zero :: Ref (a,env') a
Suc :: Ref env' a -> Ref (x,env') a
data Find env final = Find (forall a . Ref env a -> Maybe (Ref final a))
data Equal a b where
Eq :: Equal a a
sym :: Equal a b -> Equal b a
sym Eq = Eq
match' :: Ref env' a -> Ref env'' a -> Bool
match' _ _ = True
match :: Ref env a -> Ref env b -> Maybe (Equal a b)
match Zero Zero = Just Eq
match (Suc x)(Suc y) = match x y
match _ _ = Nothing
-- Notice the essential type sig for the argument to Exists
f1 :: forall env. (Exists (Ref env)) -> Exists (Find env)
f1 (Exists (ref1 :: Ref env b))
= Exists ( Find (\ ref2 -> case match ref2 ref1 of
Just Eq -> Just Zero
_ -> Nothing
):: Find env (b,())
)
-- same as 'f1' except that 'ref1' and 'ref2' are swapped in the
-- application of 'match'
f2 :: forall env. (Exists (Ref env)) -> Exists (Find env)
f2 (Exists (ref1 :: Ref env b))
= Exists (Find (\ ref2 -> case match ref1 ref2 of
Just Eq -> Just Zero
_ -> Nothing
) :: Find env (b,())
)
|
