{-# LANGUAGE TypeApplications, ScopedTypeVariables, PolyKinds,
  TypeFamilies, RankNTypes, FlexibleContexts #-}
module Vta1 where

quad :: a -> b -> c -> d -> (a, b, c, d)
quad = (,,,)
silly = quad @_ @Bool @Char @_ 5 True 'a' "Hello"
pairup_nosig x y = (x, y)

pairup_sig :: a -> b -> (a, b)
pairup_sig u w = (u, w)
answer_sig = pairup_sig @Bool @Int False 7
answer_read = show (read @Int "3")
answer_show = show @Integer (read "5")
answer_showread = show @Int (read @Int "7")
intcons a = (:) @Int a
intpair x y = pairup_sig @Int x y
answer_pairup = pairup_sig @Int 5 True
answer_intpair = intpair 1 "hello"
answer_intcons = intcons 7 []

type family F a

type instance F Char = Bool

g :: F a -> a
g _ = undefined

f :: Char
f = g True
answer = g @Char False

mapSame :: forall b . (forall a . a -> a) -> [b] -> [b]
mapSame _ [] = []
mapSame fun (x : xs) = fun @b x : (mapSame @b fun xs)

pair :: forall a . a -> (forall b . b -> (a, b))
pair x y = (x, y)
b = pair @Int 3 @Bool True
c = mapSame id [1, 2, 3]
d = pair 3 @Bool True

pairnum :: forall a . Num a => forall b . b -> (a, b)
pairnum = pair 3
e = (pair 3 :: forall a . Num a => forall b . b -> (a, b)) @Int
      @Bool
      True
h = pairnum @Int @Bool True

data First (a :: * -> *) = F

data Proxy (a :: k) = P

data Three (a :: * -> k -> *) = T

foo :: Proxy a -> Int
foo _ = 0

first :: First a -> Int
first _ = 0
fTest = first F
fMaybe = first @Maybe F
test = foo P
bar = foo @Bool P

too :: Three a -> Int
too _ = 3
threeBase = too T
threeOk = too @Either T
blah = Nothing @Int

newtype N = MkN{unMkN :: forall a . Show a => a -> String}
n = MkN show
boo = unMkN n @Bool

boo2 :: forall (a :: * -> *) . Proxy a -> Bool
boo2 _ = False
base = boo2 P
bar' = boo2 @Maybe P