Improve GADT typing with or-clauses #7091
Description
Original bug ID: 7091
Reporter: @Chris00
Assigned to: @garrigue
Status: assigned (set by @alainfrisch on 2017-02-22T16:15:15Z)
Resolution: open
Priority: normal
Severity: feature
Platform: x86_64
OS: GNU/Linux
OS Version: Debian testing
Target version: undecided
Category: typing
Duplicate of: #7319
Monitored by: runhang @hcarty @Chris00
Bug description
# type 'a a = A : int a | B : float a | C : int a;;
# let f : type v. v a -> int = function A -> 1 | B -> 2 | C -> 1;;
val f : 'v a -> int = <fun>
works fine. However:
# let f : type v. v a -> int = function A | C -> 1 | B -> 2;;
Characters 38-39:
let f : type v. v a -> int = function A | C -> 1 | B -> 2;;
^
Error: This pattern matches values of type int a
but a pattern was expected which matches values of type v a
Type int is not compatible with type v
This is rather surprising and should be fixed if possible (at least the error which really points in the wrong direction).