\section{Related Work}
Igarashi et al \cite{FJ} define Featherweight Java
and its generic sibling, Featherweight Generic Java. Their language is
a functional calculus reduced to the bare essentials, they develop the full metatheory, they
support generics, and study the type erasing transformation used by
the Java compiler. Stadelmeier et. al. extends this approach by global type
inference \cite{TIforFGJ}.

\subsection{Wildcards in formal Java models}
Wildcards are first described in a research paper in \cite{addingWildcardsToJava}. In
\cite{TEP05} the Featherweight Java-Calculus \textsf{Wild~ FJ} is introduced. It
contains a formal description of wildcards. The Java Language Specification
\cite{GoJoStBrBuSm23}  refers to \textsf{Wild~FJ} for the introduction of
wildcards. In \cite{aModelForJavaWithWildcards} a formal model based of explicite existential types
is introduced and proven as sound. Additionally, for a subset of Java a
translation to the formal model is given, such that this subset is proven as
sound. In \cite{WildcardsNeedWitnessProtection} another core calculus is
introduced, which is proven as 
sound, too. In this paper it is shown that the unsoundness of Java which is
discovered in \cite{AT16} is avoidable, even in the absence of nullness-aware type
system. In \cite{TamingWildcards} finally a framework is presented which combines
use-site variance (wildcards as in Java) and definition-site variance (as in Scala). For
instance, it can be used to add use-site variance to Scala and extend the Java
type system to infer the definition-site variance.

Our calculus is mixture ...

\subsection{Type inference}
Some object-oriented languages like Scala, C\#, and Java perform
\emph{local} type inference \cite{PT98,OZZ01}. Local type
inference means that missing type annotations are recovered using only
information from adjacent nodes in the syntax tree without long distance
constraints. For instance, the type of a variable initialized with a
non-functional expression or the return type of a method can be
inferred. However, method argument types, in particular for recursive
methods, cannot be inferred by local type inference.

Milner's algorithm $\mathcal{W}$ \cite{DBLP:journals/jcss/Milner78} is
the gold standard for global type inference for languages with
parametric polymorphism, which is used by ML-style languages. The fundamental idea
of the algorithm is to enforce type equality by many-sorted type
unification \cite{Rob65,MM82}. This approach is effective and results
in so-called principal types because many-sorted unification is
unitary, which means that there is at most one most general result.

Pl\"umicke \cite{Plue07_3} presents a first attempt to adopt Milner's
approach to Java. However, the presence of subtyping means that type
unification is no longer unitary, but still finitary. Thus, there is
no longer a single most general type, but any type is an instance of a
finite set of maximal types (for more details see Section
\ref{sec:unification}). Further work by the same author
\cite{plue15_2,plue17_2},
refines this approach by moving to a constraint-based algorithm and by
considering lambda expressions and Scale-like function types.

Pluemicke has a different approach to introduce wildcards in \cite{Plue09_1}. He
allows wildcards as any subsitution for type variables and disclaim the
capture conversion. Instead he extended
the subtyping ordering such that for $\theta \sub \theta' \sub \theta''$ holds
indeed the transitiv closure of $\QMextends{\theta} \sub \theta'$ and $\theta' \sub
\QMsuper{\theta''}$ but not the reflexive closure. He gave a type unification
algorithm for this type system, which he proved as sound and complete. 

The problem of his type system is in the lossing reflexivity as shown in
example \ref{intro-example1}. First approaches to solve this problem he gave in
\cite{plue24_1}, where he fixes that no pairwise different nodes in the
abstract syntax gets the same type variable and that no pairwise different type
variables are equalized. In \cite{PH23} he showed how his type inference
algorithm suffices theese properties.

In Pl\"umicke's work there is indeed a formal definition of the subtying
ordering and a correctness proof of the type unification algorithms but no
soundness proof of the type system, itself. Therefore we choose for our type
inference algorithms with wildcars the approach of ???????