let f = fun x -> (x, x)

	f : 'a -> 'a * 'a



	Gu[x:t] |- x : t1 | {t1 = t}    Gu[x:t] |- x : t2 | {t2 = t}
	-------------------------------------------------------------
	Gu[x:t] |- (x, x) : t' | {t' = t1 * t2} u {t1 = t} u {t2 = t}
	-------------------------------------------------------------
	G |- fun x -> (x, x) : t3 | {t' = t1 * t2} u {t1 = t} u {t2 = t}
	                            u {t3 = \ALL{t} . t -> t'}

	//{t' = t1 * t2}
	//{t1 = t}
	//{t2 = t}
	//{t3 = \ALL{t} . t -> t'}

	theta = [t' <- t1 * t2][t1 <- t][t2 <- t]

	        [t' <- t * t][t1 <- t][t2 <- t][t3 = \ALL{t} . t -> t']
What is the type of (fun x -> (x, x)) ?

	t3 theta
	t3 [t' <- t * t][t1 <- t][t2 <- t][t3 = \ALL{t} . t -> t']
	\ALL{t} . t -> t * t

	let f = fun x -> (x, x) in
		(f 7, f "string")

	 ...                       ...
	----------------------    -----------------------------
	Gu[f:t3] |- f 7 : s1|C1    Gu[f:t3] |- f "string" : s2|C2
	-------------------------------------------------------
	Gu[f : t3] |- (f 7, f "string")

	C1 = {t3 = s1 -> s2, s1 = int}
	C2 = {t3 = s3 -> s4, s3 = string}

	s1 -> s2 = s3 -> s4
	int -> s2 = string -> s4

Instead, put a type schema in the environment:

	Gu[f:\ALL{t} . t -> t * t] |- f : s|{s = s5 -> s5 * s5}
	-----------------------
	Gu[f:\ALL{t} . t -> t * t] |- f 7 : ...
	-------------------------------------------------
	Gu[f : \ALL{t} . t -> t * t] |- (f 7, f "string")

	Gu[f:\ALL{t} . t -> t * t] |- f : s'|{s' = s6 -> s6 * s6}
	-----------------------
	Gu[f:\ALL{t} . t -> t * t] |- f "string" : ...

	C1 = {s = s5 -> s5 * s5, s5 = int}
	C2 = {s' = s6 -> s6 * s6, s6 = string}







Example 2

	let rec f x =
		match x with
		  []      -> raise Exception
		| y::rest -> y + (f rest)

	int
	program does not return a value

	let rec f = fun x ->
		match x with
		  []      -> raise Exception
		| y::rest -> y + (f rest)
	in
		f [7]

	\T = \ALL {} int list -> int

	What are the typing rules for match?

	                      {...} |- f : T|{}
	                      {...} |- rest : T4|{}
	-----------------     ----------------------------------
	{...} |- y : T3|{}    {...} |- (f rest) : T5|{T = T4->T5}
	-----------------------------------------------------
	{f:T, x:T1, y:T3, rest:T4} |- y + (f rest) : T6|{T6=int,T3=int,T5=int,T=T4->T5}


	{f:T, x:T1} |- match ... : T6 | {T6=int,T3=int,T5=int,T=T4->T5, T1=T3 list}
	-----------------------------------------
	{f : T} |- fun x -> ... : T7 | {T7=T1->T6,T6=int,T3=int,T5=int,T=T4->T5, T1=T3 list}
	--------------------------------------------
	{} |- let rec f = ... in f 7 : ... | {T7=T1->T6,T6=int,T3=int,T5=int,T=T4->T5, T1=T3 list, T=T7}

Solve this set of constraints to determine the type of f:
	E0 = {T7=T1->T6, T6=int, T3=int, T5=int, T=T4->T5, T1=T3 list, T=T7}
	Theta0 = {}
		take the equation T6=int, apply rule 4
	E1 = {T7=T1->int, T3=int, T5=int, T=T4->T5, T1=T3 list, T=T7}
	Theta1 = {T6 <- int}
		take the equation T5=int, apply rule 4
	E2 = {T7=T1->int, T3=int, T=T4->int, T1=T3 list, T=T7}
	Theta2 = {T6 <- int, T5 <- int}
		take the equation T1=T3 list, apply rule 4
	E3 = {T7=(T3 list)->int, T3=int, T=T4->int, T=T7}
	Theta3 = {T6 <- int, T5 <- int, T1 <- T3 list}
		take the equation T3=int, apply rule 4
	E4 = {T7=(int list)->int T=T4->int, T=T7}
	Theta4 = {T6 <- int, T5 <- int, T1 <- int list, T3 <- int}
		take the equation T=T7, apply rule 4
	E5 = {T7=(int list)->int, T7=T4->int}
	Theta5 = {T6 <- int, T5 <- int, T1 <- int list, T3 <- int, T <- T7}
		take the equation T7=(int list)->int, apply rule 4
	E6 = {(int list)->int=T4->int}
	Theta6 = {T6 <- int, T5 <- int, T1 <- int list, T3 <- int, T <- T7,
	          T7 <- (int list)->int}
		take the only equation and apply rule 1
	E6 = {(int list)=T4, int=int}
	Theta6 = {T6 <- int, T5 <- int, T1 <- int list, T3 <- int, T <- T7,
	          T7 <- (int list)->int}
	E6 = {(int list)=T4}
	Theta6 = {T6 <- int, T5 <- int, T1 <- int list, T3 <- int, T <- T7,
	          T7 <- (int list)->int}
	E6 = {}
	Theta9 = {T6 <- int, T5 <- int, T1 <- int list, T3 <- int, T <- T7,
	          T7 <- (int list)->int, T4 <- int list}