Back-edge check (Semant.is_back_edge) is too strong

[pcwalton]

The back-edge check to prevent infinitely nested tag types rejects some valid programs, namely those that look like this:

tag a { ... }
tag b { FOO(a); }

The order of the tag declarations must be switched.

Instead of comparing opaque IDs, we could instead do the following: In the Semant context, store a well-ordering on every tag type. Every time a type /a/ is contained in a type /b/ without boxing, we declare that /a/ < /b/. Then boxed back-pointers from /b/ to /a/ result in opaque types. Any contradiction (declaring that /b/ < /a/ when /a/ < /b/ is already established) results in an error, because a type would have infinite size.

[dherman]

Thank you so much for figuring this out, Patrick. I was pretty frustrated that I couldn't make sense of the problem before, and you cut to the heart of it.

Some clarification that at least helps me: there's a very concrete reason why the ordering and the restriction are necessary. It's not that the type has unbounded size (all trees have unbounded size), nor even that it has infinite size. For example, with the type:

tag list { CONS(int, list); NIL(); }

could still have finite size. CONS(1, CONS(2, CONS(3, NIL()))) is perfectly finite. But the problem is that it doesn't have /statically predictable size/, which is one of the key aspects of the Rust design.

As another example: in a sense, there's nothing inherently worse about the type:

tag void { VOID(void); }

compared to the type:

tag void { VOID(@void); }

Both of them are impossible to instantiate, so neither really threatens any kind of safety properties. But the first type has statically unpredictable size, whereas the second has a static size that can be inductively computed, thanks to the ordering you describe.

So in summary: by imposing a well-ordering on these potentially cyclic types, we recover an inductively defined, static sizeof operation.

[pcwalton]

Fixed in commit bc03c82.