type_invention_error : bool ref

SYNOPSIS

Determines if invented type variables are treated as an error.

DESCRIPTION

If HOL Light is unable to assign specific types to a term entered in quotation, it will invent its own type variables to use in the most general type. The flag type_invention_error determines whether in such cases the term parser treats it as an error. The default is false, since sometimes the invention of type variables is immaterial, e.g. in ad-hoc logical lemmas used inside a proof. However, to enforce a more careful style, set it to true.

FAILURE CONDITIONS

Not applicable.

EXAMPLE

When the following term is entered, HOL Light invents a type variable to use as the most general type. In the normal course of events this merely results in a warning (see type_invention_warning to remove even this warning):

  # let tm = `x = x`;;
  Warning: inventing type variables
  val tm : term = `x = x`

whereas if type_invention_error is set to true, the term parser fails with an error message:

  # type_invention_error := true;;
  val it : unit = ()
  # let tm = `x = x`;;
  Exception:
  Failure "typechecking error (cannot infer type of variables): =, x".

You can avoid the error by explicitly giving appropriate types or type variables yourself:

  # let tm = `(x:int) = x`;;
  val tm : term = `x = x`