  While generalized algebraic datatypes (\GADTs) are now considered
well-understood, adding them to a language with a notion of subtyping comes
with a few surprises. What does it mean for a \GADT parameter to be covariant?
The answer turns out to be quite subtle. It involves fine-grained properties of
the subtyping relation that raise interesting design questions. We allow
variance annotations in \GADT definitions, study their soundness, and present a
sound and complete algorithm to check them. Our work may be applied to
real-world ML-like languages with explicit subtyping such as OCaml, or to
languages with general subtyping constraints.
