`Nothing` should be permissive

[shriram]

Sometimes an imperative function ends with a structure update. Technically, that returns the updated structure.

However, it's reasonable to want to annotate this with the return type Nothing, both to indicate that this is an effectful function and to warn the user to not rely on (and hence compositionally use) this particular return value.

For instance, this program

data Box: box(ref v) end

fun set-to-3(b :: Box) -> Nothing:
  b!{v: 3}
end

b = box(1)
set-to-3(b)

raises an error because the return value doesn't match the Nothing annotation. But Nothing should be permitted here.

Note that this also happens with the type-checker:

data Box<T>: box(ref v :: T) end

fun set-to-3(b :: Box<Number>) -> Nothing:
  b!{v: 3}
end

b = box(1)
set-to-3(b)

[blerner]

But b!{v: 3} evaluates to the box, which is decidedly not nothing. We wanted ! to be chainable, so e.g. b!{v: 3}!{v: 4} would work. Unless we change that semantics (which would be backward-incompatible, though I don't know if anyone cares...), I think this bug is a WONTFIX: I think it absolutely should not be the case that annotating the return type as Nothing should change the actual return value of the function, nor should the return type lie.

[shriram]

Okay. I was asking to change the semantics of the annotation, not of the implementation (where I think our current design is a good one). One can achieve my desired effect in a rather clunky way, by (a) always writing an explicit nothing and (b) adding a block (which might previously not have been necessary). I think it's ugly but it probably doesn't occur often enough to be a real issue.