Scott-encoded pair with type lambdas

gistfile1.txt

-- In "readable" notation. "Definitions" are for clarity and will in fact all appear inline.

Pair :: * -> * -> *
Pair = 
  -- type params
  \a :: * . \b :: * .
  -- match output type
  forall t :: * . 
  -- matcher type
  a -> b -> t
  
pair : forall a :: * . forall b :: * . a -> b -> (Pair a b)
-- i.e. the following, which is in this case legal because it's in the output type, but would be a problem if we had
-- to write the full type of pair somewhere
-- forall a :: * . forall b :: * . a -> b -> ((\a' :: * . \b' :: * . forall t :: * . a' -> b' -> t) a b)
-- but which reduces to this which is fine
-- forall a :: * . forall b :: * . a -> b -> (forall t :: * . a -> b -> t)
pair a b match = match a b

addComponents : (Pair Int Int) -> Int
-- i.e. the following, which is illegal because it has a type lambda as the argument type of a function
-- ((\a' :: * . \b' :: * . forall t :: * . a' -> b' -> t) Int Int) -> Int
-- but reduces to this, which is legal
-- (forall t :: * . Int -> Int -> t) -> Int
addComponents tuple = tuple (\a b . a + b)