Permalink
Browse files

Fix PR#6405: unsound interaction of -rectypes and GADTs

git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@14769 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
  • Loading branch information...
Jacques Garrigue
Jacques Garrigue committed May 9, 2014
1 parent e34fa84 commit b6500cc2a4ab8a50565247976da0ce17b3940587
View
@@ -11,6 +11,7 @@ Language features:
- Separation between read-only strings (type string) and read-write byte
sequences (type bytes). Activated by command-line option -safe-string.
- Exception cases in pattern matching (patch by Jeremy Yallop).
+- Extensible open datatypes (patch by Leo White).
Build system for the OCaml distribution:
- Use -bin-annot when building.
@@ -33,7 +34,7 @@ Type system:
- PR#6331: Slight change in the criterion to distinguish private
abbreviations and private row types: create a private abbreviation for
closed objects and fixed polymorphic variants.
-- PR#6333: Compare first class module types structurally rather than
+* PR#6333: Compare first class module types structurally rather than
nominally. Value subtyping allows module subtyping as long as the internal
representation is unchanged.
@@ -131,6 +132,7 @@ Bug fixes:
- PR#6384: Uncaught Not_found exception with a hidden .cmi file
- PR#6385: wrong allocation of large closures by the bytecode interpreter
- PR#6394: Assertion failed in Typecore.expand_path
+- PR#6405: unsound interaction of -rectypes and GADTs
- fix -dsource printing of "external _pipe = ..."
(Gabriel Scherer)
- bound-checking bug in caml_string_{get,set}{16,32,64}
@@ -1,8 +1,7 @@
-# Characters 118-119:
+# Characters 137-138:
fun C k -> k (fun x -> x);;
- ^
-Error: Recursive local constraint when unifying
- (((ex#0 -> ex#1) -> ex#1) -> (ex#2 -> ex#1) -> ex#1) t
- with ((a -> o) -> o) t
+ ^
+Error: This expression has type ex#0 but an expression was expected of type
+ ex#1 = (ex#2 -> ex#1) -> ex#1
#
@@ -1,8 +1,7 @@
-# Characters 118-119:
+# Characters 137-138:
fun C k -> k (fun x -> x);;
- ^
-Error: Recursive local constraint when unifying
- (((ex#0 -> ex#1) -> ex#1) -> (ex#2 -> ex#1) -> ex#1) t
- with ((a -> o) -> o) t
+ ^
+Error: This expression has type ex#0 but an expression was expected of type
+ ex#1 = (ex#2 -> ex#1) -> ex#1
#
@@ -102,12 +102,8 @@ module Existential_escape =
module Rectype =
struct
type (_,_) t = C : ('a,'a) t
- let _ =
- fun (type s) ->
- let a : (s, s * s) t = failwith "foo" in
- match a with
- C ->
- ()
+ let f : type s. (s, s*s) t -> unit =
+ fun C -> () (* here s = s*s! *)
end
;;
@@ -53,10 +53,8 @@ module Nonexhaustive :
Error: This expression has type a#2 t but an expression was expected of type
a#2 t
The type constructor a#2 would escape its scope
-# Characters 174-175:
- C ->
- ^
-Error: Recursive local constraint when unifying (s, s) t with (s, s * s) t
+# module Rectype :
+ sig type (_, _) t = C : ('a, 'a) t val f : ('s, 's * 's) t -> unit end
# Characters 178-186:
| (IntLit _ | BoolLit _) -> ()
^^^^^^^^
@@ -53,10 +53,8 @@ module Nonexhaustive :
Error: This expression has type a#2 t but an expression was expected of type
a#2 t
The type constructor a#2 would escape its scope
-# Characters 174-175:
- C ->
- ^
-Error: Recursive local constraint when unifying (s, s) t with (s, s * s) t
+# module Rectype :
+ sig type (_, _) t = C : ('a, 'a) t val f : ('s, 's * 's) t -> unit end
# Characters 178-186:
| (IntLit _ | BoolLit _) -> ()
^^^^^^^^
@@ -295,12 +295,12 @@ Warning 10: this expression should have type unit.
unit -> object method private m : int method n : int method o : int end
# - : int * int = (1, 1)
# class c : unit -> object method m : int end
-# - : int = 98
-# - : int = 99
+# - : int = 99
# - : int = 100
-# - : int * int * int = (101, 102, 103)
-# - : int * int * int * int * int = (104, 105, 106, 33, 33)
-# - : int * int * int * int * int = (107, 108, 109, 33, 33)
+# - : int = 101
+# - : int * int * int = (102, 103, 104)
+# - : int * int * int * int * int = (105, 106, 107, 33, 33)
+# - : int * int * int * int * int = (108, 109, 110, 33, 33)
# Characters 42-69:
class a = let _ = new b in object end
^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -294,12 +294,12 @@ Warning 10: this expression should have type unit.
unit -> object method private m : int method n : int method o : int end
# - : int * int = (1, 1)
# class c : unit -> object method m : int end
-# - : int = 98
-# - : int = 99
+# - : int = 99
# - : int = 100
-# - : int * int * int = (101, 102, 103)
-# - : int * int * int * int * int = (104, 105, 106, 33, 33)
-# - : int * int * int * int * int = (107, 108, 109, 33, 33)
+# - : int = 101
+# - : int * int * int = (102, 103, 104)
+# - : int * int * int * int * int = (105, 106, 107, 33, 33)
+# - : int * int * int * int * int = (108, 109, 110, 33, 33)
# Characters 42-69:
class a = let _ = new b in object end
^^^^^^^^^^^^^^^^^^^^^^^^^^^
View
@@ -1694,7 +1694,8 @@ let occur env ty0 ty =
let occur_in env ty0 t =
try occur env ty0 t; false with Unify _ -> true
-(* checks that a local constraint is non recursive *)
+(* Check that a local constraint is well-founded *)
+(* PR#6405: always assume -rectypes mode here *)
let rec local_non_recursive_abbrev visited env p ty =
let ty = repr ty in
if not (List.memq ty !visited) then begin
@@ -1704,15 +1705,9 @@ let rec local_non_recursive_abbrev visited env p ty =
if Path.same p p' then raise Recursive_abbrev;
begin try
local_non_recursive_abbrev visited env p (try_expand_once_opt env ty)
- with Cannot_expand ->
- if !Clflags.recursive_types then () else
- iter_type_expr (local_non_recursive_abbrev visited env p) ty
+ with Cannot_expand -> ()
end
- | Tobject _ | Tvariant _ ->
- ()
- | _ ->
- if !Clflags.recursive_types then () else
- iter_type_expr (local_non_recursive_abbrev visited env p) ty
+ | _ -> ()
end
let local_non_recursive_abbrev env p =

0 comments on commit b6500cc

Please sign in to comment.