blob: 0e23ed1640c42b8958b30798bca7de965fee63e6 (
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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
{-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables, GADTs #-}
-- Nov 2014: impredicative types are very dodgy so I am
-- FAR from confident that these tests give the right errors
-- Here are a bunch of tests for impredicative polymorphism
-- mainly written by Dimitrios
-- Sept 16: I'm just accepting the bizarre output.
-- None of this is right
module ShouldCompile where
xs :: [forall a. a->a]
xs = [\x -> x]
foo = id xs
-- Annotation resolves impredicative instantiation
bar = ((:)::(forall a.a ->a) -> [forall a. a->a] -> [forall a. a ->a])
(head foo) foo
-- result type resolves everything! really neat
barr :: [forall a. a -> a]
barr = (head foo):(tail foo)
zoo = tail xs
zooo = head xs
-- This is the only unsatisfactory case...annotating
-- one of the arguments does not do the job...but maybe
-- this is reasonable to expect ...
-- bar3 = ((head foo) :: forall a. a ->a) : foo
data Pair a b where
P :: a -> b -> Pair a b
data List a where
Nil :: List a
Cons :: a -> List a -> List a
-- FromMono :: (a->a) -> List (forall a. a->a)
-- This constructor looks utterly bogus, so
-- I'm commenting it out; SLPJ 7 Jan 08
f :: Int -> Pair Int Int
f x = P x x
h0 :: (forall a. a -> a) -> Int
h0 g = let y = P (g 3) (g (P 3 4))
in 3
h1 (g::(forall a. a ->a))
= let y = P (g 3) (g (P 3 4))
in 3
h2 :: (forall a. a -> a) -> Int
h2 (g::(forall a. a ->a)) = let y = P (g 3) (g (P 3 4))
in 3
xs1 :: List (forall a. a ->a)
xs1 = let cons = Cons :: (forall a. a ->a)
-> List (forall a. a->a)
-> List (forall a. a ->a)
in cons (\x -> x) Nil
xs2 :: List (forall a. a -> a)
xs2 = (Cons :: ((forall a. a->a)
-> List (forall a. a->a)
-> List (forall a. a->a)))
(\x ->x) Nil
foo2 :: forall a. List a -> a -> a
foo2 x y = y
bar4 = (foo2 :: List (forall a. a->a) -> (forall a. a->a) -> (forall a.a->a))
xs1 (\x -> x)
|
