{-# LANGUAGE RankNTypes
           , PolyKinds
           , GADTs
           , TypeApplications
           , PatternSynonyms
           , ExistentialQuantification
           , StandaloneKindSignatures
           , DataKinds
           , ExistentialQuantification
#-}

module ExplicitSpecificityA1 where

import Data.Proxy
import Data.Kind

-- Type variables bound in RULES
{-# RULES "parametricity" forall (f :: forall {a}. a -> a). map f = id #-}

-- Type signatures
foo1 :: a -> a
foo1 x = x

foo2 :: forall a. a -> a
foo2 x = x

foo3 :: forall {a}. a -> a
foo3 x = x

foo4 :: forall a {b}. a -> b -> b
foo4 _ x = x

foo5 :: forall {a} b. a -> b -> b
foo5 _ x = x

bar1 :: ()
bar1 = let { x1 = foo1 42
           ; x2 = foo2 @Int 42
           ; x3 = foo3 42
           ; x4 = foo4 @Bool True 42
           ; x5 = foo5 @Int True 42
           }
       in ()

-- Data declarations
data T1 a = C1 a

data T2 (a :: k) = C2 { f2 :: Proxy a }

data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a

data T4 a where C4 :: forall {k} (a::k). Proxy a -> T4 a

data T5 k (a :: k) where C5 :: forall k (a::k). Proxy a -> T5 k a

data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a

bar2 :: ()
bar2 = let { x1 = C1 @Int 42
           ; x2 = C2 @Type @Int Proxy
           ; x3 = C3 @Type @Int Proxy
           ; x4 = C4 @Int Proxy
           ; x5 = C5 @Type @Int Proxy
           ; x6 = C6 @Int Proxy
           }
       in ()

-- Pattern synonyms
data T7 a where C7 :: forall a b. a -> b -> T7 a

data T8 a where C8 :: forall a {b}. a -> b -> T8 a

pattern Pat1 :: forall a. () => forall b. a -> b -> T7 a
pattern Pat1 x y = C7 x y

pattern Pat2 :: forall {a}. () => forall b. a -> b -> T7 a
pattern Pat2 x y = C7 x y

pattern Pat3 :: forall a. () => forall b. a -> b -> T8 a
pattern Pat3 x y = C8 x y

pattern Pat4 :: forall {a}. () => forall b. a -> b -> T8 a
pattern Pat4 x y = C8 x y

pattern Pat5 :: forall {a}. () => forall {b}. a -> b -> T7 a
pattern Pat5 x y = C7 x y

bar3 :: (T7 a) -> ()
bar3 (Pat1 x y) = ()
bar3 (Pat2 x y) = ()

bar4 :: (T8 a) -> ()
bar4 (Pat3 x y) = ()
bar4 (Pat4 x y) = ()

-- Existential variable quantification
data HList = HNil
           | forall {a}. HCons a HList

-- Type synonyms
type TySy = forall a {b}. Either a b

-- Standalone kind signatures
type Foo :: forall a {b}. a -> b -> b
type Foo x y = y

type Bar = Foo @Bool True 42