rec_check: expand fragile patterns for clarity#1911
rec_check: expand fragile patterns for clarity#1911gasche wants to merge 1 commit intoocaml:trunkfrom
Conversation
As I was reading the code again I became convinced that there was a mistake in the array-element-type classification code, because it defaults to Paddrarray instead of Pgenarray -- which is the safe default. I had to go through all the cases to convince me that there was no bug (the default cases are all address-only cases), so I propose to spell it out explicitly in the code for clarity.
trefis
left a comment
There was a problem hiding this comment.
I feel like I'm missing something.
| | Tlink _ | Tsubst _ -> | ||
| (* [Typeopt.scrape_ty] starts with [Ctype.expand_head_opt], | ||
| so these cases are impossible *) | ||
| assert false |
There was a problem hiding this comment.
I agree that Tlink can't happen, because repr removes links.
I'm not sure your explanation holds for Tsubst though: try_expand_head_opt will raise Cannot_expand on Tsubsts, which will be caught by expand_head_opt which will then simply return its input (well, after calling repr on it).
Note: I'm not saying Tsubst can happen at this particular place, just that your explanation doesn't convince me.
There was a problem hiding this comment.
Thanks for the review. I don't know much about these internal invariants of the type-checker, and some of the things I wrote there are wishful thinking. It's very good that someone like you who knows more can double-check it. I agree that it's not clear what happens with Tsubst here, what motivated me to include it in the assert false is that other functions of ctype.ml failed on it in the same way.
There was a problem hiding this comment.
and some of the things I wrote there are wishful thinking
Please, don't (ever) do that again.
I agree that it's not clear what happens with
Tsubsthere, what motivated me to include it in theassert falseis that other functions ofctype.mlfailed on it in the same way.
Well, I guess that's because Tsubst can only appear in very few places, and are always (afaict) cleaned up right away.
It seems pretty obvious that your function is never called in these periods of time where Tsubst exists, so assert false is indeed fine.
I'd suggest either removing your comment, or splitting the cases and given a proper explanation to both.
| @@ -169,7 +169,7 @@ let is_ref : Types.value_description -> bool = function | |||
| let scrape env ty = | |||
| (Ctype.repr (Ctype.expand_head_opt env (Ctype.correct_levels ty))).desc | |||
There was a problem hiding this comment.
It's not part of your diff, but that call to repr is useless I believe. (Though it doesn't cost much and makes it easier to reason about the code, so perhaps it's fine to just leave it here).
| | Tpoly(t, _alphas) -> | ||
| (* this case should not occur after [scrape_ty], | ||
| but we handle it defensively *) | ||
| array_element_kind env t |
There was a problem hiding this comment.
Again, I don't understand why. Seems like repr (expand_head_opt (Tpoly(_)) would just be a noop. What am I missing?
|
I'll try to take a look at this next week. |
|
@trefis wrote:
Looking at this again, it seems indeed that my rationale is wrong. Tpoly is removed by scraping, but only the one above the array Note that Which raises the question: why is there this duplication in array-type-classification between (This may have been discussed when we reviewed the new rec-check, apologies for the redundant question.) |
Again, I don't think |
|
This is now superseded by #1922. |
As I was reading the code again I became convinced that there was
a mistake in the array-element-type classification code, because it
defaults to Paddrarray instead of Pgenarray -- which is the safe
default. I had to go through all the cases to convince me that there
was no bug (the default cases are all address-only cases), so
I propose to spell it out explicitly in the code for clarity.
(This small work was done as part of @Cemoixerestre's internship
on the recursive-value static check.)