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
Interaction between GADTs and polymorphic variants #5724
Comments
Comment author: @garrigue This is a documented limitation of GADTs: types cannot be refined if a pattern-matching contains polymorphic variant. |
Comment author: @yallop It's good to see that the trunk typechecker now accepts the example. |
Comment author: @garrigue Re-open before changing resolution. |
Comment author: @garrigue This is now fixed in trunk, since revision 13221. Here is the corresponding message sent to the caml-list: As you may be aware from past threads, since the introduction of GADTs However, a weakness of this approach was that propagation was disabled At long last I have removed this restriction on the presence of polymorphic
What happens is that inside pattern-matching, only required constructors
During pattern-matching it is not allowed to match on absent type constructors,
In particular the last two points are important, because previously such uses The idea is that allowing propagation of types is more important than |
Original bug ID: 5724
Reporter: @yallop
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:18:42Z)
Resolution: fixed
Priority: normal
Severity: major
Version: 4.00.0
Fixed in version: 4.01.0+dev
Category: ~DO NOT USE (was: OCaml general)
Child of: #5998
Bug description
OCaml reports an error for the last line of the following program:
type _ t =
| A : int t
| B : [`C] -> bool t
let isA (type a) (r : a t) = match r with
| A -> true
| B `C -> false
^^^^
Error: This pattern matches values of type bool t
but a pattern was expected which matches values of type int t
If the `C in the pattern is replaced with an underscore, the program is accepted.
The text was updated successfully, but these errors were encountered: