The rule right now for inheritance is that you can't change the nullability of the type signatures in overrides. This includes covariance rules for return types:

class Base
{
  virtual Obj a() { ... }
  virtual Obj? b() { ... }
  virtual Void c(Str? x) {}
}

class Foo : Base
{
  override Obj? a() { ... }
  override Obj b() { ... }
  override Void c(Str x) {}
}

In the above example the override of both a and b is a compiler error. Technically the override of b is covariant and could be supported since aren't breaking the base class contract. But I'm not going to allow that until we get some experience under our belt with nullable types (it also has ramifications for value-types).

The override of c is a compiler error because method parameters must match exactly.

All logical, no objections to that. I don't see how allowing b case would help - you can return Obj in function returning Obj? but why would you declare it if you can't rely on it anywhere?

But this reminds me a question which has been floating around my mind since I've read the paper that JohnDG linked lately. How do we consider nullability? We could run the static provability algoritms inside methods locally or we could go for a wider scope within class or a pod - globally. This approach could allow more convenient coding like:

::pod AA::
class A {
    public Str? getX() { 
      return "hello"
    }

    Void acceptStr(Str x) {
      ...
    }

    Void useX() {
      x := getX  // x is actuall non-null Str
      ...
      x.hash     // OK!
      ...
      acceptStr (x) // OK!
    }
 }

 ::pod BB::
 class B {

    Void useXFromDifferentPod {
       a := A.make
       x := a.getX()  // different pod, disregarding implementation
       ...
       x.hash         // compilation error, signature is used for inference
       ...
       a.acceptStr(x) // compilation error, signature is used for inference
       ...           
    }
 }

This could also enable more aggressive optimization techniques inside pods.

Again, I'm not sure about dynamic usages but I guess it wouldn't make a big difference since there is very little known anyway in such cases...

We could run the static provability algoritms inside methods locally or we could go for a wider scope within class or a pod - globally.

The compiler works at the pod level. The compiler already performs pod optimization techniques. For example inside a pod, non-virtual fields are accessed directly without going thru their getter/setter since we can perform pod-level analysis. Outside of the pod we always access fields thru their getter/setter (although typically HotSpot will inline them). So pod level analysis will probably be an area ripe for optimization in the future.