Conversation
0a2d93b to
d7edc97
Compare
garrigue
left a comment
There was a problem hiding this comment.
Globally, this looks correct. However, I'm wondering what should be returned in pat_type. We seem to have an invariant to keep it non-generic, but wouldn't it make sense to just always put the (generalized) expected_ty, from a semantical point of view?
| in | ||
| let loc = sp.ppat_loc in | ||
| let rup k x = | ||
| if constrs = None then (ignore (rp x)); |
There was a problem hiding this comment.
You record the type of the pattern before unification with the expected type.
This is a change w.r.t. the previous behavior.
Is this intentional?
There was a problem hiding this comment.
Sorry, looking at what does Stypes.record, you are just registering the node earlier, and unification can still occur afterwards. So one has more information if the next unification fails, and the same otherwise. Fine.
| begin_def (); | ||
| let expected_ty = instance expected_ty in | ||
| end_def (); | ||
| generalize_structure expected_ty; |
There was a problem hiding this comment.
Here it should be OK to use generalize: since we are matching a value, different members could be seen as using independent instances.
There was a problem hiding this comment.
I don't think it makes a difference here: expected_ty doesn't contain any type variable at the generic level when we receive it. Which means that after the
begin_def;
instance;
end_def;
sequence, there won't be any generalizable variables.
Given that, I'd rather keep the call to generalize_structure here, for uniformity.
There was a problem hiding this comment.
Oh, I see. I hadn't seen that due to the generalize_structure in type_cases, there are no generalized type variables in the type.
This would change if switch later to a more agressive policy of taking full instances, that could be fully generalized soundly.
But then it seems that the only improvement of the current patch is to avoid some warnings with label/constructor disambiguation. Is there any other practical change?
| generalize_structure expected_ty; | ||
| generalize_structure ty_res; | ||
| List.iter generalize_structure ty_args; | ||
|
|
There was a problem hiding this comment.
Here the sharing of type variables is needed, so this indeed has to be generalize_structure.
|
Thanks for the review. I haven't had time to think much about the question you ask (or to fix the small issues in the code) yet, but I'll get back to you some time next week. |
|
I'm copying here an inline comment, as it might no be very visible: Since, in As a result, it seems that the only improvement of the current patch is to avoid some warnings with label/constructor disambiguation. Is there any other practical change? |
|
I haven't actually tested it with this version of the patch, but I think it should address ambiguity errors like this one: # type 'a r = { a : 'a; b: 'a };;
type 'a r = { a : 'a; b : 'a; }
# type 'a ty = Int : int ty | Float : float ty;;
type 'a ty = Int : int ty | Float : float ty
# let foo (type a) (ty : a ty) (x : a r) =
match ty, x with
| Int, { a = 3; b } -> b
| _ -> assert false;; |
Indeed, that's the test I add with my first commit: at that time it still complains that the type of
The practical change is illustrated in the test suite by the example Leo just repeated. I plan to open a new PR containing (only) the changes relating to principality warnings as a follow up to this PR. |
Perhaps. Although I think putting the instance makes just as much sense? |
|
My comment concerning whether For now I'm satisfied with the current PR, which keeps all invariants, and so is safe. |
4a3c5f3 to
f658de3
Compare
|
Understood. Thanks for looking at this! I've now rebased and squashed the commits, I'll merge once the CIs are happy (hopefully appveyor won't time out this time). |
f658de3 to
d931b9c
Compare
Extracts the least controversial part #1675 .