Lambda the Ultimate

You got it in one ;^)

In languages that allow it the common, though less flexible, answer is a bit of recursively bounded parametric polymorphism. In Scala

class Child[C <: Child[C]] {
self : C =>
   var roomie : Option[C] = None

   def roomWith(aChild : C)= { 
     roomie = Some(aChild)
     aChild.roomie = Some(this) 
   }
}
class Boy extends Child[Boy]
class Girl extends Child[Girl]

You find it in a fair amount of Java code as well, for instance in the Java standard library there is

class Enum<T extends Enum<T>>

The C++ community calls this the curiously recurring template pattern. Template semantics implicitly create the bounds that must be explicit in Scala and Java.

Again, I don't know Eiffel, so I may be working from flawed premises here; I plead forbearance.

This is not type safe, but it is in some intuitive sense correct

...which seems a sure sign that one has gotten either their formalisms or their intuitions wrong.

Taking the subclass signatures as a given, the only sane signature for roomWith on Child is not to accept the union of the subtype signatures, but the intersection. Working on the assumption that no objects are simultaneously instances of Boy and Girl, this is the uninhabited type. As all types can be regarded as superclasses of the uninhabited type, Boy and Girl's signatures for roomWith are thus contravariant in the argument, as expected.

One might object that this could make it awkward to inherit the (presumably identical) implementations of the roomWith method, to which I would ask why subtyping is being conflated with code reuse (and with ad-hoc polymorphism, and with dynamic dispatch...) in the first place, but that's another matter entirely.

One might also object that this makes the roomWith method on Child useless; this is of course true, both necessarily so on pain of type unsafety, and logically so given the desired restriction on roommate assignment requiring information not present in the Child class. There are arguments in favor of ignoring type safety for the sake of ease and expressivity, but they fall rather flat if deployed on behalf of a static-typed language. Might as well take up Ruby or something and be done with it.

All that said, I'm still suspicious that I'm missing something important. Given the descriptions I've heard of Eiffel--promoting it as a static-typed object-oriented language with an emphasis on reliability and correctness--it's baffling that something as central as subtyping/inheritance would egregiously break type safety guarantees, accepting incorrect code that could easily have been caught at compile-time. So again, if anyone can set my mind at ease, I would be most grateful.

Eiffel's marketing as "correct and reliable" seem to have more to do with it's relationship with Design By Contract than on its static type system.

The irony is that a static type promises a contract and covariant arguments violate the contract by, in DBC terms, "strengthening preconditions".

The temptation to "cheat" must be strong. Java has an unsound bit of covariance as well. This compiles but creates an error at runtime

String[] strings = new String[]{"hello", "world"};
Object[] objects = strings;
objects[0] = new Integer(42); // runtime error

The irony is that a static type promises a contract and covariant arguments violate the contract by, in DBC terms, "strengthening preconditions".

Yes, exactly. A peculiar contradiction, it seems to me, since "weakening preconditions" serves well as a concise and accurate description of why arguments ought to be contravariant!

Java has an unsound bit of covariance as well. This compiles but creates an error at runtime

Well, yes, but this fails to surprise. Java seems to have been designed to strike a careful balance between making the type system as obstructive as possible while minimizing any actual guarantees of correctness. Creating runtime errors in Java code is hardly sporting, I fear.

At any rate, given that assignment permits only subclasses but element access permits only superclasses, mutable collections are sadly forced to be invariant.

Java seems to have been designed to strike a careful balance between making the type system as obstructive as possible while minimizing any actual guarantees of correctness.

Wonderfully stated. :-)

At any rate, given that assignment permits only subclasses but element access permits only superclasses, mutable collections are sadly forced to be invariant.

A more expressive language than Java could utilize separate 'read-only' and 'write-only' facets (or interfaces) for each mutable collection, and simply have the initial collection extend both.

I've seen similar discussion regarding 'circle and ellipse'. A read-only circle subtypes a read-only ellipse, and a write-only ellipse subtypes a write-only circle. Presumably both could extend closed 2D geometries.

Though, IMO all these collections and ellipses and rooming or children really fall outside the purview of OOP. OOP types should focus on communications relationships, behavioral contracts, where and how elements plug safely and securely into the larger OO 'machine'. Data and modeling (of numbers, geometries, organized data) deserves their own first-class paradigm, such as term rewriting, pure functional, rules-based or concurrent logic, immutable values.

That simply sounds like a badly designed hierarchy. When I have a single boy and a collection of children (boys and girls) and call roomWith on each of the children in the collection with the single boy as argument would I get an UnsupportedOperationException whenever the child is actually a girl?

The "roomWith" method on Child seems useless as you can't reliably call it. It looks like it was introduced only to save some typing while implementing Boy and Girl using inheritance. IMO some other mechanism of "code reuse" should be used.

If "Boy" can't fulfill the contract established by "Child" there should not be a subtype relation.

Maybe so. But if a language is going to have inheritance without subtyping, that really ought to be reflected in the safety analysis.

[edit] maybe I should have read 'can never be' as 'never can be'. Your assertion would have made more sense.

You are right. I have been a little bit sloppy in formulating that way.

Eiffel has been designed to be typesafe with one exception. It allows catcalls which are type errors, because it allows you to inject the wrong type.

So an actual catcall is a type errror, but not all type errors are catcalls. But there are no other type errors possible in Eiffel.