Conversely, when comparing types, a known type argument
(a type argument for which a map entry already exists)
takes the place of its corresponding type parameter.
As type inference progresses, the map is populated more and more
until all equations have been considered, or until unification fails.
Type inference succeeds if no unification step fails and the map has
an entry for each type parameter.
</p>

<p>