let fun ident(x) => x in ident(ident)(2) end
then the second ident has type int->int and the first ident
has type (int->int)->(int->int). The type inference
algorithm will find by checking the declaration of ident that it
has some type 'X->'X for a type variable 'X that is
used nowhere else in the program (the type checker can tell this by looking in
the type environment to see whether 'X appears there). At each use
of ident, it replaces 'X with new type variables (say,
'Y and 'Z respectively). This decoupling permits them
to be solved independently, as desired, to obtain 'Y = (int->int)->(int->int)
and 'Z=int->int.
Below is some code that implements type inference with let-polymorphism.
There are a few changes from the simple type inference just given. The
environment no longer maps identifiers to types; it maps them to type schemas.
A type schema is a type along with a list of type variables that can be
substituted differently at every use of the identifier. In declcheck, the types
that are determined for variables are abstracted by schema to
construct type schemas. Then, when type-checking an identifier, the instantiate
function is used to replace all the type parameters identified by schema
with fresh type variables.