Here's a simple example program:
(top-level ((in int x))
(let ((f (lambda (x) (+ x 1))))
(f 2)))
The only type declaration is on the shader input attribute 'x'. Here's the typed program that the compiler generates:
(t ((primitive int))
(top-level
((in int V0)
(function
V2
(t ((for-all
((tvar T3) (tvar T7))
(-> ((tvar T3)) ((tvar T7)))
(and (= (tvar T3) (primitive int))
(substitute (tvar T7) (tvar T3)))))
(lambda (V1)
(t ((tvar T7))
(primcall
+
(t ((tvar T3)) V1)
(t ((primitive int)) 1)))))))
(t ((primitive int))
(call (t ((-> ((primitive int)) ((primitive int)))) V2)
(t ((primitive int)) 2)))))
The interesting bit is the 'for-all' expression that generalizes the function 'f' to accept any arguments as long as they satisfy the predicate (the 'and' expression). In this case the only valid type for 'x' is an integer.
The compiler is currently unable to emit GLSL code for the function because it doesn't yet know how to translate a 'for-all' into a series of functions for each valid type combination. That's the next step.