The Free On-line Dictionary of Computing (30 December 2018):

type inference

    An algorithm for ascribing types to
   expressions in some language, based on the types of the
   constants of the language and a set of type inference rules
   such as

   	f :: A -> B,  x :: A
   	---------------------  (App)
   	      f x :: B

   This rule, called "App" for application, says that if
   expression f has type A -> B and expression x has type A then
   we can deduce that expression (f x) has type B.  The
   expressions above the line are the premises and below, the
   conclusion.  An alternative notation often used is:

   	G |- x : A

   where "|-" is the turnstile symbol (LaTeX \vdash) and G is a
   type assignment for the free variables of expression x.  The
   above can be read "under assumptions G, expression x has type
   A".  (As in Haskell, we use a double "::" for type
   declarations and a single ":" for the infix list constructor,
   cons).

   Given an expression

   	plus (head l) 1

   we can label each subexpression with a type, using type
   variables X, Y, etc. for unknown types:

   	(plus :: Int -> Int -> Int)
   		(((head :: [a] -> a) (l :: Y)) :: X)
   		(1 :: Int)

   We then use unification on type variables to match the
   partial application of plus to its first argument against
   the App rule, yielding a type (Int -> Int) and a substitution
   X = Int.  Re-using App for the application to the second
   argument gives an overall type Int and no further
   substitutions.  Similarly, matching App against the
   application (head l) we get Y = [X].  We already know X = Int
   so therefore Y = [Int].

   This process is used both to infer types for expressions and
   to check that any types given by the user are consistent.

   See also generic type variable, principal type.

   (1995-02-03)