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

Opened by Patrick Walton at 2010-09-22 01:31:46

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.

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.
Dave Herman at 2010-09-16 05:53:23
Fixed in commit bc03c82c79f4f970eb183cc40eb89f687f8853f5.
Patrick Walton at 2010-09-22 01:31:46