{-# 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)