Last active
August 29, 2015 14:18
-
-
Save vogler/e6ba1a0878cb7cbbb64c to your computer and use it in GitHub Desktop.
subtyping of polymorphic variants when using GADTs
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
type 'r t = A : [`A | `T] t | B : [`B | `T] t;; (* the information 'r : [> `T] seems to be missing *) | |
(* type _ t = A : [ `A | `T ] t | B : [ `B | `T ] t *) | |
(* the following works as expected: *) | |
let rec f : type r. r t -> r = function A -> `T | B -> `T;; | |
(* val f : 'r t -> 'r = <fun> *) | |
f A;; | |
(* - : [ `A | `T ] = `T *) | |
(* now f should be called on different modules for the same q, and the results should be combined *) | |
let rec g : type r. r t -> r = fun q -> let h a s = f q in List.fold_left h `T [1;2;3];; | |
(* Error: This expression has type [> `T ] | |
but an expression was expected of type r *) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment