Instances where (modern) programming languages disregarded or ignored TypeTheory, and have painted themselves into corners. (Feel free to add your own; probably no fair to list low-level languages like C that provide myriad mechanisms for subverting type systems).

'''Covariant arguments in EiffelLanguage'''

BertrandMeyer is, of course, one of the leading authorities on ObjectOrientedProgramming. He wrote the classic ObjectOrientedSoftwareConstruction, considered by many to be the most comprehensive book on OO ever written. Many consider his brainchild, EiffelLanguage, to be an exceptionally well-designed programming language, especially for the domain of building large robust systems. Eiffel features a thoroughly modern type system, complete with generics, pre/postconditions and invariants ("design by contract"), a robust inheritance model, etc. Much of modern TypeTheory is reflected in the language.

And yet Eiffel contains one major hole in the type system by allowing derived classes to ''override'' virtual methods by introducing ''covariant'' parameters. If a virtual method is called through a polymorphic reference (the binding happens at runtime) then the compiler allows that the method is passed an object of an incorrect type. In this case undesirable behavior may occur ranging from run-time exception to program crashes and other UndefinedBehavior.

Surely BertrandMeyer knew better. At the time Eiffel was designed, at least as early as 1984, TypeTheory was sufficiently advanced that it could model most OO language features, including the overriding of methods in derived classes even in the face of multiple inheritance [Cardelli88]. One of the conclusions of TypeTheory was that in a derived-class method:

* input arguments could be modified contravariantly from the base-class function (in other words, the type of a derived-class function argument could be a SuperType of the type of the corresponding argument in the base-class function).

* output arguments (including the return type) may be modified covariantly (the return type of the derived-class function may be a SubType of the base-class function).

* For bidirectional arguments, the type must remain the same.

ContraVsCoVariance is a long discussion among language designers. While the above approach is unproblematic for constructing a sound type system, it is seen as having no big practical value either. Indeed, in the practice of writing actual programs it was probably never observed and reported in a published papers that contra-variant arguments are needed, while examples where CoVariance happens are quite frequent in practice and reported in publications. That's why efforts to accommodate CoVariance in a sound type system have been one of the hot topics of research in type theory. Later proposals include the ones published by [Castagna' 95] and K. Bruce [FOOL].

Meyer ignored TypeTheory and went with pragmatism by implementing covariant overriding of arguments. (Note that this is completely wrong according to Cardelli and completely different from what Castagna describes. Both papers are not at odds with each other.)

Needless to say, this was a major source of embarrassment to Meyer and the Eiffel community. A cure was sought. Rather than doing the obvious (either biting the bullet and withdrawing covariant arguments, or inserting a runtime typecheck or precondition in covariant derived-class methods, or letting covariantly typed functions specialize their ancestor instead of overriding it), a notorious and brutal hack called "no polymorphic catcalls" was devised, effectively removing the offending method from the base class, where it arguably should never have been declared in the first place. This cure was arguably worse than the disease, as it caused many correct programs to suddenly not compile anymore.

Judging by modern standards, and given the fact that the hole is still open after more than a decade, it is apparent that B. Meyer's decision was a design mistake. It is puzzling for many of us, given subsequent developments in programming language implementations, why a runtime type check would not automatically be inserted in the methods that can potentially trigger the problem. Eiffel provides runtime exceptions in other instances of an ImperfectHierarchy (such as precondition narrowing - a more general issue which includes covariance, and method deletion).

It should be noted that this is only an issue with SingleDispatch languages (including Eiffel). Languages supporting some level of MultipleDispatch (wherein functions may be polymorphic on all their arguments) have fewer problems with covariance - being able to fall back on the (type-correct) base class method if a noncovariant actual parameter is passed to a method expecting a covariant formal parameter. (Whether this behavior is ''semantically'' correct is another issue; the above-mentioned Castagna paper provides methods to deal with semantic issues).

References:
* K. Bruce (2002) FoundationsOfObjectOrientedProgrammingLanguages discusses both the Eiffel case and the need and possible solutions for covariant arguments
* G. Castagna (1995) "covariance and contravariance : conflict without a cause" http://citeseer.ist.psu.edu/castagna94covariance.html . This paper proposes a type system with support for both features.
* B. Meyer (1995) "Static typing and other mysteries of life" http://archive.eiffel.com/doc/manuals/technology/typing/paper/page.html the case for covariance and that practical implications of the type holes are manageable 
* B. Meyer & collaborators "Typesafe covariance" http://se.ethz.ch/~meyer/ongoing/covariance/recast.pdf reporting on the progress towards a solution and restating the case for CoVariance in 2003.
* Luca Cardelli "A Semantics of Multiple Inheritance" http://citeseer.ist.psu.edu/cardelli88semantics.html, a revised version of the paper that appeared in the 1984 Semantics of Data Types Symposium, LNCS 173, pages 51-66

----
'''Java's array subtyping'''

In JavaLanguage an array of subtype is considered a subtype of an array of the base type. For example:
  String[] <: Object[]
Such that an array of strings can be passed where an array of object. In a language like Java where arrays are mutable this is known to be unsafe, as the code that manipulates an Object[] reference can store anything at all in that array. See JavaArraysBreakTypeSafety.

Although somebody has argued that this was a major design blunder, the reality is that it was a trivial engineering decision. If Java didn't have this typing rule than developers would not have been allowed to write generic code that implement algorithms on arrays, such as:
 Arrays.sort(Object[] array, Comparator comp)
Writing generic algorithms in a statically type-safe manner requires ParametricPolymorphism (a.k.a. generic types, parameterized types) and this feature was not available in Java for quite a while. JavaTypingWasSimple. Unlike in the case of Eiffel type hole, Java's runtime automatically checks array store operations and throws a runtime exception (ArrayStoreE''''''xception).

----
See also LanguageTypeErrorsDiscussion