blob: 5e3b377ee2be599a257fbabccc8feaa51d473502 (
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
|
{-# LANGUAGE ImpredicativeTypes #-}
-- Sept 16: now failing, because I've further reduced the scop
-- of impredicative types
module Base1 where
-- basic examples of impredicative instantiation of variables
data MEither a b = MLeft a
| MRight b
| MEmpty
type Sid = forall a. a -> a
-- no need for impredicativity
test0 = MRight id
-- requires impredicativity
test1 :: Sid -> MEither Sid b
test1 fid = MLeft fid
test2 :: MEither b Sid -> Maybe (Sid,Sid)
test2 m = case (test1 id) of
MLeft x -> case m of
MRight y -> Just (x,y)
_ -> Nothing
_ -> Nothing
test3 :: MEither a b -> b
test3 (MRight x) = x
test4 = test3 (test1 id)
|
