This commit is contained in:
Andreas Stadelmeier 2024-05-02 16:42:15 +02:00
parent b9ef35526f
commit 883969c067

View File

@ -31,6 +31,11 @@ $\begin{array}{l}
The constraint $\type{String} \lessdot {\ntv{x}}$ is solved by applying
\rulename{Super} and substituting $\type{String}$ for $\ntv{x}$.
Input constraints originating from a completely untyped input program do not contain any existential types.
Those are added during \unify{}.
The only parts where existential types are created are the \rulename{Match} and \rulename{General} rules.
\subsection{Description}
The \unify{} algorithm tries to find a solution for a set of constraints like
$\set{\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}}$.