Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

type_cases: propagate refined ty_arg to Parmatch checks #1583

Merged
merged 5 commits into from Jan 31, 2018

Conversation

Projects
None yet
4 participants
@trefis
Copy link
Contributor

trefis commented Jan 25, 2018

This PR actually does a bit more than what the title says:

  • the first commit is an unrelated (hopefully trivial) cleanup
  • the second commit is a small refactoring which hopefully should clarify why unify_pats (instance env ty_arg) was called when propagate || erased_either. If I understood correctly, the condition is slightly off: we have to unify_pats (instance env ty_arg) when we've typechecked the patterns with a partial instance of ty_arg as expected type. But, in general, I don't think we need to when propagate is true.
  • the 3rd commit is not required, but feels "more correct" than the current situation.
  • the remaining commits actually concern themselves with what the title of the GPR mentions.

Context:
After having typed all the clauses of a match, we do various checks (usefulness, exhaustivity, ...) which work by producing "values" which can (or not) be matched by the clauses of the match.
During that process, we typecheck the values produced to make sure they are of the same type as the scrutiny/patterns.

However, the type we expect these values to have is the ty_arg that has flowed into type_cases, ignoring some new information which might have been gained by typing the patterns.
Consider:

type (_,_) eq = Refl : ('a, 'a) eq

type empty = (int, string) eq

let f () =
  match None with
  | (None : empty option) -> ()

The match is currently flagged as non-exhaustive.

If we somehow propagated the information we got from typechecking the pattern, then we would notice that the match actually is exhaustive.
Notice that this is what happens (through a side channel) here:

let f x =
  match x with
  | (None : empty option) -> ()

which doesn't trigger the warning.
The 4th commit adds other similar examples.

The last commit does the suggested change: instead of using an instance of the original ty_arg for typing the productions of Parmatch, we use an instance of ty_arg' (which has been unified with all the patterns as well as with an instance of type_arg, so all the information has been gathered).

@trefis trefis requested a review from garrigue Jan 25, 2018

@garrigue
Copy link
Contributor

garrigue left a comment

This seems mostly fine, but please revert changes in ctype, and at line 4690 of typecore.

@@ -716,8 +716,7 @@ let rec update_level env level expand ty =
with Cannot_expand ->
(* +++ Levels should be restored... *)
(* Format.printf "update_level: %i < %i@." level (get_level env p); *)
if level < get_level env p then raise (Unify [(ty, newvar2 level)]);

This comment has been minimized.

@garrigue

garrigue Jan 30, 2018

Contributor

I would rather you do not mix changes to Ctype here, as this is completely irrelevant.
As a side note, I'm doing the same change (which seems indeed OK) in #1588, where it is relevant.

This comment has been minimized.

@trefis

trefis Jan 30, 2018

Author Contributor

Done.

@@ -4583,6 +4583,10 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
match caselist with
[{pc_lhs}] when is_var pc_lhs -> false
| _ -> true in
let partial =

This comment has been minimized.

@garrigue

garrigue Jan 30, 2018

Contributor

This hoisting seems fine, but may be confusing, as this is unrelated to the partial at the end of the function.

This comment has been minimized.

@trefis

trefis Jan 30, 2018

Author Contributor

Fair point. I renamed this to take_partial_instance, that should be enough to avoid any confusion.

