Bundle the kind with the con

[nomeata]

The benefit is that many passes no longer need to keep a con_env
around, and many operations in Type are now always available, in
partiuclar Type.as_*_sub, promote etc.

The downside is that, because of the multi-pass approach in typing.ml, the
annotation needs to be a kind ref.

I tried using a promise, but it seems that certain things are run more
than once in typing (the same has caused issues with recoverable error
messages before). I am not sure if this is avoidable.

If maybe the initialization can be made a bit cleaner in typing, then
I think this will improve the life of those working on the Ir
noticably.

[rossberg]

Generally this seems like a workable direction to me, though there perhaps is potential for a simpler solution. In particular, it seems that one of two choices should be possible:

1. Instead of introducing the new Type.con, put the kind directly on typ's Con constructor. That makes clear that it is only a use-site annotation.

2. Or use Type.con throughout and eliminate con_env altogether. Then a con is annotated everywhere. In that case, I would probably change Con.t to 'a Con.t, such that the kind can become a proper part of the existing con.

Another way to put this is that it makes sense to have either Type.con or con_env, but having both seems redundant.

[rossberg]

It would be cleaner to make the kind a parameter than to hardwire a Pre in here. Would save a few spurious assignments, too.

[crusso]

Stale comment mentions a promise...

[nomeata]

Yes, this was a hold-over from when I tried using a promise. Which would be so much cleaner…

I think the problem is that infer_dec_typdecs is run multiple times, and there is no good time when we can do a single fulfill.

I have pushed a commit that makes the ref a bit promise-like, in that it only allows going from a Pre-type to a non-pre-type once, and then complains if something wants to set the kind a second time with a different non-pre-type. But I am not sure if it is worth the bother, and can easily revert d5baf2b.

[crusso]

Looks good to me but I've had a few beers

[nomeata]

1. Instead of introducing the new Type.con, put the kind directly on typ's Con constructor. That makes clear that it is only a use-site annotation.

This makes very much sense in terms of the types, but it is harder with the the delayed determination of kinds in open_binds and in typing. A ref is (unfortunately :-() more convenient for the late assignments. (One could put a ref in the occurrences, but this has issues again with passes that have to traverse all types, such as async).

2. Or use Type.con throughout and eliminate con_env altogether. Then a con is annotated everywhere. In that case, I would probably change Con.t to 'a Con.t, such that the kind can become a proper part of the existing con.

That is a reasonable refactoring over what we have right now. If you are happy with this change semantic-wise, I’ll do that refactoring.

Although: There is a function avoid that takes two con_env. What does it do? How would it work in a world without con_env? (It is the only function in type.mli that still takes a con_env.)

[rossberg]

1. Instead of introducing the new Type.con, put the kind directly on typ's Con constructor. That makes clear that it is only a use-site annotation.

This makes very much sense in terms of the types, but it is harder with the the delayed determination of kinds in open_binds and in typing. A ref is (unfortunately :-() more convenient for the late assignments. (One could put a ref in the occurrences, but this has issues again with passes that have to traverse all types, such as async).

Well, it would still be a ref, just elsewhere.

1. Or use Type.con throughout and eliminate con_env altogether. Then a con is annotated everywhere. In that case, I would probably change Con.t to 'a Con.t, such that the kind can become a proper part of the existing con.

That is a reasonable refactoring over what we have right now. If you are happy with this change semantic-wise, I’ll do that refactoring.

Although: There is a function avoid that takes two con_env. What does it do? How would it work in a world without con_env? (It is the only function in type.mli that still takes a con_env.)

Avoid tries to expand local type defs when they go out of scope. I think after this change it would have to work with a typ_env as input and denote the corresponding cons through that. (It really only needs a con set.)

Can you implement one of these before landing?

[nomeata]

Well, it would still be a ref, just elsewhere.

What I mean is: With a ref at the binding site, there is a single place to update the ref once. With the ref only at all occurences, then it is hard to avoid updating it multiple times (which is bad when the modification is not idempotent, or might not terminate with recursive definitions.

Avoid tries to expand local type defs when they go out of scope. I think after this change it would have to work with a typ_env as input and denote the corresponding cons through that. (It really only needs a con set.)

Ok, that is roughly what I expected, including that a con_set ought to be enough. Is this just a best-effort thing for better error messages?

BTW, this loops in avoid (reported in #170):

{ type Rec = ?Rec; (null : Rec) };

Can you implement one of these before landing?

Yes, sure (the second, though).

[nomeata]

Can you implement one of these before landing?

Refactoring done. It is unclear whether the fact that the annotation of a Con.t is mutable should be determined in con.ml or in type.ml.

Changed have been made since Claudio’s review.

[rossberg]

Hm, you already got my review a couple of hours ago. ;)

[nomeata]

Hm, you already got my review a couple of hours ago. ;)

Eh, where? I am confused. Did you actually submit the review, or maybe just add the comments? In any case I am expecting GitHub to say “Andreas requested changes” or “Andreas approves the PR”.

[rossberg]

Oops, sorry, I forgot to click the Submit button. (It's confusing that GH already shows the comments on the conversation page for me.)

[crusso]

@rossberg shall I merge?

[rossberg]

Go for it!

[nomeata]

Whoohoo

[matthewhammer]

👏 👏