@spec apply_subst(HOL.Data.type() | atom(), substitution()) ::
  HOL.Data.type() | atom()

Applies a substitution to a given type or atom.

@spec mk_new_unknown_type() :: HOL.Data.type()

Creates a new and unique unknown type.

@spec solve([{HOL.Data.type(), HOL.Data.type()}]) :: substitution()

Tries to solve a given list of type constraints by unifying them.

Employs Robinson's unification algorithm (first-order syntactic unification) to find the most general unifier for the types. The returned substitutions are given as a Map mapping "_unknown" type identifiers to types or atoms.

Examples

iex> solve([{mk_new_unknown_type(), HOL.Data.mk_type(:i)}])
%{__unknown_1: :i}

iex> solve([{mk_new_unknown_type(), mk_new_unknown_type()}])
%{__unknown_1: :__unknown_2}

iex> t1 = mk_new_unknown_type()
iex> t2 = mk_new_unknown_type()
iex> solve([{t1, t2}, {t2, HOL.Data.mk_type(:i, [HOL.Data.mk_type(:i)])}])
%{__unknown_1: {:type, :i, [{:type, :i, []}]}, __unknown_2: {:type, :i, [{:type, :i, []}]}}

@spec unknown_type?(HOL.Data.type() | atom()) :: boolean()

Checks whether the given atom or type represents an unknown type. An atom is an unknown type if the prefix of its string representation "_unknown". A type is an unknown type if its goal recursively reduces to an unknown type.