diff options
author | Jacques Garrigue <garrigue at math.nagoya-u.ac.jp> | 2013-09-05 08:25:30 +0000 |
---|---|---|
committer | Jacques Garrigue <garrigue at math.nagoya-u.ac.jp> | 2013-09-05 08:25:30 +0000 |
commit | 7185e693f52e03406d38ddc99dea9624742e610b (patch) | |
tree | 8a078cd2d22eee6bd0ac43747f587402a5ae237e | |
parent | fe6ff6a0337125d5286ea33be9722487c5568776 (diff) | |
download | ocaml-7185e693f52e03406d38ddc99dea9624742e610b.tar.gz |
Fix PR#6158
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@14062 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
-rw-r--r-- | testsuite/tests/typing-gadts/pr6158.ml | 9 | ||||
-rw-r--r-- | testsuite/tests/typing-gadts/pr6158.ml.principal.reference | 19 | ||||
-rw-r--r-- | testsuite/tests/typing-gadts/pr6158.ml.reference | 15 |
3 files changed, 43 insertions, 0 deletions
diff --git a/testsuite/tests/typing-gadts/pr6158.ml b/testsuite/tests/typing-gadts/pr6158.ml new file mode 100644 index 0000000000..752380cb37 --- /dev/null +++ b/testsuite/tests/typing-gadts/pr6158.ml @@ -0,0 +1,9 @@ +type 'a t = T of 'a +type 'a s = S of 'a + +type (_, _) eq = Refl : ('a, 'a) eq;; + +let f : (int s, int t) eq -> unit = function Refl -> ();; + +module M (S : sig type 'a t = T of 'a type 'a s = T of 'a end) = +struct let f : ('a S.s, 'a S.t) eq -> unit = function Refl -> () end;; diff --git a/testsuite/tests/typing-gadts/pr6158.ml.principal.reference b/testsuite/tests/typing-gadts/pr6158.ml.principal.reference new file mode 100644 index 0000000000..e7d5458744 --- /dev/null +++ b/testsuite/tests/typing-gadts/pr6158.ml.principal.reference @@ -0,0 +1,19 @@ + +# type 'a t = T of 'a +type 'a s = S of 'a +type (_, _) eq = Refl : ('a, 'a) eq +# Characters 46-50: + let f : (int s, int t) eq -> unit = function Refl -> ();; + ^^^^ +Error: This pattern matches values of type (int s, int s) eq + but a pattern was expected which matches values of type + (int s, int t) eq + Type int s is not compatible with type int t +# Characters 120-124: + struct let f : ('a S.s, 'a S.t) eq -> unit = function Refl -> () end;; + ^^^^ +Error: This pattern matches values of type (ex#0 S.s, ex#1 S.t) eq + but a pattern was expected which matches values of type + (ex#0 S.s, ex#0 S.t) eq + The type constructor ex#0 would escape its scope +# diff --git a/testsuite/tests/typing-gadts/pr6158.ml.reference b/testsuite/tests/typing-gadts/pr6158.ml.reference new file mode 100644 index 0000000000..c7d5c1eca8 --- /dev/null +++ b/testsuite/tests/typing-gadts/pr6158.ml.reference @@ -0,0 +1,15 @@ + +# type 'a t = T of 'a +type 'a s = S of 'a +type (_, _) eq = Refl : ('a, 'a) eq +# Characters 46-50: + let f : (int s, int t) eq -> unit = function Refl -> ();; + ^^^^ +Error: This pattern matches values of type (int s, int s) eq + but a pattern was expected which matches values of type + (int s, int t) eq + Type int s is not compatible with type int t +# module M : + functor (S : sig type 'a t = T of 'a type 'a s = T of 'a end) -> + sig val f : (a#0 S.s, a#0 S.t) eq -> unit end +# |