Fix #7902: Type-checker infers a recursive type, even though -rectype… (#9556)

Changes

@@ -604,6 +604,9 @@ OCaml 4.11
 - #7817, #9546: Unsound inclusion check for polymorphic variant
   (Jacques Garrigue, report by Mikhail Mandrykin, review by Gabriel Scherer)
 
+- #7902, #9556: Type-checker infers recursive type, eventhough -rectypes is off.
+  (Jacques Garrigue, report by Francois Pottier, review by Leo White)
+
 - #7917, #9426: Use GCC option -fexcess-precision=standard when available,
   avoiding a problem with x87 excess precision in Float.round.
   (Xavier Leroy, review by Sébastien Hinderer)

testsuite/tests/typing-gadts/pr6174.ml

@@ -11,5 +11,5 @@ Line 3, characters 24-25:
 3 |  fun C k -> k (fun x -> x);;
                             ^
 Error: This expression has type $0 but an expression was expected of type
-         $1 = ($2 -> $1) -> $1
+         $1 = o
 |}];;

testsuite/tests/typing-gadts/pr7016.ml

@@ -24,8 +24,6 @@ let get1' = function
   | (Cons (x, _) : (_ * 'a, 'a) t) -> x
   | Nil -> assert false ;; (* ok *)
 [%%expect{|
-val get1' : ('b * 'a as 'a, 'a) t -> 'b = <fun>
-|}, Principal{|
 Line 3, characters 4-7:
 3 |   | Nil -> assert false ;; (* ok *)
         ^^^

testsuite/tests/typing-gadts/pr7374.ml

@@ -29,16 +29,22 @@ Error: This expression has type (a, a) eq
        Type a is not compatible with type t = [ `Rec of 'a ] X.t as 'a
 |}]
 
-(* trigger segfault
+(* Trigger the unsoundness if Fix were definable *)
 module Id = struct
   type 'a t = 'b constraint 'a = [ `Rec of 'b ]
 end
-
 module Bad = Fix(Id)
-
-let segfault () =
-  print_endline (cast (trans (Bad.uniq Refl) (Bad.uniq Refl)) 0)
-*)
+let magic : type a b. a -> b =
+  fun x ->
+    let Refl = (Bad.uniq Refl : (a,Bad.t) eq) in
+    let Refl = (Bad.uniq Refl : (b,Bad.t) eq) in x
+[%%expect{|
+module Id : sig type 'a t = 'b constraint 'a = [ `Rec of 'b ] end
+Line 4, characters 13-16:
+4 | module Bad = Fix(Id)
+                 ^^^
+Error: Unbound module Fix
+|}]
 
 (* addendum: ensure that hidden paths are checked too *)
 module F (X : sig type 'a t end) = struct

testsuite/tests/typing-gadts/pr7902.ml

@@ -0,0 +1,41 @@
+(* TEST
+   * expect
+*)
+
+type ('a, 'b) segment =
+  | SegNil : ('a, 'a) segment
+  | SegCons : ('a * 'a, 'b) segment -> ('a, 'b) segment
+
+let color : type a b . (a, b) segment -> int = function
+  | SegNil -> 0
+  | SegCons SegNil -> 0
+  | SegCons _ -> 0
+[%%expect{|
+type ('a, 'b) segment =
+    SegNil : ('a, 'a) segment
+  | SegCons : ('a * 'a, 'b) segment -> ('a, 'b) segment
+val color : ('a, 'b) segment -> int = <fun>
+|}]
+
+(* Fail *)
+let color (* : type a b . (a, b) segment -> int *) = function
+  | SegNil -> 0
+  | SegCons SegNil -> 0
+  | SegCons _ -> 0
+[%%expect{|
+Line 3, characters 12-18:
+3 |   | SegCons SegNil -> 0
+                ^^^^^^
+Error: This pattern matches values of type ('a * 'a, 'a * 'a) segment
+       but a pattern was expected which matches values of type
+         ('a * 'a, 'a) segment
+       The type variable 'a occurs inside 'a * 'a
+|}, Principal{|
+Line 3, characters 4-18:
+3 |   | SegCons SegNil -> 0
+        ^^^^^^^^^^^^^^
+Error: This pattern matches values of type ('a, 'a * 'a) segment
+       but a pattern was expected which matches values of type
+         ('a, 'a) segment
+       The type variable 'a occurs inside 'a * 'a
+|}]

typing/ctype.ml

@@ -304,12 +304,15 @@ type unification_mode =
 let umode = ref Expression
 let generate_equations = ref false
 let assume_injective = ref false
+let allow_recursive_equation = ref false
 
-let set_mode_pattern ~generate ~injective f =
+let set_mode_pattern ~generate ~injective ~allow_recursive f =
   Misc.protect_refs
-    [Misc.R (umode, Pattern);
-     Misc.R (generate_equations, generate);
-     Misc.R (assume_injective, injective)] f
+    [ Misc.R (umode, Pattern);
+      Misc.R (generate_equations, generate);
+      Misc.R (assume_injective, injective);
+      Misc.R (allow_recursive_equation, allow_recursive);
+    ] f
 
 (*** Checks for type definitions ***)
 
@@ -1796,7 +1799,8 @@ let type_changed = ref false (* trace possible changes to the studied type *)
 let merge r b = if b then r := true
 
 let occur env ty0 ty =
-  let allow_recursive = !Clflags.recursive_types || !umode = Pattern  in
+  let allow_recursive =
+    !Clflags.recursive_types || !umode = Pattern && !allow_recursive_equation in
   let old = !type_changed in
   try
     while
@@ -1819,18 +1823,18 @@ let occur_in env ty0 t =
 (* PR#6992: we actually need it for contractiveness *)
 (* This is a simplified version of occur, only for the rectypes case *)
 
-let rec local_non_recursive_abbrev strict visited env p ty =
+let rec local_non_recursive_abbrev ~allow_rec strict visited env p ty =
   (*Format.eprintf "@[Check %s =@ %a@]@." (Path.name p) !Btype.print_raw ty;*)
   let ty = repr ty in
   if not (List.memq ty visited) then begin
     match ty.desc with
       Tconstr(p', args, _abbrev) ->
         if Path.same p p' then raise Occur;
-        if not strict && is_contractive env p' then () else
+        if allow_rec && not strict && is_contractive env p' then () else
         let visited = ty :: visited in
         begin try
           (* try expanding, since [p] could be hidden *)
-          local_non_recursive_abbrev strict visited env p
+          local_non_recursive_abbrev ~allow_rec strict visited env p
             (try_expand_head try_expand_once_opt env ty)
         with Cannot_expand ->
           let params =
@@ -1840,19 +1844,24 @@ let rec local_non_recursive_abbrev strict visited env p ty =
           List.iter2
             (fun tv ty ->
               let strict = strict || not (is_Tvar (repr tv)) in
-              local_non_recursive_abbrev strict visited env p ty)
+              local_non_recursive_abbrev ~allow_rec strict visited env p ty)
             params args
         end
+    | Tobject _ | Tvariant _ when not strict ->
+        ()
     | _ ->
-        if strict then (* PR#7374 *)
+        if strict || not allow_rec then (* PR#7374 *)
           let visited = ty :: visited in
-          iter_type_expr (local_non_recursive_abbrev true visited env p) ty
+          iter_type_expr
+            (local_non_recursive_abbrev ~allow_rec true visited env p) ty
   end
 
 let local_non_recursive_abbrev env p ty =
+  let allow_rec =
+    !Clflags.recursive_types || !umode = Pattern && !allow_recursive_equation in
   try (* PR#7397: need to check trace_gadt_instances *)
     wrap_trace_gadt_instances env
-      (local_non_recursive_abbrev false [] env p) ty;
+      (local_non_recursive_abbrev ~allow_rec false [] env p) ty;
     true
   with Occur -> false
 
@@ -2660,7 +2669,8 @@ and unify3 env t1 t1' t2 t2' =
             unify_list env tl1 tl2
           else if !assume_injective then
             set_mode_pattern ~generate:true ~injective:false
-                             (fun () -> unify_list env tl1 tl2)
+              ~allow_recursive:!allow_recursive_equation
+              (fun () -> unify_list env tl1 tl2)
           else if in_current_module p1 (* || in_pervasives p1 *)
                   || List.exists (expands_to_datatype !env) [t1'; t1; t2] then
             unify_list env tl1 tl2
@@ -2674,6 +2684,7 @@ and unify3 env t1 t1' t2 t2' =
               (fun i (t1, t2) ->
                 if i then unify env t1 t2 else
                 set_mode_pattern ~generate:false ~injective:false
+                  ~allow_recursive:!allow_recursive_equation
                   begin fun () ->
                     let snap = snapshot () in
                     try unify env t1 t2 with Unify _ ->
@@ -3047,11 +3058,11 @@ let unify env ty1 ty2 =
       undo_compress snap;
       raise (Unify (expand_trace !env trace))
 
-let unify_gadt ~equations_level:lev (env:Env.t ref) ty1 ty2 =
+let unify_gadt ~equations_level:lev ~allow_recursive (env:Env.t ref) ty1 ty2 =
   try
     univar_pairs := [];
     gadt_equations_level := Some lev;
-    set_mode_pattern ~generate:true ~injective:true
+    set_mode_pattern ~generate:true ~injective:true ~allow_recursive
                      (fun () -> unify env ty1 ty2);
     gadt_equations_level := None;
     TypePairs.clear unify_eq_set;

typing/ctype.mli

@@ -252,7 +252,8 @@ val enforce_constraints: Env.t -> type_expr -> unit
 val unify: Env.t -> type_expr -> type_expr -> unit
         (* Unify the two types given. Raise [Unify] if not possible. *)
 val unify_gadt:
-        equations_level:int -> Env.t ref -> type_expr -> type_expr -> unit
+        equations_level:int -> allow_recursive:bool ->
+        Env.t ref -> type_expr -> type_expr -> unit
         (* Unify the two types given and update the environment with the
            local constraints. Raise [Unify] if not possible. *)
 val unify_var: Env.t -> type_expr -> type_expr -> unit

typing/typecore.ml

@@ -303,12 +303,14 @@ let get_gadt_equations_level () =
   | None -> assert false
 
 (* unification inside type_pat*)
-let unify_pat_types ?(refine=false) loc env ty ty' =
+let unify_pat_types ?(refine = None) loc env ty ty' =
   try
-    if refine then
-      unify_gadt ~equations_level:(get_gadt_equations_level ()) env ty ty'
-    else
-      unify !env ty ty'
+    match refine with
+    | Some allow_recursive ->
+        unify_gadt ~equations_level:(get_gadt_equations_level ())
+          ~allow_recursive env ty ty'
+    | None ->
+        unify !env ty ty'
   with
   | Unify trace ->
       raise(Error(loc, !env, Pattern_type_clash(trace, None)))
@@ -1317,7 +1319,8 @@ and type_pat_aux
     type_pat category ~no_existentials ~mode ~env
   in
   let loc = sp.ppat_loc in
-  let refine = match mode with Normal -> false | Counter_example _ -> true in
+  let refine =
+    match mode with Normal -> None | Counter_example _ -> Some true in
   let unif (x : pattern) : pattern =
     unify_pat ~refine env x (instance expected_ty);
     x
@@ -1551,8 +1554,10 @@ and type_pat_aux
       in
       let expected_ty = instance expected_ty in
       (* PR#7214: do not use gadt unification for toplevel lets *)
-      unify_pat_types loc env ty_res expected_ty
-        ~refine:(refine || constr.cstr_generalized && no_existentials = None);
+      let refine =
+        if refine = None && constr.cstr_generalized && no_existentials = None
+        then Some false else refine in
+      unify_pat_types ~refine loc env ty_res expected_ty;
       end_def ();
       generalize_structure expected_ty;
       generalize_structure ty_res;