11.1.2 Semantics of type quantifiers

If a type variable in the type declaration for a polymorphic predicate or function is universally quantified, this means the caller will determine the value of the type variable, and the callee must be defined so that it will work for all types which are an instance of its declared type.

For an existentially quantified type variable, the situation is the converse: the callee must determine the value of the type variable, and all callers must be defined so as to work for all types which are an instance of the called procedure’s declared type.

When type checking a predicate or function, if a variable has a type that occurs as a universally quantified type variable in the predicate or function declaration, or a type that occurs as an existentially quantified type variable in the declaration of one of the predicates or functions that it calls, then its type is treated as an opaque type. This means that there are very few things which it is legal to do with such a variable — basically you can only pass it to another procedure expecting the same type, unify it with another value of the same type, put it in a polymorphic data structure, or pass it to a polymorphic procedure whose argument type is universally quantified. (Note, however, that the standard library includes some quite powerful procedures such as ‘io.write’ which can be useful in this context.)

A non-variable type (i.e. a type that is not a type variable) is considered more general than an existentially quantified type variable. Type inference will therefore never infer an existentially quantified type for a predicate or function unless that predicate or function calls (directly or indirectly) a predicate or function which was explicitly declared to have an existentially quantified type.

Note that an existentially typed procedure is not allowed to have different types for its existentially typed arguments in different clauses (even mode-specific clauses) or in different subgoals of a single clause; however, the same effect can be achieved in other ways (see Some idioms using existentially quantified types).

For procedures involving calls to existentially-typed predicates or functions, the compiler’s mode analysis must take account of the modes for type variables in all polymorphic calls. Universally quantified type variables have mode in, whereas existentially quantified type variables have mode out. As usual, the compiler’s mode analysis will attempt to reorder the elements of conjunctions in order to satisfy the modes.