diff options
| author | Jacques Garrigue <garrigue at math.nagoya-u.ac.jp> | 2015-09-18 09:55:18 +0000 |
|---|---|---|
| committer | Jacques Garrigue <garrigue at math.nagoya-u.ac.jp> | 2015-09-18 09:55:18 +0000 |
| commit | f5bf4bdce139a01861d9614d000f70eb4b2d6b68 (patch) | |
| tree | ef66de25c0831cd3a99cfc33a223598432707c33 | |
| parent | affb539deaa07a028d78b07e0eb29eb6bbe5d919 (diff) | |
| download | ocaml-f5bf4bdce139a01861d9614d000f70eb4b2d6b68.tar.gz | |
Fix PR#6993: allow recursive types when doing unification on GADT indices
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@16426 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
| -rw-r--r-- | Changes | 1 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/pr6993_bad.ml | 12 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/pr6993_bad.ml.reference | 13 | ||||
| -rw-r--r-- | typing/ctype.ml | 7 |
4 files changed, 31 insertions, 2 deletions
@@ -178,6 +178,7 @@ Bug fixes: - PR#6982: unexpected type error when packing a module alias - PR#6985: `module type of struct include Bar end exposes %s#row when Bar contains private row types +- PR#6993: Segfault from recursive modules violating exhaustiveness assumptions - GPR#205: Clear caml_backtrace_last_exn before registering as root (report and fix by Frederic Bour) - GPR#220: minor -dsource error on recursive modules diff --git a/testsuite/tests/typing-gadts/pr6993_bad.ml b/testsuite/tests/typing-gadts/pr6993_bad.ml new file mode 100644 index 0000000000..122b50f33b --- /dev/null +++ b/testsuite/tests/typing-gadts/pr6993_bad.ml @@ -0,0 +1,12 @@ +type (_, _) eqp = Y : ('a, 'a) eqp | N : string -> ('a, 'b) eqp +let f : ('a list, 'a) eqp -> unit = function N s -> print_string s;; + +module rec A : sig type t = B.t list end = + struct type t = B.t list end +and B : sig type t val eq : (B.t list, t) eqp end = + struct + type t = A.t + let eq = Y + end;; + +f B.eq;; diff --git a/testsuite/tests/typing-gadts/pr6993_bad.ml.reference b/testsuite/tests/typing-gadts/pr6993_bad.ml.reference new file mode 100644 index 0000000000..cda1b16a47 --- /dev/null +++ b/testsuite/tests/typing-gadts/pr6993_bad.ml.reference @@ -0,0 +1,13 @@ + +# Characters 100-130: + let f : ('a list, 'a) eqp -> unit = function N s -> print_string s;; + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +Y +type (_, _) eqp = Y : ('a, 'a) eqp | N : string -> ('a, 'b) eqp +val f : ('a list, 'a) eqp -> unit = <fun> +# module rec A : sig type t = B.t list end +and B : sig type t val eq : (B.t list, t) eqp end +# Exception: Match_failure ("//toplevel//", 2, 36). +# diff --git a/typing/ctype.ml b/typing/ctype.ml index 62a2ecad87..a83e34c80e 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -1652,9 +1652,12 @@ let correct_abbrev env path params ty = exception Occur +let allow_recursive env ty = + (!Clflags.recursive_types || !umode = Pattern) && is_contractive env ty + let rec occur_rec env visited ty0 ty = if ty == ty0 then raise Occur; - let occur_ok = !Clflags.recursive_types && is_contractive env ty in + let occur_ok = allow_recursive env ty in match ty.desc with Tconstr(p, tl, abbrev) -> begin try @@ -1669,7 +1672,7 @@ let rec occur_rec env visited ty0 ty = match ty'.desc with Tobject _ | Tvariant _ -> () | _ -> - if not (!Clflags.recursive_types && is_contractive env ty') then + if not (allow_recursive env ty') then iter_type_expr (occur_rec env (ty'::visited) ty0) ty' with Cannot_expand -> if not occur_ok then raise Occur |