@@ -4630,7 +4631,7 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
(* `Contaminating' unifications start here *)
List.iter (fun f -> f()) !pattern_force;
(* Post-processing and generalization *)
if propagate || erase_either then unify_pats (instance env ty_arg);
if partial <> None then unify_pats (instance env ty_arg);

This comment has been minimized.

@garrigue

garrigue Jan 30, 2018

Contributor

This seems OK too, but it only works because there is the unify_pats ty_arg' above. I.e. ty_arg may be really polymorphic.
I would also add a generalize ty_arg' at line 4639, i.e. just after generalizing patl, to be sure that this specific version has proper levels (it has been unified with the patterns in patl, but might still be subtly different).

This comment has been minimized.

@trefis

trefis Jan 30, 2018

Author Contributor

Fair point, I added the suggested call to generalize.

Subst.type_expr (Subst.for_saving Subst.identity) ty_arg
else ty_arg
Subst.type_expr (Subst.for_saving Subst.identity) ty_arg'
else ty_arg'

This comment has been minimized.

@garrigue

garrigue Jan 30, 2018

Contributor

This makes sense.

in
let partial =
if partial_flag then
check_partial ~lev env ty_arg_check loc cases
check_partial ~lev env (instance env ty_arg_check) loc cases

This comment has been minimized.

@garrigue

garrigue Jan 30, 2018

Contributor

Due to the end_def at line 4611, we are no longer at the same level as when the patterns were typed.
I suggest keeping ty_arg_check rather than an instance of it. This is perfectly fine from the point of view of levels.

This comment has been minimized.

@trefis

trefis Jan 30, 2018

Author Contributor

I agree with the first part.
I did the change only because it seemed to me that, except here, we never pass an expected type which might be general to type_pat. But this might be purely incidental.

Can you comment on that point before I revert the change as per your suggestion?

This comment has been minimized.

@garrigue

garrigue Jan 30, 2018

Contributor

I'm not sure this is the only case, but you are right that expected_ty is not handled as a type scheme in type_pat. I do not see any problem with doing that here, as the type is a fresh copy, and by unification its levels will be lowered. It might be cleaner to take an instance at an higher level.

This comment has been minimized.

@trefis

trefis Jan 30, 2018

Author Contributor

When you say "by unification its levels will be lowered" I think you mean that they will be lowered to the current level (that is, the one at which check_partial is called).
Wouldn't that be equivalent to taking an instance at that same level before calling check_partial?

It might be cleaner to take an instance at an higher level.

Assuming that "higher" means "deeper", I don't understand why you'd want to do that in this case.

This comment has been minimized.

@garrigue

garrigue Jan 31, 2018

Contributor

Strictly speaking, this is the levels in the type it is unified to.
But looking more carefully, I think you are right: at this point type_pat does not contain nested calls to begin_def, so the levels in the generated type will indeed be the level at which type_pat is called. So taking an instance should be OK.

@trefis trefis force-pushed the trefis:propagate_ty_arg_to_check branch from 2b4cb82 to 5a50aec Jan 30, 2018

@garrigue
Copy link
Contributor

garrigue left a comment

This looks fine now.

@trefis trefis force-pushed the trefis:propagate_ty_arg_to_check branch from 5a50aec to e78a7a5 Jan 31, 2018

@trefis trefis merged commit 3fec4c8 into ocaml:trunk Jan 31, 2018

0 of 2 checks passed

continuous-integration/appveyor/pr Waiting for AppVeyor build to complete
Details
continuous-integration/travis-ci/pr The Travis CI build is in progress
Details
@trefis

This comment has been minimized.

Copy link
Contributor Author

trefis commented Jan 31, 2018

I rebased and squashed the commits implementing the suggested changes in the original commits before merging.

Thanks for the review!

@trefis trefis deleted the trefis:propagate_ty_arg_to_check branch Jan 31, 2018

@shindere

This comment has been minimized.

Copy link
Contributor

shindere commented Feb 1, 2018

@trefis The test in testsuite/tests/typing-warnings/inside_out.ml does not
pass on my machine. Is it expected to fail?

@trefis

This comment has been minimized.

Copy link
Contributor Author

trefis commented Feb 1, 2018

It is not expected to fail. I just rechecked on trunk to make sure, and it still passes on my machine.

Can you give some more information: what the result is for you, etc.

@gasche

This comment has been minimized.

Copy link
Member

gasche commented Feb 2, 2018

@shindere you may need to rebuild expect to notice the type-checker changes; cd testsuite && make clean && make lib tools.

@shindere

This comment has been minimized.

Copy link
Contributor

shindere commented Feb 2, 2018

@shindere

This comment has been minimized.

Copy link
Contributor

shindere commented Feb 2, 2018

@trefis

This comment has been minimized.

Copy link
Contributor Author

trefis commented Feb 6, 2018

By the way, doesn't this indicate that there is a problem with the Makefiles?
Ping @diml who is (I believe) the author of expect.

@shindere

This comment has been minimized.

Copy link
Contributor

shindere commented Feb 6, 2018

@gasche

This comment has been minimized.

Copy link
Member

gasche commented on 1b670fb Mar 19, 2018

@trefis with this commit the inside_out test file does not make sense anymore: it was there to observe wrong negatives you wanted to fix, and they are now all fixed, but they keep the comments saying "warning", "error" while they actually work fine. Could we remove it now?

This comment has been minimized.

Copy link
Contributor Author

trefis replied Mar 19, 2018

Remove the comments or the whole file?

This comment has been minimized.

Copy link
Member

gasche replied Mar 20, 2018

Indeed, removing the comments sounds nicer, but then maybe you could add some explanation as to why a file full of sentences that pass without any warnings or errors is present in typing-warnings.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.