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

Author: Jacques Garrigue

Changes

@@ -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

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;;

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).
+# 

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