module Main where



data Term =
  Variable String |
  Abstraction String Type Term |
  Application Term Term |
  TypeAbstraction String Term |
  TypeApplication Term Type
    deriving (Show, Eq, Ord)


data Type =
  TypeVariable String |
  FunctionType Type Type |
  UniversalType String Type
    deriving (Show, Eq, Ord)


type Context = [(String, Type)]


typeCheck :: Context -> Term -> Type


main :: IO ()
main = do
  print (typeCheck [] term)

term = TypeAbstraction "A" (Abstraction "x" (TypeVariable "A") (Variable "x"))