In the explanatory text there is the phrase “where type parameters are instantiated” which I do not understand.

Jacques Garrigue replied that “that the type parameters may be more specific than in the generic case.”.
I see now that values that would be admitted to the type defined without the “-> 'a term” are excluded.
<p>I would say somewhat more verbosely that the text “<tt>Add : (int -> int -> int) term</tt>” means that when the <tt>Add</tt> constructor is used, the type of the value produced is <tt>(int -> int -> int) term</tt>.
This is a recursive type.
I need to understand how an int list could be defined if it were not primitive.
Perhaps it is not possible without GADTs, is it possible with?
<a href=f.html>This</a> works: