summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJacques Garrigue <garrigue at math.nagoya-u.ac.jp>2013-09-05 08:25:30 +0000
committerJacques Garrigue <garrigue at math.nagoya-u.ac.jp>2013-09-05 08:25:30 +0000
commit7185e693f52e03406d38ddc99dea9624742e610b (patch)
tree8a078cd2d22eee6bd0ac43747f587402a5ae237e
parentfe6ff6a0337125d5286ea33be9722487c5568776 (diff)
downloadocaml-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.ml9
-rw-r--r--testsuite/tests/typing-gadts/pr6158.ml.principal.reference19
-rw-r--r--testsuite/tests/typing-gadts/pr6158.ml.reference15
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
+#