diff options
| -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 +# |