-
Notifications
You must be signed in to change notification settings - Fork 1.1k
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
Fix #10907: Wrong type inferred from existential types #10959
Changes from 1 commit
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -111,24 +111,6 @@ Warning 8 [partial-match]: this pattern-matching is not exhaustive. | |
Here is an example of a case that is not matched: | ||
Some A | ||
val g : 'a M.j t option -> unit = <fun> | ||
|}, Principal{| | ||
module M : | ||
sig | ||
type 'a d | ||
type i = < m : 'c. 'c -> 'c d > | ||
type 'a j = < m : 'c. 'c -> 'a > | ||
end | ||
type _ t = A : M.i t | ||
File "_none_", line 1: | ||
Warning 18 [not-principal]: typing this pattern requires considering $0 and 'c M.d as equal. | ||
But the knowledge of these types is not principal. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Note: this is an example of a principality warning that was raised during exhaustivity analysis, on a sub-case of an "exploded" wildcard pattern. The dummy location (File "none", line 1) comes from the dummy location used by parmatch when exploding wildcard partterns. I believe that the change in this testsuite result does not come from the lowering of levels (the actual type-checking change in the PR), but simply from the fact that we now silence this warning during exhaustivity analysis. (We silenced them because our behavior change would raise those warnings very often in this situation.) It's interesting that it already occurred in the wild. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Indeed, it purely comes from my turning off the warning on counter-examples. |
||
Line 9, characters 2-20: | ||
9 | let None = y in () ;; | ||
^^^^^^^^^^^^^^^^^^ | ||
Warning 8 [partial-match]: this pattern-matching is not exhaustive. | ||
Here is an example of a case that is not matched: | ||
Some A | ||
val g : 'a M.j t option -> unit = <fun> | ||
|}] | ||
|
||
(* more examples by @lpw25 *) | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,53 @@ | ||
(* TEST | ||
* expect | ||
*) | ||
|
||
(* from @dyzsr *) | ||
type 'a t = T : ('a -> 'b) * ('b -> 'a) -> 'a t;; | ||
[%%expect{| | ||
type 'a t = T : ('a -> 'b) * ('b -> 'a) -> 'a t | ||
|}] | ||
|
||
let t = T ((fun x -> x), (fun x -> x));; | ||
[%%expect{| | ||
val t : 'a t = T (<fun>, <fun>) | ||
|}] | ||
|
||
let t1 = let T (g, h) = t in h (g 1);; | ||
[%%expect{| | ||
val t1 : int = 1 | ||
|}] | ||
|
||
let f x = let T (g, h) = t in h (g x);; | ||
[%%expect{| | ||
val f : 'a -> 'a = <fun> | ||
|}] | ||
|
||
(* reformulation by @gasche *) | ||
|
||
(* an isomorphism between 'a and 'b *) | ||
type ('a, 'b) iso = ('a -> 'b) * ('b -> 'a) | ||
|
||
(* exists 'b. ('a, 'b) iso *) | ||
type 'a some_iso = Iso : ('a, 'b) iso -> 'a some_iso | ||
[%%expect{| | ||
type ('a, 'b) iso = ('a -> 'b) * ('b -> 'a) | ||
type 'a some_iso = Iso : ('a, 'b) iso -> 'a some_iso | ||
|}] | ||
|
||
(* forall 'a. exists 'b. ('a, 'b) iso *) | ||
let t : 'a . 'a some_iso = | ||
Iso ((fun x -> x), (fun x -> x)) | ||
[%%expect{| | ||
val t : 'a some_iso = Iso (<fun>, <fun>) | ||
|}] | ||
|
||
let unsound_cast : 'a 'b. 'a -> 'b = fun x -> | ||
match t with Iso (g, h) -> h (g x) | ||
[%%expect{| | ||
Lines 1-2, characters 37-36: | ||
1 | .....................................fun x -> | ||
2 | match t with Iso (g, h) -> h (g x) | ||
Error: This definition has type 'c. 'c -> 'c which is less general than | ||
'a 'b. 'a -> 'b | ||
|}] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nitpick: There is an extra
*
at the end. Is this muscle-memory due to writing too many comments? (I would expect François Pottier to make these typos out of habit, but not Jacques :-D)There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Well, this PR is pretty short, and it still includes a comment (in a mli, I admit), so this is not so true :-)