Attached Files  type_pat_cps.diff [^] (35,978 bytes) 20150507 09:47 [Show Content] [Hide Content]Index: testsuite/tests/typinggadts/omega07.ml.principal.reference
===================================================================
 testsuite/tests/typinggadts/omega07.ml.principal.reference (revision 16098)
+++ testsuite/tests/typinggadts/omega07.ml.principal.reference (working copy)
@@ 63,15 +63,7 @@
# val smaller : ('a succ, 'b succ) le > ('a, 'b) le = <fun>
# type (_, _) diff = Diff : 'c nat * ('a, 'c, 'b) plus > ('a, 'b) diff
# * * * * * * * * * val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
# Characters 87243:
 ..match a, b,le with (* warning *)
  NZ, m, LeZ _ > Diff (m, PlusZ m)
  NS x, NS y, LeS q >
 match diff q x y with Diff (m, p) > Diff (m, PlusS p)
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
(NS _, NZ, _)
val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
+# val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
# val diff : ('a, 'b) le > 'b nat > ('a, 'b) diff = <fun>
# type (_, _) filter = Filter : ('m, 'n) le * ('a, 'm) seq > ('a, 'n) filter
val leS' : ('m, 'n) le > ('m, 'n succ) le = <fun>
Index: testsuite/tests/typinggadts/omega07.ml.reference
===================================================================
 testsuite/tests/typinggadts/omega07.ml.reference (revision 16098)
+++ testsuite/tests/typinggadts/omega07.ml.reference (working copy)
@@ 63,15 +63,7 @@
# val smaller : ('a succ, 'b succ) le > ('a, 'b) le = <fun>
# type (_, _) diff = Diff : 'c nat * ('a, 'c, 'b) plus > ('a, 'b) diff
# * * * * * * * * * val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
# Characters 87243:
 ..match a, b,le with (* warning *)
  NZ, m, LeZ _ > Diff (m, PlusZ m)
  NS x, NS y, LeS q >
 match diff q x y with Diff (m, p) > Diff (m, PlusS p)
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
(NS _, NZ, _)
val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
+# val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
# val diff : ('a, 'b) le > 'b nat > ('a, 'b) diff = <fun>
# type (_, _) filter = Filter : ('m, 'n) le * ('a, 'm) seq > ('a, 'n) filter
val leS' : ('m, 'n) le > ('m, 'n succ) le = <fun>
Index: testsuite/tests/typinggadts/pr5332.ml.reference
===================================================================
 testsuite/tests/typinggadts/pr5332.ml.reference (revision 16098)
+++ testsuite/tests/typinggadts/pr5332.ml.reference (working copy)
@@ 13,7 +13,7 @@
 Tvar var, tb > 2
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
(Tbool, Tvar _)
+(Tbool, Tvar Zero)
val f : ('env, 'a) typ > ('env, 'a) typ > int = <fun>
# Exception: Match_failure ("//toplevel//", 9, 1).
#
Index: testsuite/tests/typinggadts/pr6163.ml.principal.reference
===================================================================
 testsuite/tests/typinggadts/pr6163.ml.principal.reference (revision 16098)
+++ testsuite/tests/typinggadts/pr6163.ml.principal.reference (working copy)
@@ 13,6 +13,6 @@
 Succ (Succ (Succ (Succ Zero))) > "4"
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
Succ (Succ (Succ (Succ (Succ _))))
+Succ (Succ (Succ (Succ (Succ Zero))))
val f : aux > string = <fun>
#
Index: testsuite/tests/typinggadts/pr6163.ml.reference
===================================================================
 testsuite/tests/typinggadts/pr6163.ml.reference (revision 16098)
+++ testsuite/tests/typinggadts/pr6163.ml.reference (working copy)
@@ 13,6 +13,6 @@
 Succ (Succ (Succ (Succ Zero))) > "4"
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
Succ (Succ (Succ (Succ (Succ _))))
+Succ (Succ (Succ (Succ (Succ Zero))))
val f : aux > string = <fun>
#
Index: testsuite/tests/typinggadts/test.ml
===================================================================
 testsuite/tests/typinggadts/test.ml (revision 16098)
+++ testsuite/tests/typinggadts/test.ml (working copy)
@@ 91,6 +91,52 @@
end
;;
+module Exhaustive2 = struct
+ type _ t = Int : int t
+ let f (x : bool t option) = match x with None > ()
+end;;
+
+module PR6220 = struct
+ type 'a t = I : int t  F : float t
+ let f : int t > int = function I > 1
+ let g : int t > int = function I > 1  _ > 2 (* no warning *)
+end;;
+
+module PR6403 = struct
+ type (_, _) eq = Refl : ('a, 'a) eq
+ type empty = { bottom : 'a . 'a }
+ type ('a, 'b) sum = Left of 'a  Right of 'b
+
+ let notequal : ((int, bool) eq, empty) sum > empty = function
+  Right empty > empty
+end;;
+
+module PR6437 = struct
+ type ('a, 'b) ctx =
+  Nil : (unit, unit) ctx
+  Cons : ('a, 'b) ctx > ('a * unit, 'b * unit) ctx
+
+ type 'a var =
+  O : ('a * unit) var
+  S : 'a var > ('a * unit) var
+
+ let rec f : type g1 g2. (g1, g2) ctx * g1 var > g2 var = function
+  Cons g, O > O
+  Cons g, S n > S (f (g, n))
+ (* Nil, _ > (assert false) *) (* warns, but shouldn't *)
+end;;
+
+module PR6801 = struct
+ type _ value =
+  String : string > string value
+  Float : float > float value
+  Any
+
+ let print_string_value (x : string value) =
+ match x with
+  String s > print_endline s (* warn : Any *)
+end;;
+
module Existential_escape =
struct
type _ t = C : int > int t
@@ 108,7 +154,7 @@
;;
module Or_patterns =
struct
+ struct
type _ t =
 IntLit : int > int t
 BoolLit : bool > bool t
Index: testsuite/tests/typinggadts/test.ml.principal.reference
===================================================================
 testsuite/tests/typinggadts/test.ml.principal.reference (revision 16098)
+++ testsuite/tests/typinggadts/test.ml.principal.reference (working copy)
@@ 47,6 +47,43 @@
type 'a v = Foo : t > t v  Bar : u > u v
val same_type : 's v * 's v > bool
end
+# module Exhaustive2 :
+ sig type _ t = Int : int t val f : bool t option > unit end
+# module PR6220 :
+ sig
+ type 'a t = I : int t  F : float t
+ val f : int t > int
+ val g : int t > int
+ end
+# module PR6403 :
+ sig
+ type (_, _) eq = Refl : ('a, 'a) eq
+ type empty = { bottom : 'a. 'a; }
+ type ('a, 'b) sum = Left of 'a  Right of 'b
+ val notequal : ((int, bool) eq, empty) sum > empty
+ end
+# module PR6437 :
+ sig
+ type ('a, 'b) ctx =
+ Nil : (unit, unit) ctx
+  Cons : ('a, 'b) ctx > ('a * unit, 'b * unit) ctx
+ type 'a var = O : ('a * unit) var  S : 'a var > ('a * unit) var
+ val f : ('g1, 'g2) ctx * 'g1 var > 'g2 var
+ end
+# Characters 175221:
+ ....match x with
+  String s > print_endline s.................
+Warning 8: this patternmatching is not exhaustive.
+Here is an example of a value that is not matched:
+Any
+module PR6801 :
+ sig
+ type _ value =
+ String : string > string value
+  Float : float > float value
+  Any
+ val print_string_value : string value > unit
+ end
# Characters 118119:
let eval (D x) = x
^
@@ 55,7 +92,7 @@
The type constructor a#2 would escape its scope
# module Rectype :
sig type (_, _) t = C : ('a, 'a) t val f : ('s, 's * 's) t > unit end
# Characters 178186:
+# Characters 180188:
 (IntLit _  BoolLit _) > ()
^^^^^^^^
Error: This pattern matches values of type int t
@@ 286,14 +323,14 @@
^
Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < foo : int >
 Type ex#17 = < bar : int; .. > is not compatible with type < >
+ Type ex#23 = < bar : int; .. > is not compatible with type < >
The second object type has no method bar
# Characters 9899:
(x:<foo:int;bar:int>)
^
Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < bar : int; foo : int >
 Type ex#19 = < bar : int; .. > is not compatible with type
+ Type ex#25 = < bar : int; .. > is not compatible with type
< bar : int >
The first object type has an abstract row, it cannot be closed
# Characters 9899:
@@ 301,7 +338,7 @@
^
Error: This expression has type < bar : int; foo : int; .. >
but an expression was expected of type 'a
 The type constructor ex#22 would escape its scope
+ The type constructor ex#28 would escape its scope
# val g : 'a > 'a int_foo > 'a int_bar > 'a = <fun>
# val g : 'a > 'a int_foo > 'a int_bar > 'a * int * int = <fun>
# type 'a ty = Int : int > int ty
Index: testsuite/tests/typinggadts/test.ml.reference
===================================================================
 testsuite/tests/typinggadts/test.ml.reference (revision 16098)
+++ testsuite/tests/typinggadts/test.ml.reference (working copy)
@@ 47,6 +47,43 @@
type 'a v = Foo : t > t v  Bar : u > u v
val same_type : 's v * 's v > bool
end
+# module Exhaustive2 :
+ sig type _ t = Int : int t val f : bool t option > unit end
+# module PR6220 :
+ sig
+ type 'a t = I : int t  F : float t
+ val f : int t > int
+ val g : int t > int
+ end
+# module PR6403 :
+ sig
+ type (_, _) eq = Refl : ('a, 'a) eq
+ type empty = { bottom : 'a. 'a; }
+ type ('a, 'b) sum = Left of 'a  Right of 'b
+ val notequal : ((int, bool) eq, empty) sum > empty
+ end
+# module PR6437 :
+ sig
+ type ('a, 'b) ctx =
+ Nil : (unit, unit) ctx
+  Cons : ('a, 'b) ctx > ('a * unit, 'b * unit) ctx
+ type 'a var = O : ('a * unit) var  S : 'a var > ('a * unit) var
+ val f : ('g1, 'g2) ctx * 'g1 var > 'g2 var
+ end
+# Characters 175221:
+ ....match x with
+  String s > print_endline s.................
+Warning 8: this patternmatching is not exhaustive.
+Here is an example of a value that is not matched:
+Any
+module PR6801 :
+ sig
+ type _ value =
+ String : string > string value
+  Float : float > float value
+  Any
+ val print_string_value : string value > unit
+ end
# Characters 118119:
let eval (D x) = x
^
@@ 55,7 +92,7 @@
The type constructor a#2 would escape its scope
# module Rectype :
sig type (_, _) t = C : ('a, 'a) t val f : ('s, 's * 's) t > unit end
# Characters 178186:
+# Characters 180188:
 (IntLit _  BoolLit _) > ()
^^^^^^^^
Error: This pattern matches values of type int t
@@ 273,14 +310,14 @@
^
Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < foo : int >
 Type ex#17 = < bar : int; .. > is not compatible with type < >
+ Type ex#23 = < bar : int; .. > is not compatible with type < >
The second object type has no method bar
# Characters 9899:
(x:<foo:int;bar:int>)
^
Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < bar : int; foo : int >
 Type ex#19 = < bar : int; .. > is not compatible with type
+ Type ex#25 = < bar : int; .. > is not compatible with type
< bar : int >
The first object type has an abstract row, it cannot be closed
# Characters 9899:
@@ 288,7 +325,7 @@
^
Error: This expression has type < bar : int; foo : int; .. >
but an expression was expected of type 'a
 The type constructor ex#22 would escape its scope
+ The type constructor ex#28 would escape its scope
# val g : 'a > 'a int_foo > 'a int_bar > 'a = <fun>
# val g : 'a > 'a int_foo > 'a int_bar > 'a * int * int = <fun>
# type 'a ty = Int : int > int ty
Index: typing/ctype.ml
===================================================================
 typing/ctype.ml (revision 16098)
+++ typing/ctype.ml (working copy)
@@ 116,6 +116,20 @@
let global_level = ref 1
let saved_level = ref []
+type levels =
+ { current_level: int; nongen_level: int; global_level: int;
+ saved_level: (int * int) list; }
+let save_levels () =
+ { current_level = !current_level;
+ nongen_level = !nongen_level;
+ global_level = !global_level;
+ saved_level = !saved_level }
+let set_levels l =
+ current_level := l.current_level;
+ nongen_level := l.nongen_level;
+ global_level := l.global_level;
+ saved_level := l.saved_level
+
let get_current_level () = !current_level
let init_def level = current_level := level; nongen_level := level
let begin_def () =
Index: typing/ctype.mli
===================================================================
 typing/ctype.mli (revision 16098)
+++ typing/ctype.mli (working copy)
@@ 37,6 +37,11 @@
val increase_global_level: unit > int
val restore_global_level: int > unit
(* This pair of functions is only used in Typetexp *)
+type levels =
+ { current_level: int; nongen_level: int; global_level: int;
+ saved_level: (int * int) list; }
+val save_levels: unit > levels
+val set_levels: levels > unit
val newty: type_desc > type_expr
val newvar: ?name:string > unit > type_expr
Index: typing/parmatch.ml
===================================================================
 typing/parmatch.ml (revision 16098)
+++ typing/parmatch.ml (working copy)
@@ 625,11 +625,11 @@
 ({pat_desc = Tpat_construct(_,c,_);pat_type=typ},_) :: _ >
if c.cstr_consts < 0 then false (* extensions *)
else
 if ignore_generalized then
+ if ignore_generalized then true
(* remove generalized constructors;
those cases will be handled separately *)
 let env = clean_env env in
 List.length env = c.cstr_normal
+ (*let env = clean_env env in
+ List.length env = c.cstr_normal*)
else
List.length env = c.cstr_consts + c.cstr_nonconsts
@@ 715,20 +715,47 @@
(* build a pattern from a constructor list *)
let pat_of_constr ex_pat cstr =
 {ex_pat with pat_desc =
 Tpat_construct (mknoloc (Longident.Lident "?pat_of_constr?"),
 cstr,omegas cstr.cstr_arity)}
+ {ex_pat with pat_desc =
+ Tpat_construct (mknoloc (Longident.Lident "?pat_of_constr?"),
+ cstr, omegas cstr.cstr_arity)}
let rec pat_of_constrs ex_pat = function
 [] > raise Empty
 [cstr] > pat_of_constr ex_pat cstr
 cstr::rem >
 {ex_pat with
 pat_desc=
 Tpat_or
 (pat_of_constr ex_pat cstr,
 pat_of_constrs ex_pat rem, None)}
+let rec orify_many = function
+ [] > assert false
+ [x] > x
+ x :: xs >
+ make_pat (Tpat_or (x, orify_many xs, None)) x.pat_type x.pat_env
+let pat_of_constrs ex_pat cstrs =
+ if cstrs = [] then raise Empty else
+ orify_many (List.map (pat_of_constr ex_pat) cstrs)
+
+let pats_of_type env ty =
+ let ty' = Ctype.expand_head env ty in
+ match ty'.desc with
+  Tconstr (path, _, _) >
+ begin match Env.find_type path env with
+  {type_kind = Type_variant cl}
+ when List.for_all (fun cd > cd.Types.cd_res <> None) cl >
+ let cstrs = fst (Env.find_type_descrs path env) in
+ List.map
+ (pat_of_constr {omega with pat_type=ty; pat_env=env})
+ cstrs
+  _ > [omega]
+ end
+  _ > [omega]
+
+let pat_of_constr_gadt ex_pat cstr =
+ let no_split = cstr.cstr_generalized  cstr.cstr_arity = 0 in
+ if no_split then pat_of_constr ex_pat cstr else
+ let env = ex_pat.pat_env in
+ let ty_args, ty_res = Ctype.instance_constructor cstr in
+ (try Ctype.unify env ty_res ex_pat.pat_type with
+ Ctype.Unify _ > assert false);
+ let id = mknoloc (Longident.Lident cstr.cstr_name) in
+ let patl =
+ List.map (fun ty > {omega with pat_env = env; pat_type = ty}) ty_args in
+ {ex_pat with pat_desc = Tpat_construct (id, cstr, patl)}
+
let rec get_variant_constructors env ty =
match (Ctype.repr ty).desc with
 Tconstr (path,_,_) > begin
@@ 778,7 +805,7 @@
in the first column of env
*)
let build_other ext env = match env with
+let build_other ext env = match env with
 ({pat_desc = Tpat_construct (lid,
({cstr_tag=Cstr_extension _} as c),_)},_) :: _ >
let c = {c with cstr_name = "*extension*"} in
@@ 910,10 +937,9 @@
 _ > fatal_error "Parmatch.get_tag" in
let all_tags = List.map (fun (p,_) > get_tag p) env in
let cnstrs = complete_constrs p all_tags in
 let pats = List.map (pat_of_constr p) cnstrs in
+ List.map (pat_of_constr_gadt p) cnstrs
(* List.iter (Format.eprintf "%a@." top_pretty) pats;
Format.eprintf "@.@."; *)
 pats
 _ > assert false
(*
@@ 981,15 +1007,6 @@
 Rnone (* No matching value *)
 Rsome of 'a (* This matching value *)
let rec orify_many =
 let orify x y =
 make_pat (Tpat_or (x, y, None)) x.pat_type x.pat_env
 in
 function
  [] > assert false
  [x] > x
  x :: xs > orify x (orify_many xs)

let rec try_many f = function
 [] > Rnone
 (p,pss)::rest >
@@ 1193,12 +1210,12 @@
try_non_omega rem && ok
 [] > true
in
 if full_match true (tdefs=None) constrs then
+ if full_match false (tdefs=None) constrs then
try_non_omega constrs
else if tdefs = None then
pressure_variants None (filter_extra pss)
else
 let full = full_match true true constrs in
+ let full = full_match false true constrs in
let ok =
if full then try_non_omega constrs
else try_non_omega (filter_all q0 (mark_partial pss))
@@ 1699,13 +1716,22 @@
(string, Types.constructor_description) Hashtbl.t *
(string, Types.label_description) Hashtbl.t
=
 let constrs = Hashtbl.create 0 in
 let labels = Hashtbl.create 0 in
+ let constrs = Hashtbl.create 7 in
+ let labels = Hashtbl.create 7 in
let rec loop pat =
match pat.pat_desc with
Tpat_or (a,b,_) >
 loop a @ loop b
  Tpat_any  Tpat_constant _  Tpat_var _ >
+ (* loop a @ loop b *)
+ begin match loop a, loop b with
+ [pa], [pb] > [mkpat (Ppat_or (pa, pb))]
+  _ > assert false
+ end
+  Tpat_any  Tpat_var _ >
+ begin match pats_of_type pat.pat_env pat.pat_type with
+ [{pat_desc = Tpat_any}] > [mkpat Ppat_any]
+  pats > List.flatten (List.map loop pats)
+ end
+  Tpat_constant _ >
[mkpat Ppat_any]
 Tpat_alias (p,_,_) > loop p
 Tpat_tuple lst >
@@ 1775,6 +1801,12 @@
(ps, constrs, labels)
end
+let ppats_of_type env ty =
+ match pats_of_type env ty with
+ [{pat_desc = Tpat_any}] >
+ ([Conv.mkpat Parsetree.Ppat_any], Hashtbl.create 0, Hashtbl.create 0)
+  pats >
+ Conv.conv (orify_many pats)
let do_check_partial ?pred exhaust loc casel pss = match pss with
 [] >
Index: typing/parmatch.mli
===================================================================
 typing/parmatch.mli (revision 16098)
+++ typing/parmatch.mli (working copy)
@@ 51,6 +51,10 @@
val pat_of_constr : pattern > constructor_description > pattern
val complete_constrs :
pattern > constructor_tag list > constructor_description list
+val ppats_of_type : Env.t > type_expr >
+ Parsetree.pattern list *
+ (string, constructor_description) Hashtbl.t *
+ (string, label_description) Hashtbl.t
val pressure_variants: Env.t > pattern list > unit
val check_partial: Location.t > case list > partial
Index: typing/typecore.ml
===================================================================
 typing/typecore.ml (revision 16098)
+++ typing/typecore.ml (working copy)
@@ 826,7 +826,11 @@
 ({ txt = Longident.Ldot (modname, _) }, _) :: _ > Some modname
 _ :: rest > find_record_qual rest
let type_label_a_list ?labels loc closed env type_lbl_a opath lid_a_list =
+let map_fold_cont f xs k =
+ List.fold_right (fun x k ys > f x (fun y > k (y :: ys)))
+ xs (fun ys > k (List.rev ys)) []
+
+let type_label_a_list ?labels loc closed env type_lbl_a opath lid_a_list k =
let lbl_a_list =
match lid_a_list, labels with
({txt=Longident.Lident s}, _)::_, Some labels when Hashtbl.mem labels s >
@@ 856,7 +860,7 @@
(fun (_,lbl1,_) (_,lbl2,_) > compare lbl1.lbl_pos lbl2.lbl_pos)
lbl_a_list
in
 List.map type_lbl_a lbl_a_list
+ map_fold_cont type_lbl_a lbl_a_list k
;;
(* Checks over the labels mentioned in a record pattern:
@@ 916,24 +920,65 @@
 Normal
 Inside_or
+type state =
+ { pattern_variables :
+ (Ident.t * type_expr * string loc * Location.t * bool (* asvariable *))
+ list;
+ pattern_force : (unit > unit) list;
+ pattern_scope : Annot.ident option;
+ allow_modules : bool;
+ module_variables : (string loc * Location.t) list;
+ snapshot : Btype.snapshot;
+ levels : Ctype.levels;
+ env : Env.t; }
+let save_state env =
+ { pattern_variables = !pattern_variables;
+ pattern_force = !pattern_force;
+ pattern_scope = !pattern_scope;
+ allow_modules = !allow_modules;
+ module_variables = !module_variables;
+ snapshot = Btype.snapshot ();
+ levels = Ctype.save_levels ();
+ env = !env; }
+let set_state s env =
+ pattern_variables := s.pattern_variables;
+ pattern_force := s.pattern_force;
+ pattern_scope := s.pattern_scope;
+ allow_modules := s.allow_modules;
+ module_variables := s.module_variables;
+ Btype.backtrack s.snapshot;
+ Ctype.set_levels s.levels;
+ env := s.env
+
(* type_pat propagates the expected type as well as maps for
constructors and labels.
Unification may update the typing environment. *)
let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
 let type_pat ?(mode=mode) ?(env=env) =
+let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty k =
+ let type_pat ?(constrs=constrs) ?(labels=labels) ?(mode=mode) ?(env=env) =
type_pat ~constrs ~labels ~no_existentials ~mode ~env in
let loc = sp.ppat_loc in
+ let rp k x : pattern = if constrs = None then k (rp x) else k x in
match sp.ppat_desc with
Ppat_any >
 rp {
 pat_desc = Tpat_any;
+ let k' d = rp k {
+ pat_desc = d;
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
pat_env = !env }
+ in
+ if labels <> None then
+ let (spl, constrs, labels) = Parmatch.ppats_of_type !env expected_ty in
+ match spl with
+  [{ppat_desc = Parsetree.Ppat_any}] > k' Tpat_any
+  [sp] >
+ type_pat ~constrs:(Some constrs) ~labels:None
+ sp expected_ty k
+  _ > assert false
+ else k' Tpat_any
 Ppat_var name >
let id = enter_variable loc name expected_ty in
 rp {
+ rp k {
pat_desc = Tpat_var (id, name);
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
@@ 941,7 +986,7 @@
pat_env = !env }
 Ppat_unpack name >
let id = enter_variable loc name expected_ty ~is_module:true in
 rp {
+ rp k {
pat_desc = Tpat_var (id, name);
pat_loc = sp.ppat_loc;
pat_extra=[Tpat_unpack, loc, sp.ppat_attributes];
@@ 962,7 +1007,7 @@
end_def ();
generalize ty';
let id = enter_variable lloc name ty' in
 rp {
+ rp k {
pat_desc = Tpat_var (id, name);
pat_loc = lloc;
pat_extra = [Tpat_constraint cty, loc, sp.ppat_attributes];
@@ 973,21 +1018,21 @@
 _ > assert false
end
 Ppat_alias(sq, name) >
 let q = type_pat sq expected_ty in
 begin_def ();
 let ty_var = build_as_type !env q in
 end_def ();
 generalize ty_var;
 let id = enter_variable ~is_as_variable:true loc name ty_var in
 rp {
 pat_desc = Tpat_alias(q, id, name);
 pat_loc = loc; pat_extra=[];
 pat_type = q.pat_type;
 pat_attributes = sp.ppat_attributes;
 pat_env = !env }
+ type_pat sq expected_ty (fun q >
+ begin_def ();
+ let ty_var = build_as_type !env q in
+ end_def ();
+ generalize ty_var;
+ let id = enter_variable ~is_as_variable:true loc name ty_var in
+ rp k {
+ pat_desc = Tpat_alias(q, id, name);
+ pat_loc = loc; pat_extra=[];
+ pat_type = q.pat_type;
+ pat_attributes = sp.ppat_attributes;
+ pat_env = !env })
 Ppat_constant cst >
unify_pat_types loc !env (type_constant cst) expected_ty;
 rp {
+ rp k {
pat_desc = Tpat_constant cst;
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
@@ 1005,7 +1050,7 @@
in
let p = if c1 <= c2 then loop c1 c2 else loop c2 c1 in
let p = {p with ppat_loc=loc} in
 type_pat p expected_ty
+ type_pat ~labels:None p expected_ty k
(* TODO: record 'extra' to remember about interval *)
 Ppat_interval _ >
raise (Error (loc, !env, Invalid_interval))
@@ 1015,13 +1060,13 @@
let spl_ann = List.map (fun p > (p,newvar ())) spl in
let ty = newty (Ttuple(List.map snd spl_ann)) in
unify_pat_types loc !env ty expected_ty;
 let pl = List.map (fun (p,t) > type_pat p t) spl_ann in
 rp {
+ map_fold_cont (fun (p,t) > type_pat p t) spl_ann (fun pl >
+ rp k {
pat_desc = Tpat_tuple pl;
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
 pat_env = !env }
+ pat_env = !env })
 Ppat_construct(lid, sarg) >
let opath =
try
@@ 1089,13 +1134,14 @@
in
if constr.cstr_inlined <> None then List.iter check_non_escaping sargs;
 let args = List.map2 (fun p t > type_pat p t) sargs ty_args in
 rp {
 pat_desc=Tpat_construct(lid, constr, args);
 pat_loc = loc; pat_extra=[];
 pat_type = expected_ty;
 pat_attributes = sp.ppat_attributes;
 pat_env = !env }
+ map_fold_cont (fun (p,t) > type_pat p t) (List.combine sargs ty_args)
+ (fun args >
+ rp k {
+ pat_desc=Tpat_construct(lid, constr, args);
+ pat_loc = loc; pat_extra=[];
+ pat_type = expected_ty;
+ pat_attributes = sp.ppat_attributes;
+ pat_env = !env })
 Ppat_variant(l, sarg) >
let arg_type = match sarg with None > []  Some _ > [newvar()] in
let row = { row_fields =
@@ 1106,18 +1152,19 @@
row_fixed = false;
row_name = None } in
unify_pat_types loc !env (newty (Tvariant row)) expected_ty;
 let arg =
 (* PR#6235: propagate type information *)
 match sarg, arg_type with
 Some p, [ty] > Some (type_pat p ty)
  _ > None
 in
 rp {
+ let k arg =
+ rp k {
pat_desc = Tpat_variant(l, arg, ref {row with row_more = newvar()});
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
pat_env = !env }
+ in begin
+ (* PR#6235: propagate type information *)
+ match sarg, arg_type with
+ Some p, [ty] > type_pat p ty (fun p > k (Some p))
+  _ > k None
+ end
 Ppat_record(lid_sp_list, closed) >
if lid_sp_list = [] then
Syntaxerr.ill_formed_ast loc "Records cannot be empty.";
@@ 1127,7 +1174,7 @@
Some (p0, p, true), expected_ty
with Not_found > None, newvar ()
in
 let type_label_pat (label_lid, label, sarg) =
+ let type_label_pat (label_lid, label, sarg) k =
begin_def ();
let (vars, ty_arg, ty_res) = instance_label false label in
if vars = [] then end_def ();
@@ 1137,55 +1184,72 @@
raise(Error(label_lid.loc, !env,
Label_mismatch(label_lid.txt, trace)))
end;
 let arg = type_pat sarg ty_arg in
 if vars <> [] then begin
 end_def ();
 generalize ty_arg;
 List.iter generalize vars;
 let instantiated tv =
 let tv = expand_head !env tv in
 not (is_Tvar tv)  tv.level <> generic_level in
 if List.exists instantiated vars then
 raise (Error(label_lid.loc, !env, Polymorphic_label label_lid.txt))
 end;
 (label_lid, label, arg)
+ type_pat sarg ty_arg (fun arg >
+ if vars <> [] then begin
+ end_def ();
+ generalize ty_arg;
+ List.iter generalize vars;
+ let instantiated tv =
+ let tv = expand_head !env tv in
+ not (is_Tvar tv)  tv.level <> generic_level in
+ if List.exists instantiated vars then
+ raise
+ (Error(label_lid.loc, !env, Polymorphic_label label_lid.txt))
+ end;
+ k (label_lid, label, arg))
in
 let lbl_pat_list =
 wrap_disambiguate "This record pattern is expected to have" expected_ty
 (type_label_a_list ?labels loc false !env type_label_pat opath)
 lid_sp_list
 in
 check_recordpat_labels loc lbl_pat_list closed;
 unify_pat_types loc !env record_ty expected_ty;
 rp {
+ let k' k lbl_pat_list =
+ check_recordpat_labels loc lbl_pat_list closed;
+ unify_pat_types loc !env record_ty expected_ty;
+ rp k {
pat_desc = Tpat_record (lbl_pat_list, closed);
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
pat_env = !env }
+ in
+ if constrs = None then
+ k (wrap_disambiguate "This record pattern is expected to have"
+ expected_ty
+ (type_label_a_list ?labels loc false !env type_label_pat opath
+ lid_sp_list)
+ (k' (fun x > x)))
+ else
+ type_label_a_list ?labels loc false !env type_label_pat opath
+ lid_sp_list (k' k)
 Ppat_array spl >
let ty_elt = newvar() in
unify_pat_types
loc !env (instance_def (Predef.type_array ty_elt)) expected_ty;
let spl_ann = List.map (fun p > (p,newvar())) spl in
 let pl = List.map (fun (p,t) > type_pat p ty_elt) spl_ann in
 rp {
+ map_fold_cont (fun (p,t) > type_pat p ty_elt) spl_ann (fun pl >
+ rp k {
pat_desc = Tpat_array pl;
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
 pat_env = !env }
+ pat_env = !env })
 Ppat_or(sp1, sp2) >
+ if constrs <> None &&
+ match sp1.ppat_desc, sp2.ppat_desc with
+ Ppat_constant _, _  _, Ppat_constant _ > false
+  _ > true
+ then
+ let state = save_state env in
+ try type_pat sp1 expected_ty k with exn when exn <> Exit >
+ set_state state env;
+ type_pat sp2 expected_ty k
+ else
let initial_pattern_variables = !pattern_variables in
 let p1 = type_pat ~mode:Inside_or sp1 expected_ty in
+ let p1 = type_pat ~mode:Inside_or sp1 expected_ty (fun x > x) in
let p1_variables = !pattern_variables in
pattern_variables := initial_pattern_variables;
 let p2 = type_pat ~mode:Inside_or sp2 expected_ty in
+ let p2 = type_pat ~mode:Inside_or sp2 expected_ty (fun x > x) in
let p2_variables = !pattern_variables in
let alpha_env =
enter_orpat_variables loc !env p1_variables p2_variables in
pattern_variables := p1_variables;
 rp {
+ rp k {
pat_desc = Tpat_or(p1, alpha_pat alpha_env p2, None);
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
@@ 1195,13 +1259,13 @@
let nv = newvar () in
unify_pat_types loc !env (instance_def (Predef.type_lazy_t nv))
expected_ty;
 let p1 = type_pat sp1 nv in
 rp {
+ type_pat sp1 nv (fun p1 >
+ rp k {
pat_desc = Tpat_lazy p1;
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
 pat_env = !env }
+ pat_env = !env })
 Ppat_constraint(sp, sty) >
(* Separate when not already separated by !principal *)
let separate = true in
@@ 1216,27 +1280,28 @@
end else ty, ty
in
unify_pat_types loc !env ty expected_ty;
 let p = type_pat sp expected_ty' in
 (*Format.printf "%a@.%a@."
 Printtyp.raw_type_expr ty
 Printtyp.raw_type_expr p.pat_type;*)
 pattern_force := force :: !pattern_force;
 let extra = (Tpat_constraint cty, loc, sp.ppat_attributes) in
 if separate then
 match p.pat_desc with
 Tpat_var (id,s) >
 {p with pat_type = ty;
 pat_desc = Tpat_alias
 ({p with pat_desc = Tpat_any; pat_attributes = []}, id,s);
 pat_extra = [extra];
 }
  _ > {p with pat_type = ty;
 pat_extra = extra :: p.pat_extra}
 else p
+ type_pat sp expected_ty' (fun p >
+ (*Format.printf "%a@.%a@."
+ Printtyp.raw_type_expr ty
+ Printtyp.raw_type_expr p.pat_type;*)
+ pattern_force := force :: !pattern_force;
+ let extra = (Tpat_constraint cty, loc, sp.ppat_attributes) in
+ let p =
+ if not separate then p else
+ match p.pat_desc with
+ Tpat_var (id,s) >
+ {p with pat_type = ty;
+ pat_desc = Tpat_alias
+ ({p with pat_desc = Tpat_any; pat_attributes = []}, id,s);
+ pat_extra = [extra];
+ }
+  _ > {p with pat_type = ty;
+ pat_extra = extra :: p.pat_extra}
+ in k p)
 Ppat_type lid >
let (path, p,ty) = build_or_pat !env loc lid.txt in
unify_pat_types loc !env ty expected_ty;
 { p with pat_extra =
+ k { p with pat_extra =
(Tpat_type (path, lid), loc, sp.ppat_attributes) :: p.pat_extra }
 Ppat_exception _ >
raise (Error (loc, !env, Exception_pattern_below_toplevel))
@@ 1249,7 +1314,7 @@
try
let r =
type_pat ~no_existentials:(not allow_existentials) ~constrs ~labels
 ~mode:Normal ~env sp expected_ty in
+ ~mode:Normal ~env sp expected_ty (fun x > x) in
iter_pattern (fun p > p.pat_env < !env) r;
newtype_level := None;
r
@@ 2085,9 +2150,9 @@
let lbl_exp_list =
wrap_disambiguate "This record expression is expected to have" ty_record
(type_label_a_list loc closed env
 (type_label_exp true env loc ty_record)
 opath)
 lid_sexp_list
+ (fun e k > k (type_label_exp true env loc ty_record e))
+ opath lid_sexp_list)
+ (fun x > x)
in
unify_exp_types loc env ty_record (instance env ty_expected);
type_pat_cps2.diff [^] (39,997 bytes) 20150508 07:16 [Show Content] [Hide Content]Index: testsuite/tests/typinggadts/omega07.ml.principal.reference
===================================================================
 testsuite/tests/typinggadts/omega07.ml.principal.reference (revision 16100)
+++ testsuite/tests/typinggadts/omega07.ml.principal.reference (working copy)
@@ 63,15 +63,7 @@
# val smaller : ('a succ, 'b succ) le > ('a, 'b) le = <fun>
# type (_, _) diff = Diff : 'c nat * ('a, 'c, 'b) plus > ('a, 'b) diff
# * * * * * * * * * val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
# Characters 87243:
 ..match a, b,le with (* warning *)
  NZ, m, LeZ _ > Diff (m, PlusZ m)
  NS x, NS y, LeS q >
 match diff q x y with Diff (m, p) > Diff (m, PlusS p)
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
(NS _, NZ, _)
val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
+# val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
# val diff : ('a, 'b) le > 'b nat > ('a, 'b) diff = <fun>
# type (_, _) filter = Filter : ('m, 'n) le * ('a, 'm) seq > ('a, 'n) filter
val leS' : ('m, 'n) le > ('m, 'n succ) le = <fun>
Index: testsuite/tests/typinggadts/omega07.ml.reference
===================================================================
 testsuite/tests/typinggadts/omega07.ml.reference (revision 16100)
+++ testsuite/tests/typinggadts/omega07.ml.reference (working copy)
@@ 63,15 +63,7 @@
# val smaller : ('a succ, 'b succ) le > ('a, 'b) le = <fun>
# type (_, _) diff = Diff : 'c nat * ('a, 'c, 'b) plus > ('a, 'b) diff
# * * * * * * * * * val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
# Characters 87243:
 ..match a, b,le with (* warning *)
  NZ, m, LeZ _ > Diff (m, PlusZ m)
  NS x, NS y, LeS q >
 match diff q x y with Diff (m, p) > Diff (m, PlusS p)
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
(NS _, NZ, _)
val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
+# val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
# val diff : ('a, 'b) le > 'b nat > ('a, 'b) diff = <fun>
# type (_, _) filter = Filter : ('m, 'n) le * ('a, 'm) seq > ('a, 'n) filter
val leS' : ('m, 'n) le > ('m, 'n succ) le = <fun>
Index: testsuite/tests/typinggadts/pr5332.ml.reference
===================================================================
 testsuite/tests/typinggadts/pr5332.ml.reference (revision 16100)
+++ testsuite/tests/typinggadts/pr5332.ml.reference (working copy)
@@ 13,7 +13,7 @@
 Tvar var, tb > 2
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
(Tbool, Tvar _)
+(Tbool, Tvar Zero)
val f : ('env, 'a) typ > ('env, 'a) typ > int = <fun>
# Exception: Match_failure ("//toplevel//", 9, 1).
#
Index: testsuite/tests/typinggadts/pr6163.ml.principal.reference
===================================================================
 testsuite/tests/typinggadts/pr6163.ml.principal.reference (revision 16100)
+++ testsuite/tests/typinggadts/pr6163.ml.principal.reference (working copy)
@@ 13,6 +13,6 @@
 Succ (Succ (Succ (Succ Zero))) > "4"
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
Succ (Succ (Succ (Succ (Succ _))))
+Succ (Succ (Succ (Succ (Succ Zero))))
val f : aux > string = <fun>
#
Index: testsuite/tests/typinggadts/pr6163.ml.reference
===================================================================
 testsuite/tests/typinggadts/pr6163.ml.reference (revision 16100)
+++ testsuite/tests/typinggadts/pr6163.ml.reference (working copy)
@@ 13,6 +13,6 @@
 Succ (Succ (Succ (Succ Zero))) > "4"
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
Succ (Succ (Succ (Succ (Succ _))))
+Succ (Succ (Succ (Succ (Succ Zero))))
val f : aux > string = <fun>
#
Index: testsuite/tests/typinggadts/test.ml
===================================================================
 testsuite/tests/typinggadts/test.ml (revision 16100)
+++ testsuite/tests/typinggadts/test.ml (working copy)
@@ 91,6 +91,52 @@
end
;;
+module Exhaustive2 = struct
+ type _ t = Int : int t
+ let f (x : bool t option) = match x with None > ()
+end;;
+
+module PR6220 = struct
+ type 'a t = I : int t  F : float t
+ let f : int t > int = function I > 1
+ let g : int t > int = function I > 1  _ > 2 (* no warning *)
+end;;
+
+module PR6403 = struct
+ type (_, _) eq = Refl : ('a, 'a) eq
+ type empty = { bottom : 'a . 'a }
+ type ('a, 'b) sum = Left of 'a  Right of 'b
+
+ let notequal : ((int, bool) eq, empty) sum > empty = function
+  Right empty > empty
+end;;
+
+module PR6437 = struct
+ type ('a, 'b) ctx =
+  Nil : (unit, unit) ctx
+  Cons : ('a, 'b) ctx > ('a * unit, 'b * unit) ctx
+
+ type 'a var =
+  O : ('a * unit) var
+  S : 'a var > ('a * unit) var
+
+ let rec f : type g1 g2. (g1, g2) ctx * g1 var > g2 var = function
+  Cons g, O > O
+  Cons g, S n > S (f (g, n))
+ (* Nil, _ > (assert false) *) (* warns, but shouldn't *)
+end;;
+
+module PR6801 = struct
+ type _ value =
+  String : string > string value
+  Float : float > float value
+  Any
+
+ let print_string_value (x : string value) =
+ match x with
+  String s > print_endline s (* warn : Any *)
+end;;
+
module Existential_escape =
struct
type _ t = C : int > int t
@@ 108,7 +154,7 @@
;;
module Or_patterns =
struct
+ struct
type _ t =
 IntLit : int > int t
 BoolLit : bool > bool t
Index: testsuite/tests/typinggadts/test.ml.principal.reference
===================================================================
 testsuite/tests/typinggadts/test.ml.principal.reference (revision 16100)
+++ testsuite/tests/typinggadts/test.ml.principal.reference (working copy)
@@ 47,6 +47,43 @@
type 'a v = Foo : t > t v  Bar : u > u v
val same_type : 's v * 's v > bool
end
+# module Exhaustive2 :
+ sig type _ t = Int : int t val f : bool t option > unit end
+# module PR6220 :
+ sig
+ type 'a t = I : int t  F : float t
+ val f : int t > int
+ val g : int t > int
+ end
+# module PR6403 :
+ sig
+ type (_, _) eq = Refl : ('a, 'a) eq
+ type empty = { bottom : 'a. 'a; }
+ type ('a, 'b) sum = Left of 'a  Right of 'b
+ val notequal : ((int, bool) eq, empty) sum > empty
+ end
+# module PR6437 :
+ sig
+ type ('a, 'b) ctx =
+ Nil : (unit, unit) ctx
+  Cons : ('a, 'b) ctx > ('a * unit, 'b * unit) ctx
+ type 'a var = O : ('a * unit) var  S : 'a var > ('a * unit) var
+ val f : ('g1, 'g2) ctx * 'g1 var > 'g2 var
+ end
+# Characters 175221:
+ ....match x with
+  String s > print_endline s.................
+Warning 8: this patternmatching is not exhaustive.
+Here is an example of a value that is not matched:
+Any
+module PR6801 :
+ sig
+ type _ value =
+ String : string > string value
+  Float : float > float value
+  Any
+ val print_string_value : string value > unit
+ end
# Characters 118119:
let eval (D x) = x
^
@@ 55,7 +92,7 @@
The type constructor a#2 would escape its scope
# module Rectype :
sig type (_, _) t = C : ('a, 'a) t val f : ('s, 's * 's) t > unit end
# Characters 178186:
+# Characters 180188:
 (IntLit _  BoolLit _) > ()
^^^^^^^^
Error: This pattern matches values of type int t
@@ 286,14 +323,14 @@
^
Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < foo : int >
 Type ex#17 = < bar : int; .. > is not compatible with type < >
+ Type ex#23 = < bar : int; .. > is not compatible with type < >
The second object type has no method bar
# Characters 9899:
(x:<foo:int;bar:int>)
^
Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < bar : int; foo : int >
 Type ex#19 = < bar : int; .. > is not compatible with type
+ Type ex#25 = < bar : int; .. > is not compatible with type
< bar : int >
The first object type has an abstract row, it cannot be closed
# Characters 9899:
@@ 301,7 +338,7 @@
^
Error: This expression has type < bar : int; foo : int; .. >
but an expression was expected of type 'a
 The type constructor ex#22 would escape its scope
+ The type constructor ex#28 would escape its scope
# val g : 'a > 'a int_foo > 'a int_bar > 'a = <fun>
# val g : 'a > 'a int_foo > 'a int_bar > 'a * int * int = <fun>
# type 'a ty = Int : int > int ty
Index: testsuite/tests/typinggadts/test.ml.reference
===================================================================
 testsuite/tests/typinggadts/test.ml.reference (revision 16100)
+++ testsuite/tests/typinggadts/test.ml.reference (working copy)
@@ 47,6 +47,43 @@
type 'a v = Foo : t > t v  Bar : u > u v
val same_type : 's v * 's v > bool
end
+# module Exhaustive2 :
+ sig type _ t = Int : int t val f : bool t option > unit end
+# module PR6220 :
+ sig
+ type 'a t = I : int t  F : float t
+ val f : int t > int
+ val g : int t > int
+ end
+# module PR6403 :
+ sig
+ type (_, _) eq = Refl : ('a, 'a) eq
+ type empty = { bottom : 'a. 'a; }
+ type ('a, 'b) sum = Left of 'a  Right of 'b
+ val notequal : ((int, bool) eq, empty) sum > empty
+ end
+# module PR6437 :
+ sig
+ type ('a, 'b) ctx =
+ Nil : (unit, unit) ctx
+  Cons : ('a, 'b) ctx > ('a * unit, 'b * unit) ctx
+ type 'a var = O : ('a * unit) var  S : 'a var > ('a * unit) var
+ val f : ('g1, 'g2) ctx * 'g1 var > 'g2 var
+ end
+# Characters 175221:
+ ....match x with
+  String s > print_endline s.................
+Warning 8: this patternmatching is not exhaustive.
+Here is an example of a value that is not matched:
+Any
+module PR6801 :
+ sig
+ type _ value =
+ String : string > string value
+  Float : float > float value
+  Any
+ val print_string_value : string value > unit
+ end
# Characters 118119:
let eval (D x) = x
^
@@ 55,7 +92,7 @@
The type constructor a#2 would escape its scope
# module Rectype :
sig type (_, _) t = C : ('a, 'a) t val f : ('s, 's * 's) t > unit end
# Characters 178186:
+# Characters 180188:
 (IntLit _  BoolLit _) > ()
^^^^^^^^
Error: This pattern matches values of type int t
@@ 273,14 +310,14 @@
^
Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < foo : int >
 Type ex#17 = < bar : int; .. > is not compatible with type < >
+ Type ex#23 = < bar : int; .. > is not compatible with type < >
The second object type has no method bar
# Characters 9899:
(x:<foo:int;bar:int>)
^
Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < bar : int; foo : int >
 Type ex#19 = < bar : int; .. > is not compatible with type
+ Type ex#25 = < bar : int; .. > is not compatible with type
< bar : int >
The first object type has an abstract row, it cannot be closed
# Characters 9899:
@@ 288,7 +325,7 @@
^
Error: This expression has type < bar : int; foo : int; .. >
but an expression was expected of type 'a
 The type constructor ex#22 would escape its scope
+ The type constructor ex#28 would escape its scope
# val g : 'a > 'a int_foo > 'a int_bar > 'a = <fun>
# val g : 'a > 'a int_foo > 'a int_bar > 'a * int * int = <fun>
# type 'a ty = Int : int > int ty
Index: typing/ctype.ml
===================================================================
 typing/ctype.ml (revision 16100)
+++ typing/ctype.ml (working copy)
@@ 116,6 +116,20 @@
let global_level = ref 1
let saved_level = ref []
+type levels =
+ { current_level: int; nongen_level: int; global_level: int;
+ saved_level: (int * int) list; }
+let save_levels () =
+ { current_level = !current_level;
+ nongen_level = !nongen_level;
+ global_level = !global_level;
+ saved_level = !saved_level }
+let set_levels l =
+ current_level := l.current_level;
+ nongen_level := l.nongen_level;
+ global_level := l.global_level;
+ saved_level := l.saved_level
+
let get_current_level () = !current_level
let init_def level = current_level := level; nongen_level := level
let begin_def () =
Index: typing/ctype.mli
===================================================================
 typing/ctype.mli (revision 16100)
+++ typing/ctype.mli (working copy)
@@ 37,6 +37,11 @@
val increase_global_level: unit > int
val restore_global_level: int > unit
(* This pair of functions is only used in Typetexp *)
+type levels =
+ { current_level: int; nongen_level: int; global_level: int;
+ saved_level: (int * int) list; }
+val save_levels: unit > levels
+val set_levels: levels > unit
val newty: type_desc > type_expr
val newvar: ?name:string > unit > type_expr
Index: typing/parmatch.ml
===================================================================
 typing/parmatch.ml (revision 16100)
+++ typing/parmatch.ml (working copy)
@@ 625,11 +625,11 @@
 ({pat_desc = Tpat_construct(_,c,_);pat_type=typ},_) :: _ >
if c.cstr_consts < 0 then false (* extensions *)
else
 if ignore_generalized then
+ if ignore_generalized then true
(* remove generalized constructors;
those cases will be handled separately *)
 let env = clean_env env in
 List.length env = c.cstr_normal
+ (*let env = clean_env env in
+ List.length env = c.cstr_normal*)
else
List.length env = c.cstr_consts + c.cstr_nonconsts
@@ 715,20 +715,47 @@
(* build a pattern from a constructor list *)
let pat_of_constr ex_pat cstr =
 {ex_pat with pat_desc =
 Tpat_construct (mknoloc (Longident.Lident "?pat_of_constr?"),
 cstr,omegas cstr.cstr_arity)}
+ {ex_pat with pat_desc =
+ Tpat_construct (mknoloc (Longident.Lident "?pat_of_constr?"),
+ cstr, omegas cstr.cstr_arity)}
let rec pat_of_constrs ex_pat = function
 [] > raise Empty
 [cstr] > pat_of_constr ex_pat cstr
 cstr::rem >
 {ex_pat with
 pat_desc=
 Tpat_or
 (pat_of_constr ex_pat cstr,
 pat_of_constrs ex_pat rem, None)}
+let rec orify_many = function
+ [] > assert false
+ [x] > x
+ x :: xs >
+ make_pat (Tpat_or (x, orify_many xs, None)) x.pat_type x.pat_env
+let pat_of_constrs ex_pat cstrs =
+ if cstrs = [] then raise Empty else
+ orify_many (List.map (pat_of_constr ex_pat) cstrs)
+
+let pats_of_type env ty =
+ let ty' = Ctype.expand_head env ty in
+ match ty'.desc with
+  Tconstr (path, _, _) >
+ begin match Env.find_type path env with
+  {type_kind = Type_variant cl}
+ when List.for_all (fun cd > cd.Types.cd_res <> None) cl >
+ let cstrs = fst (Env.find_type_descrs path env) in
+ List.map
+ (pat_of_constr {omega with pat_type=ty; pat_env=env})
+ cstrs
+  _ > [omega]
+ end
+  _ > [omega]
+
+let pat_of_constr_gadt ex_pat cstr =
+ let no_split = cstr.cstr_generalized  cstr.cstr_arity = 0 in
+ if no_split then pat_of_constr ex_pat cstr else
+ let env = ex_pat.pat_env in
+ let ty_args, ty_res = Ctype.instance_constructor cstr in
+ (try Ctype.unify env ty_res ex_pat.pat_type with
+ Ctype.Unify _ > assert false);
+ let id = mknoloc (Longident.Lident cstr.cstr_name) in
+ let patl =
+ List.map (fun ty > {omega with pat_env = env; pat_type = ty}) ty_args in
+ {ex_pat with pat_desc = Tpat_construct (id, cstr, patl)}
+
let rec get_variant_constructors env ty =
match (Ctype.repr ty).desc with
 Tconstr (path,_,_) > begin
@@ 778,7 +805,7 @@
in the first column of env
*)
let build_other ext env = match env with
+let build_other ext env = match env with
 ({pat_desc = Tpat_construct (lid,
({cstr_tag=Cstr_extension _} as c),_)},_) :: _ >
let c = {c with cstr_name = "*extension*"} in
@@ 910,10 +937,9 @@
 _ > fatal_error "Parmatch.get_tag" in
let all_tags = List.map (fun (p,_) > get_tag p) env in
let cnstrs = complete_constrs p all_tags in
 let pats = List.map (pat_of_constr p) cnstrs in
+ List.map (pat_of_constr_gadt p) cnstrs
(* List.iter (Format.eprintf "%a@." top_pretty) pats;
Format.eprintf "@.@."; *)
 pats
 _ > assert false
(*
@@ 981,15 +1007,6 @@
 Rnone (* No matching value *)
 Rsome of 'a (* This matching value *)
let rec orify_many =
 let orify x y =
 make_pat (Tpat_or (x, y, None)) x.pat_type x.pat_env
 in
 function
  [] > assert false
  [x] > x
  x :: xs > orify x (orify_many xs)

let rec try_many f = function
 [] > Rnone
 (p,pss)::rest >
@@ 1193,12 +1210,12 @@
try_non_omega rem && ok
 [] > true
in
 if full_match true (tdefs=None) constrs then
+ if full_match false (tdefs=None) constrs then
try_non_omega constrs
else if tdefs = None then
pressure_variants None (filter_extra pss)
else
 let full = full_match true true constrs in
+ let full = full_match false true constrs in
let ok =
if full then try_non_omega constrs
else try_non_omega (filter_all q0 (mark_partial pss))
@@ 1662,119 +1679,70 @@
(* Exhaustiveness check *)
(************************)

 let rec get_first f =
 function
  [] > None
  x :: xs >
 match f x with
  None > get_first f xs
  x > x


(* conversion from Typedtree.pattern to Parsetree.pattern list *)
module Conv = struct
open Parsetree
let mkpat desc = Ast_helper.Pat.mk desc
 let rec select : 'a list list > 'a list list =
 function
  xs :: [] > List.map (fun y > [y]) xs
  (x::xs)::ys >
 List.map
 (fun lst > x :: lst)
 (select ys)
 @
 select (xs::ys)
  _ > []

let name_counter = ref 0
let fresh name =
let current = !name_counter in
name_counter := !name_counter + 1;
"#$" ^ name ^ string_of_int current
 let conv (typed: Typedtree.pattern) :
 Parsetree.pattern list *
 (string, Types.constructor_description) Hashtbl.t *
 (string, Types.label_description) Hashtbl.t
 =
 let constrs = Hashtbl.create 0 in
 let labels = Hashtbl.create 0 in
+ let conv typed =
+ let constrs = Hashtbl.create 7 in
+ let labels = Hashtbl.create 7 in
let rec loop pat =
match pat.pat_desc with
 Tpat_or (a,b,_) >
 loop a @ loop b
  Tpat_any  Tpat_constant _  Tpat_var _ >
 [mkpat Ppat_any]
+ Tpat_or (pa,pb,_) >
+ mkpat (Ppat_or (loop pa, loop pb))
+  Tpat_any
+  Tpat_var _
+  Tpat_constant _ >
+ mkpat Ppat_any
 Tpat_alias (p,_,_) > loop p
 Tpat_tuple lst >
 let results = select (List.map loop lst) in
 List.map
 (fun lst > mkpat (Ppat_tuple lst))
 results
  Tpat_construct (cstr_lid, cstr,lst) >
+ mkpat (Ppat_tuple (List.map loop lst))
+  Tpat_construct (cstr_lid, cstr, lst) >
let id = fresh cstr.cstr_name in
let lid = { cstr_lid with txt = Longident.Lident id } in
Hashtbl.add constrs id cstr;
 let results = select (List.map loop lst) in
 begin match lst with
 [] >
 [mkpat (Ppat_construct(lid, None))]
  _ >
 List.map
 (fun lst >
 let arg =
 match lst with
 [] > assert false
  [x] > Some x
  _ > Some (mkpat (Ppat_tuple lst))
 in
 mkpat (Ppat_construct(lid, arg)))
 results
 end
+ let arg =
+ match List.map loop lst with
+  [] > None
+  [p] > Some p
+  lst > Some (mkpat (Ppat_tuple lst))
+ in
+ mkpat (Ppat_construct(lid, arg))
 Tpat_variant(label,p_opt,row_desc) >
 begin match p_opt with
  None >
 [mkpat (Ppat_variant(label, None))]
  Some p >
 let results = loop p in
 List.map
 (fun p >
 mkpat (Ppat_variant(label, Some p)))
 results
 end
+ let arg = Misc.may_map loop p_opt in
+ mkpat (Ppat_variant(label, arg))
 Tpat_record (subpatterns, _closed_flag) >
 let pats =
 select
 (List.map (fun (_,_,x) > loop x) subpatterns)
 in
 let label_idents =
 List.map
 (fun (_,lbl,_) >
+ let fields =
+ List.map
+ (fun (_, lbl, p) >
let id = fresh lbl.lbl_name in
Hashtbl.add labels id lbl;
 Longident.Lident id)
 subpatterns
 in
 List.map
 (fun lst >
 let lst = List.map2 (fun lid pat >
 (mknoloc lid, pat)
 ) label_idents lst in
 mkpat (Ppat_record (lst, Open)))
 pats
+ (mknoloc (Longident.Lident id), loop p))
+ subpatterns
+ in
+ mkpat (Ppat_record (fields, Open))
 Tpat_array lst >
 let results = select (List.map loop lst) in
 List.map (fun lst > mkpat (Ppat_array lst)) results
+ mkpat (Ppat_array (List.map loop lst))
 Tpat_lazy p >
 let results = loop p in
 List.map (fun p > mkpat (Ppat_lazy p)) results
+ mkpat (Ppat_lazy (loop p))
in
let ps = loop typed in
(ps, constrs, labels)
end
+let ppat_of_type env ty =
+ match pats_of_type env ty with
+ [{pat_desc = Tpat_any}] >
+ (Conv.mkpat Parsetree.Ppat_any, Hashtbl.create 0, Hashtbl.create 0)
+  pats >
+ Conv.conv (orify_many pats)
let do_check_partial ?pred exhaust loc casel pss = match pss with
 [] >
@@ 1798,12 +1766,12 @@
let v =
match pred with
 Some pred >
 let (patterns,constrs,labels) = Conv.conv u in
+ let (pattern,constrs,labels) = Conv.conv u in
(* Hashtbl.iter (fun s (path, _) >
Printf.fprintf stderr "CONV: %s > %s \n%!" s (Path.name path))
constrs
; *)
 get_first (pred constrs labels) patterns
+ pred constrs labels pattern
 None > Some u
in
begin match v with
Index: typing/parmatch.mli
===================================================================
 typing/parmatch.mli (revision 16100)
+++ typing/parmatch.mli (working copy)
@@ 51,6 +51,11 @@
val pat_of_constr : pattern > constructor_description > pattern
val complete_constrs :
pattern > constructor_tag list > constructor_description list
+val ppat_of_type :
+ Env.t > type_expr >
+ Parsetree.pattern *
+ (string, constructor_description) Hashtbl.t *
+ (string, label_description) Hashtbl.t
val pressure_variants: Env.t > pattern list > unit
val check_partial: Location.t > case list > partial
Index: typing/typecore.ml
===================================================================
 typing/typecore.ml (revision 16100)
+++ typing/typecore.ml (working copy)
@@ 826,7 +826,11 @@
 ({ txt = Longident.Ldot (modname, _) }, _) :: _ > Some modname
 _ :: rest > find_record_qual rest
let type_label_a_list ?labels loc closed env type_lbl_a opath lid_a_list =
+let map_fold_cont f xs k =
+ List.fold_right (fun x k ys > f x (fun y > k (y :: ys)))
+ xs (fun ys > k (List.rev ys)) []
+
+let type_label_a_list ?labels loc closed env type_lbl_a opath lid_a_list k =
let lbl_a_list =
match lid_a_list, labels with
({txt=Longident.Lident s}, _)::_, Some labels when Hashtbl.mem labels s >
@@ 856,7 +860,7 @@
(fun (_,lbl1,_) (_,lbl2,_) > compare lbl1.lbl_pos lbl2.lbl_pos)
lbl_a_list
in
 List.map type_lbl_a lbl_a_list
+ map_fold_cont type_lbl_a lbl_a_list k
;;
(* Checks over the labels mentioned in a record pattern:
@@ 916,32 +920,59 @@
 Normal
 Inside_or
+(* Remember current state for backtracking.
+ No variable information, as we only backtrack on
+ patterns without variables (cf. assert statements). *)
+type state =
+ { snapshot: Btype.snapshot;
+ levels: Ctype.levels;
+ env: Env.t; }
+let save_state env =
+ { snapshot = Btype.snapshot ();
+ levels = Ctype.save_levels ();
+ env = !env; }
+let set_state s env =
+ Btype.backtrack s.snapshot;
+ Ctype.set_levels s.levels;
+ env := s.env
+
(* type_pat propagates the expected type as well as maps for
constructors and labels.
Unification may update the typing environment. *)
let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
 let type_pat ?(mode=mode) ?(env=env) =
+(* constrs <> None => called from parmatch: backtrack on orpatterns
+ labels <> None => explode Ppat_any for gadts *)
+let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty k =
+ let type_pat ?(constrs=constrs) ?(labels=labels) ?(mode=mode) ?(env=env) =
type_pat ~constrs ~labels ~no_existentials ~mode ~env in
let loc = sp.ppat_loc in
+ let rp k x : pattern = if constrs = None then k (rp x) else k x in
match sp.ppat_desc with
Ppat_any >
 rp {
 pat_desc = Tpat_any;
+ let k' d = rp k {
+ pat_desc = d;
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
pat_env = !env }
+ in
+ if labels <> None then
+ let (sp, constrs, labels) = Parmatch.ppat_of_type !env expected_ty in
+ if sp.ppat_desc = Parsetree.Ppat_any then k' Tpat_any
+ else type_pat ~constrs:(Some constrs) ~labels:None sp expected_ty k
+ else k' Tpat_any
 Ppat_var name >
+ assert (constrs = None);
let id = enter_variable loc name expected_ty in
 rp {
+ rp k {
pat_desc = Tpat_var (id, name);
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
pat_env = !env }
 Ppat_unpack name >
+ assert (constrs = None);
let id = enter_variable loc name expected_ty ~is_module:true in
 rp {
+ rp k {
pat_desc = Tpat_var (id, name);
pat_loc = sp.ppat_loc;
pat_extra=[Tpat_unpack, loc, sp.ppat_attributes];
@@ 951,6 +982,7 @@
 Ppat_constraint({ppat_desc=Ppat_var name; ppat_loc=lloc},
({ptyp_desc=Ptyp_poly _} as sty)) >
(* explicitly polymorphic type *)
+ assert (constrs = None);
let cty, force = Typetexp.transl_simple_type_delayed !env sty in
let ty = cty.ctyp_type in
unify_pat_types lloc !env ty expected_ty;
@@ 962,7 +994,7 @@
end_def ();
generalize ty';
let id = enter_variable lloc name ty' in
 rp {
+ rp k {
pat_desc = Tpat_var (id, name);
pat_loc = lloc;
pat_extra = [Tpat_constraint cty, loc, sp.ppat_attributes];
@@ 973,21 +1005,22 @@
 _ > assert false
end
 Ppat_alias(sq, name) >
 let q = type_pat sq expected_ty in
 begin_def ();
 let ty_var = build_as_type !env q in
 end_def ();
 generalize ty_var;
 let id = enter_variable ~is_as_variable:true loc name ty_var in
 rp {
 pat_desc = Tpat_alias(q, id, name);
 pat_loc = loc; pat_extra=[];
 pat_type = q.pat_type;
 pat_attributes = sp.ppat_attributes;
 pat_env = !env }
+ assert (constrs = None);
+ type_pat sq expected_ty (fun q >
+ begin_def ();
+ let ty_var = build_as_type !env q in
+ end_def ();
+ generalize ty_var;
+ let id = enter_variable ~is_as_variable:true loc name ty_var in
+ rp k {
+ pat_desc = Tpat_alias(q, id, name);
+ pat_loc = loc; pat_extra=[];
+ pat_type = q.pat_type;
+ pat_attributes = sp.ppat_attributes;
+ pat_env = !env })
 Ppat_constant cst >
unify_pat_types loc !env (type_constant cst) expected_ty;
 rp {
+ rp k {
pat_desc = Tpat_constant cst;
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
@@ 1005,7 +1038,7 @@
in
let p = if c1 <= c2 then loop c1 c2 else loop c2 c1 in
let p = {p with ppat_loc=loc} in
 type_pat p expected_ty
+ type_pat ~labels:None p expected_ty k
(* TODO: record 'extra' to remember about interval *)
 Ppat_interval _ >
raise (Error (loc, !env, Invalid_interval))
@@ 1015,13 +1048,13 @@
let spl_ann = List.map (fun p > (p,newvar ())) spl in
let ty = newty (Ttuple(List.map snd spl_ann)) in
unify_pat_types loc !env ty expected_ty;
 let pl = List.map (fun (p,t) > type_pat p t) spl_ann in
 rp {
+ map_fold_cont (fun (p,t) > type_pat p t) spl_ann (fun pl >
+ rp k {
pat_desc = Tpat_tuple pl;
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
 pat_env = !env }
+ pat_env = !env })
 Ppat_construct(lid, sarg) >
let opath =
try
@@ 1089,13 +1122,14 @@
in
if constr.cstr_inlined <> None then List.iter check_non_escaping sargs;
 let args = List.map2 (fun p t > type_pat p t) sargs ty_args in
 rp {
 pat_desc=Tpat_construct(lid, constr, args);
 pat_loc = loc; pat_extra=[];
 pat_type = expected_ty;
 pat_attributes = sp.ppat_attributes;
 pat_env = !env }
+ map_fold_cont (fun (p,t) > type_pat p t) (List.combine sargs ty_args)
+ (fun args >
+ rp k {
+ pat_desc=Tpat_construct(lid, constr, args);
+ pat_loc = loc; pat_extra=[];
+ pat_type = expected_ty;
+ pat_attributes = sp.ppat_attributes;
+ pat_env = !env })
 Ppat_variant(l, sarg) >
let arg_type = match sarg with None > []  Some _ > [newvar()] in
let row = { row_fields =
@@ 1106,18 +1140,19 @@
row_fixed = false;
row_name = None } in
unify_pat_types loc !env (newty (Tvariant row)) expected_ty;
 let arg =
 (* PR#6235: propagate type information *)
 match sarg, arg_type with
 Some p, [ty] > Some (type_pat p ty)
  _ > None
 in
 rp {
+ let k arg =
+ rp k {
pat_desc = Tpat_variant(l, arg, ref {row with row_more = newvar()});
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
pat_env = !env }
+ in begin
+ (* PR#6235: propagate type information *)
+ match sarg, arg_type with
+ Some p, [ty] > type_pat p ty (fun p > k (Some p))
+  _ > k None
+ end
 Ppat_record(lid_sp_list, closed) >
if lid_sp_list = [] then
Syntaxerr.ill_formed_ast loc "Records cannot be empty.";
@@ 1127,7 +1162,7 @@
Some (p0, p, true), expected_ty
with Not_found > None, newvar ()
in
 let type_label_pat (label_lid, label, sarg) =
+ let type_label_pat (label_lid, label, sarg) k =
begin_def ();
let (vars, ty_arg, ty_res) = instance_label false label in
if vars = [] then end_def ();
@@ 1137,55 +1172,72 @@
raise(Error(label_lid.loc, !env,
Label_mismatch(label_lid.txt, trace)))
end;
 let arg = type_pat sarg ty_arg in
 if vars <> [] then begin
 end_def ();
 generalize ty_arg;
 List.iter generalize vars;
 let instantiated tv =
 let tv = expand_head !env tv in
 not (is_Tvar tv)  tv.level <> generic_level in
 if List.exists instantiated vars then
 raise (Error(label_lid.loc, !env, Polymorphic_label label_lid.txt))
 end;
 (label_lid, label, arg)
+ type_pat sarg ty_arg (fun arg >
+ if vars <> [] then begin
+ end_def ();
+ generalize ty_arg;
+ List.iter generalize vars;
+ let instantiated tv =
+ let tv = expand_head !env tv in
+ not (is_Tvar tv)  tv.level <> generic_level in
+ if List.exists instantiated vars then
+ raise
+ (Error(label_lid.loc, !env, Polymorphic_label label_lid.txt))
+ end;
+ k (label_lid, label, arg))
in
 let lbl_pat_list =
 wrap_disambiguate "This record pattern is expected to have" expected_ty
 (type_label_a_list ?labels loc false !env type_label_pat opath)
 lid_sp_list
 in
 check_recordpat_labels loc lbl_pat_list closed;
 unify_pat_types loc !env record_ty expected_ty;
 rp {
+ let k' k lbl_pat_list =
+ check_recordpat_labels loc lbl_pat_list closed;
+ unify_pat_types loc !env record_ty expected_ty;
+ rp k {
pat_desc = Tpat_record (lbl_pat_list, closed);
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
pat_env = !env }
+ in
+ if constrs = None then
+ k (wrap_disambiguate "This record pattern is expected to have"
+ expected_ty
+ (type_label_a_list ?labels loc false !env type_label_pat opath
+ lid_sp_list)
+ (k' (fun x > x)))
+ else
+ type_label_a_list ?labels loc false !env type_label_pat opath
+ lid_sp_list (k' k)
 Ppat_array spl >
let ty_elt = newvar() in
unify_pat_types
loc !env (instance_def (Predef.type_array ty_elt)) expected_ty;
let spl_ann = List.map (fun p > (p,newvar())) spl in
 let pl = List.map (fun (p,t) > type_pat p ty_elt) spl_ann in
 rp {
+ map_fold_cont (fun (p,t) > type_pat p ty_elt) spl_ann (fun pl >
+ rp k {
pat_desc = Tpat_array pl;
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
 pat_env = !env }
+ pat_env = !env })
 Ppat_or(sp1, sp2) >
+ if constrs <> None &&
+ match sp1.ppat_desc, sp2.ppat_desc with
+ Ppat_constant _, _  _, Ppat_constant _ > false
+  _ > true
+ then
+ let state = save_state env in
+ try type_pat sp1 expected_ty k with exn when exn <> Exit >
+ set_state state env;
+ type_pat sp2 expected_ty k
+ else
let initial_pattern_variables = !pattern_variables in
 let p1 = type_pat ~mode:Inside_or sp1 expected_ty in
+ let p1 = type_pat ~mode:Inside_or sp1 expected_ty (fun x > x) in
let p1_variables = !pattern_variables in
pattern_variables := initial_pattern_variables;
 let p2 = type_pat ~mode:Inside_or sp2 expected_ty in
+ let p2 = type_pat ~mode:Inside_or sp2 expected_ty (fun x > x) in
let p2_variables = !pattern_variables in
let alpha_env =
enter_orpat_variables loc !env p1_variables p2_variables in
pattern_variables := p1_variables;
 rp {
+ rp k {
pat_desc = Tpat_or(p1, alpha_pat alpha_env p2, None);
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
@@ 1195,13 +1247,13 @@
let nv = newvar () in
unify_pat_types loc !env (instance_def (Predef.type_lazy_t nv))
expected_ty;
 let p1 = type_pat sp1 nv in
 rp {
+ type_pat sp1 nv (fun p1 >
+ rp k {
pat_desc = Tpat_lazy p1;
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
 pat_env = !env }
+ pat_env = !env })
 Ppat_constraint(sp, sty) >
(* Separate when not already separated by !principal *)
let separate = true in
@@ 1216,27 +1268,28 @@
end else ty, ty
in
unify_pat_types loc !env ty expected_ty;
 let p = type_pat sp expected_ty' in
 (*Format.printf "%a@.%a@."
 Printtyp.raw_type_expr ty
 Printtyp.raw_type_expr p.pat_type;*)
 pattern_force := force :: !pattern_force;
 let extra = (Tpat_constraint cty, loc, sp.ppat_attributes) in
 if separate then
 match p.pat_desc with
 Tpat_var (id,s) >
 {p with pat_type = ty;
 pat_desc = Tpat_alias
 ({p with pat_desc = Tpat_any; pat_attributes = []}, id,s);
 pat_extra = [extra];
 }
  _ > {p with pat_type = ty;
 pat_extra = extra :: p.pat_extra}
 else p
+ type_pat sp expected_ty' (fun p >
+ (*Format.printf "%a@.%a@."
+ Printtyp.raw_type_expr ty
+ Printtyp.raw_type_expr p.pat_type;*)
+ pattern_force := force :: !pattern_force;
+ let extra = (Tpat_constraint cty, loc, sp.ppat_attributes) in
+ let p =
+ if not separate then p else
+ match p.pat_desc with
+ Tpat_var (id,s) >
+ {p with pat_type = ty;
+ pat_desc = Tpat_alias
+ ({p with pat_desc = Tpat_any; pat_attributes = []}, id,s);
+ pat_extra = [extra];
+ }
+  _ > {p with pat_type = ty;
+ pat_extra = extra :: p.pat_extra}
+ in k p)
 Ppat_type lid >
let (path, p,ty) = build_or_pat !env loc lid.txt in
unify_pat_types loc !env ty expected_ty;
 { p with pat_extra =
+ k { p with pat_extra =
(Tpat_type (path, lid), loc, sp.ppat_attributes) :: p.pat_extra }
 Ppat_exception _ >
raise (Error (loc, !env, Exception_pattern_below_toplevel))
@@ 1249,7 +1302,7 @@
try
let r =
type_pat ~no_existentials:(not allow_existentials) ~constrs ~labels
 ~mode:Normal ~env sp expected_ty in
+ ~mode:Normal ~env sp expected_ty (fun x > x) in
iter_pattern (fun p > p.pat_env < !env) r;
newtype_level := None;
r
@@ 2085,9 +2138,9 @@
let lbl_exp_list =
wrap_disambiguate "This record expression is expected to have" ty_record
(type_label_a_list loc closed env
 (type_label_exp true env loc ty_record)
 opath)
 lid_sexp_list
+ (fun e k > k (type_label_exp true env loc ty_record e))
+ opath lid_sexp_list)
+ (fun x > x)
in
unify_exp_types loc env ty_record (instance env ty_expected);
type_pat_cps3.diff [^] (45,336 bytes) 20150518 06:04 [Show Content] [Hide Content]Index: testsuite/tests/typinggadts/omega07.ml.principal.reference
===================================================================
 testsuite/tests/typinggadts/omega07.ml.principal.reference (revision 16123)
+++ testsuite/tests/typinggadts/omega07.ml.principal.reference (working copy)
@@ 63,15 +63,7 @@
# val smaller : ('a succ, 'b succ) le > ('a, 'b) le = <fun>
# type (_, _) diff = Diff : 'c nat * ('a, 'c, 'b) plus > ('a, 'b) diff
# * * * * * * * * * val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
# Characters 87243:
 ..match a, b,le with (* warning *)
  NZ, m, LeZ _ > Diff (m, PlusZ m)
  NS x, NS y, LeS q >
 match diff q x y with Diff (m, p) > Diff (m, PlusS p)
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
(NS _, NZ, _)
val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
+# val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
# val diff : ('a, 'b) le > 'b nat > ('a, 'b) diff = <fun>
# type (_, _) filter = Filter : ('m, 'n) le * ('a, 'm) seq > ('a, 'n) filter
val leS' : ('m, 'n) le > ('m, 'n succ) le = <fun>
Index: testsuite/tests/typinggadts/omega07.ml.reference
===================================================================
 testsuite/tests/typinggadts/omega07.ml.reference (revision 16123)
+++ testsuite/tests/typinggadts/omega07.ml.reference (working copy)
@@ 63,15 +63,7 @@
# val smaller : ('a succ, 'b succ) le > ('a, 'b) le = <fun>
# type (_, _) diff = Diff : 'c nat * ('a, 'c, 'b) plus > ('a, 'b) diff
# * * * * * * * * * val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
# Characters 87243:
 ..match a, b,le with (* warning *)
  NZ, m, LeZ _ > Diff (m, PlusZ m)
  NS x, NS y, LeS q >
 match diff q x y with Diff (m, p) > Diff (m, PlusS p)
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
(NS _, NZ, _)
val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
+# val diff : ('a, 'b) le > 'a nat > 'b nat > ('a, 'b) diff = <fun>
# val diff : ('a, 'b) le > 'b nat > ('a, 'b) diff = <fun>
# type (_, _) filter = Filter : ('m, 'n) le * ('a, 'm) seq > ('a, 'n) filter
val leS' : ('m, 'n) le > ('m, 'n succ) le = <fun>
Index: testsuite/tests/typinggadts/pr5332.ml.reference
===================================================================
 testsuite/tests/typinggadts/pr5332.ml.reference (revision 16123)
+++ testsuite/tests/typinggadts/pr5332.ml.reference (working copy)
@@ 13,7 +13,7 @@
 Tvar var, tb > 2
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
(Tbool, Tvar _)
+(Tbool, Tvar Zero)
val f : ('env, 'a) typ > ('env, 'a) typ > int = <fun>
# Exception: Match_failure ("//toplevel//", 9, 1).
#
Index: testsuite/tests/typinggadts/pr6163.ml.principal.reference
===================================================================
 testsuite/tests/typinggadts/pr6163.ml.principal.reference (revision 16123)
+++ testsuite/tests/typinggadts/pr6163.ml.principal.reference (working copy)
@@ 13,6 +13,6 @@
 Succ (Succ (Succ (Succ Zero))) > "4"
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
Succ (Succ (Succ (Succ (Succ _))))
+Succ (Succ (Succ (Succ (Succ Zero))))
val f : aux > string = <fun>
#
Index: testsuite/tests/typinggadts/pr6163.ml.reference
===================================================================
 testsuite/tests/typinggadts/pr6163.ml.reference (revision 16123)
+++ testsuite/tests/typinggadts/pr6163.ml.reference (working copy)
@@ 13,6 +13,6 @@
 Succ (Succ (Succ (Succ Zero))) > "4"
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
Succ (Succ (Succ (Succ (Succ _))))
+Succ (Succ (Succ (Succ (Succ Zero))))
val f : aux > string = <fun>
#
Index: testsuite/tests/typinggadts/test.ml
===================================================================
 testsuite/tests/typinggadts/test.ml (revision 16123)
+++ testsuite/tests/typinggadts/test.ml (working copy)
@@ 97,6 +97,52 @@
class d (Just x) = object method x : int = x end
end;;
+module Exhaustive2 = struct
+ type _ t = Int : int t
+ let f (x : bool t option) = match x with None > ()
+end;;
+
+module PR6220 = struct
+ type 'a t = I : int t  F : float t
+ let f : int t > int = function I > 1
+ let g : int t > int = function I > 1  _ > 2 (* no warning *)
+end;;
+
+module PR6403 = struct
+ type (_, _) eq = Refl : ('a, 'a) eq
+ type empty = { bottom : 'a . 'a }
+ type ('a, 'b) sum = Left of 'a  Right of 'b
+
+ let notequal : ((int, bool) eq, empty) sum > empty = function
+  Right empty > empty
+end;;
+
+module PR6437 = struct
+ type ('a, 'b) ctx =
+  Nil : (unit, unit) ctx
+  Cons : ('a, 'b) ctx > ('a * unit, 'b * unit) ctx
+
+ type 'a var =
+  O : ('a * unit) var
+  S : 'a var > ('a * unit) var
+
+ let rec f : type g1 g2. (g1, g2) ctx * g1 var > g2 var = function
+  Cons g, O > O
+  Cons g, S n > S (f (g, n))
+ (* Nil, _ > (assert false) *) (* warns, but shouldn't *)
+end;;
+
+module PR6801 = struct
+ type _ value =
+  String : string > string value
+  Float : float > float value
+  Any
+
+ let print_string_value (x : string value) =
+ match x with
+  String s > print_endline s (* warn : Any *)
+end;;
+
module Existential_escape =
struct
type _ t = C : int > int t
@@ 114,7 +160,7 @@
;;
module Or_patterns =
struct
+ struct
type _ t =
 IntLit : int > int t
 BoolLit : bool > bool t
Index: testsuite/tests/typinggadts/test.ml.principal.reference
===================================================================
 testsuite/tests/typinggadts/test.ml.principal.reference (revision 16123)
+++ testsuite/tests/typinggadts/test.ml.principal.reference (working copy)
@@ 65,6 +65,43 @@
type _ opt = Just : 'a > 'a opt  Nothing : 'a opt
class d : int opt > object method x : int end
end
+# module Exhaustive2 :
+ sig type _ t = Int : int t val f : bool t option > unit end
+# module PR6220 :
+ sig
+ type 'a t = I : int t  F : float t
+ val f : int t > int
+ val g : int t > int
+ end
+# module PR6403 :
+ sig
+ type (_, _) eq = Refl : ('a, 'a) eq
+ type empty = { bottom : 'a. 'a; }
+ type ('a, 'b) sum = Left of 'a  Right of 'b
+ val notequal : ((int, bool) eq, empty) sum > empty
+ end
+# module PR6437 :
+ sig
+ type ('a, 'b) ctx =
+ Nil : (unit, unit) ctx
+  Cons : ('a, 'b) ctx > ('a * unit, 'b * unit) ctx
+ type 'a var = O : ('a * unit) var  S : 'a var > ('a * unit) var
+ val f : ('g1, 'g2) ctx * 'g1 var > 'g2 var
+ end
+# Characters 175221:
+ ....match x with
+  String s > print_endline s.................
+Warning 8: this patternmatching is not exhaustive.
+Here is an example of a value that is not matched:
+Any
+module PR6801 :
+ sig
+ type _ value =
+ String : string > string value
+  Float : float > float value
+  Any
+ val print_string_value : string value > unit
+ end
# Characters 118119:
let eval (D x) = x
^
@@ 73,7 +110,7 @@
The type constructor a#2 would escape its scope
# module Rectype :
sig type (_, _) t = C : ('a, 'a) t val f : ('s, 's * 's) t > unit end
# Characters 178186:
+# Characters 180188:
 (IntLit _  BoolLit _) > ()
^^^^^^^^
Error: This pattern matches values of type int t
@@ 265,7 +302,7 @@
 TA, D z > z
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
(TE TC, D [ ])
+(TE TC, D [ 0. ])
val f : 'a ty > 'a t > int = <fun>
# Characters 147154:
 D [1.0], TE TC > 14
@@ 287,7 +324,7 @@
 {left=TA; right=D z} > z
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
{left=TE TC; right=D [ ]}
+{left=TE TC; right=D [ 0. ]}
type ('a, 'b) pair = { left : 'a; right : 'b; }
val f : 'a ty > 'a t > int = <fun>
# module M : sig type 'a t val eq : ('a t, 'b t) eq end
@@ 309,14 +346,14 @@
^
Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < foo : int >
 Type ex#17 = < bar : int; .. > is not compatible with type < >
+ Type ex#25 = < bar : int; .. > is not compatible with type < >
The second object type has no method bar
# Characters 9899:
(x:<foo:int;bar:int>)
^
Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < bar : int; foo : int >
 Type ex#19 = < bar : int; .. > is not compatible with type
+ Type ex#27 = < bar : int; .. > is not compatible with type
< bar : int >
The first object type has an abstract row, it cannot be closed
# Characters 9899:
@@ 324,7 +361,7 @@
^
Error: This expression has type < bar : int; foo : int; .. >
but an expression was expected of type 'a
 The type constructor ex#22 would escape its scope
+ The type constructor ex#30 would escape its scope
# val g : 'a > 'a int_foo > 'a int_bar > 'a = <fun>
# val g : 'a > 'a int_foo > 'a int_bar > 'a * int * int = <fun>
# type 'a ty = Int : int > int ty
Index: testsuite/tests/typinggadts/test.ml.reference
===================================================================
 testsuite/tests/typinggadts/test.ml.reference (revision 16123)
+++ testsuite/tests/typinggadts/test.ml.reference (working copy)
@@ 65,6 +65,43 @@
type _ opt = Just : 'a > 'a opt  Nothing : 'a opt
class d : int opt > object method x : int end
end
+# module Exhaustive2 :
+ sig type _ t = Int : int t val f : bool t option > unit end
+# module PR6220 :
+ sig
+ type 'a t = I : int t  F : float t
+ val f : int t > int
+ val g : int t > int
+ end
+# module PR6403 :
+ sig
+ type (_, _) eq = Refl : ('a, 'a) eq
+ type empty = { bottom : 'a. 'a; }
+ type ('a, 'b) sum = Left of 'a  Right of 'b
+ val notequal : ((int, bool) eq, empty) sum > empty
+ end
+# module PR6437 :
+ sig
+ type ('a, 'b) ctx =
+ Nil : (unit, unit) ctx
+  Cons : ('a, 'b) ctx > ('a * unit, 'b * unit) ctx
+ type 'a var = O : ('a * unit) var  S : 'a var > ('a * unit) var
+ val f : ('g1, 'g2) ctx * 'g1 var > 'g2 var
+ end
+# Characters 175221:
+ ....match x with
+  String s > print_endline s.................
+Warning 8: this patternmatching is not exhaustive.
+Here is an example of a value that is not matched:
+Any
+module PR6801 :
+ sig
+ type _ value =
+ String : string > string value
+  Float : float > float value
+  Any
+ val print_string_value : string value > unit
+ end
# Characters 118119:
let eval (D x) = x
^
@@ 73,7 +110,7 @@
The type constructor a#2 would escape its scope
# module Rectype :
sig type (_, _) t = C : ('a, 'a) t val f : ('s, 's * 's) t > unit end
# Characters 178186:
+# Characters 180188:
 (IntLit _  BoolLit _) > ()
^^^^^^^^
Error: This pattern matches values of type int t
@@ 252,7 +289,7 @@
 TA, D z > z
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
(TE TC, D [ ])
+(TE TC, D [ 0. ])
val f : 'a ty > 'a t > int = <fun>
# Characters 147154:
 D [1.0], TE TC > 14
@@ 274,7 +311,7 @@
 {left=TA; right=D z} > z
Warning 8: this patternmatching is not exhaustive.
Here is an example of a value that is not matched:
{left=TE TC; right=D [ ]}
+{left=TE TC; right=D [ 0. ]}
type ('a, 'b) pair = { left : 'a; right : 'b; }
val f : 'a ty > 'a t > int = <fun>
# module M : sig type 'a t val eq : ('a t, 'b t) eq end
@@ 296,14 +333,14 @@
^
Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < foo : int >
 Type ex#17 = < bar : int; .. > is not compatible with type < >
+ Type ex#25 = < bar : int; .. > is not compatible with type < >
The second object type has no method bar
# Characters 9899:
(x:<foo:int;bar:int>)
^
Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < bar : int; foo : int >
 Type ex#19 = < bar : int; .. > is not compatible with type
+ Type ex#27 = < bar : int; .. > is not compatible with type
< bar : int >
The first object type has an abstract row, it cannot be closed
# Characters 9899:
@@ 311,7 +348,7 @@
^
Error: This expression has type < bar : int; foo : int; .. >
but an expression was expected of type 'a
 The type constructor ex#22 would escape its scope
+ The type constructor ex#30 would escape its scope
# val g : 'a > 'a int_foo > 'a int_bar > 'a = <fun>
# val g : 'a > 'a int_foo > 'a int_bar > 'a * int * int = <fun>
# type 'a ty = Int : int > int ty
Index: typing/ctype.ml
===================================================================
 typing/ctype.ml (revision 16123)
+++ typing/ctype.ml (working copy)
@@ 116,6 +116,20 @@
let global_level = ref 1
let saved_level = ref []
+type levels =
+ { current_level: int; nongen_level: int; global_level: int;
+ saved_level: (int * int) list; }
+let save_levels () =
+ { current_level = !current_level;
+ nongen_level = !nongen_level;
+ global_level = !global_level;
+ saved_level = !saved_level }
+let set_levels l =
+ current_level := l.current_level;
+ nongen_level := l.nongen_level;
+ global_level := l.global_level;
+ saved_level := l.saved_level
+
let get_current_level () = !current_level
let init_def level = current_level := level; nongen_level := level
let begin_def () =
Index: typing/ctype.mli
===================================================================
 typing/ctype.mli (revision 16123)
+++ typing/ctype.mli (working copy)
@@ 37,6 +37,11 @@
val increase_global_level: unit > int
val restore_global_level: int > unit
(* This pair of functions is only used in Typetexp *)
+type levels =
+ { current_level: int; nongen_level: int; global_level: int;
+ saved_level: (int * int) list; }
+val save_levels: unit > levels
+val set_levels: levels > unit
val newty: type_desc > type_expr
val newvar: ?name:string > unit > type_expr
Index: typing/parmatch.ml
===================================================================
 typing/parmatch.ml (revision 16123)
+++ typing/parmatch.ml (working copy)
@@ 621,18 +621,10 @@
in
loop env
let full_match ignore_generalized closing env = match env with
+let full_match closing env = match env with
 ({pat_desc = Tpat_construct(_,c,_);pat_type=typ},_) :: _ >
if c.cstr_consts < 0 then false (* extensions *)
 else
 if ignore_generalized then
 (* remove generalized constructors;
 those cases will be handled separately *)
 let env = clean_env env in
 List.length env = c.cstr_normal
 else
 List.length env = c.cstr_consts + c.cstr_nonconsts

+ else List.length env = c.cstr_consts + c.cstr_nonconsts
 ({pat_desc = Tpat_variant _} as p,_) :: _ >
let fields =
List.map
@@ 666,11 +658,6 @@
 ({pat_desc = Tpat_lazy(_)},_) :: _ > true
 _ > fatal_error "Parmatch.full_match"
let full_match_gadt env = match env with
  ({pat_desc = Tpat_construct(_,c,_);pat_type=typ},_) :: _ >
 List.length env = c.cstr_consts + c.cstr_nonconsts
  _ > true

let extendable_match env = match env with
 ({pat_desc=Tpat_construct(_,{cstr_tag=(Cstr_constant _Cstr_block _)},_)}
as p,_) :: _ >
@@ 715,20 +702,35 @@
(* build a pattern from a constructor list *)
let pat_of_constr ex_pat cstr =
 {ex_pat with pat_desc =
 Tpat_construct (mknoloc (Longident.Lident "?pat_of_constr?"),
 cstr,omegas cstr.cstr_arity)}
+ {ex_pat with pat_desc =
+ Tpat_construct (mknoloc (Longident.Lident "?pat_of_constr?"),
+ cstr, omegas cstr.cstr_arity)}
let rec pat_of_constrs ex_pat = function
 [] > raise Empty
 [cstr] > pat_of_constr ex_pat cstr
 cstr::rem >
 {ex_pat with
 pat_desc=
 Tpat_or
 (pat_of_constr ex_pat cstr,
 pat_of_constrs ex_pat rem, None)}
+let rec orify_many = function
+ [] > assert false
+ [x] > x
+ x :: xs >
+ make_pat (Tpat_or (x, orify_many xs, None)) x.pat_type x.pat_env
+let pat_of_constrs ex_pat cstrs =
+ if cstrs = [] then raise Empty else
+ orify_many (List.map (pat_of_constr ex_pat) cstrs)
+
+let pats_of_type env ty =
+ let ty' = Ctype.expand_head env ty in
+ match ty'.desc with
+  Tconstr (path, _, _) >
+ begin match Env.find_type path env with
+  {type_kind = Type_variant cl}
+ when List.for_all (fun cd > cd.Types.cd_res <> None) cl >
+ let cstrs = fst (Env.find_type_descrs path env) in
+ List.map
+ (pat_of_constr {omega with pat_type=ty; pat_env=env})
+ cstrs
+  _ > [omega]
+ end
+  _ > [omega]
+
let rec get_variant_constructors env ty =
match (Ctype.repr ty).desc with
 Tconstr (path,_,_) > begin
@@ 756,11 +758,12 @@
 Tpat_construct (_,c,_) >
let not_tags = complete_tags c.cstr_consts c.cstr_nonconsts all_tags in
let constrs = get_variant_constructors p.pat_env c.cstr_res in
 map_filter
 (fun cnstr >
 if List.mem cnstr.cstr_tag not_tags then Some cnstr else None)
 constrs
  _ > fatal_error "Parmatch.complete_constr"
+ let others =
+ List.filter (fun cnstr > List.mem cnstr.cstr_tag not_tags) constrs in
+ let const, nonconst =
+ List.partition (fun cnstr > cnstr.cstr_arity = 0) others in
+ const @ nonconst
+  _ > fatal_error "Parmatch.complete_constrs"
(* Auxiliary for build_other *)
@@ 778,7 +781,7 @@
in the first column of env
*)
let build_other ext env = match env with
+let build_other ext env = match env with
 ({pat_desc = Tpat_construct (lid,
({cstr_tag=Cstr_extension _} as c),_)},_) :: _ >
let c = {c with cstr_name = "*extension*"} in
@@ 902,20 +905,6 @@
 [] > omega
 _ > omega
let build_other_gadt ext env =
 match env with
  ({pat_desc = Tpat_construct _} as p,_) :: _ >
 let get_tag = function
  {pat_desc = Tpat_construct (_,c,_)} > c.cstr_tag
  _ > fatal_error "Parmatch.get_tag" in
 let all_tags = List.map (fun (p,_) > get_tag p) env in
 let cnstrs = complete_constrs p all_tags in
 let pats = List.map (pat_of_constr p) cnstrs in
 (* List.iter (Format.eprintf "%a@." top_pretty) pats;
 Format.eprintf "@.@."; *)
 pats
  _ > assert false

(*
Core function :
Is the last row of pattern matrix pss + qs satisfiable ?
@@ 956,7 +945,7 @@
(* first column of pss is made of variables only *)
 [] > satisfiable (filter_extra pss) qs
 constrs >
 if full_match false false constrs then
+ if full_match false constrs then
List.exists
(fun (p,pss) >
not (is_absent_pat p) &&
@@ 981,15 +970,6 @@
 Rnone (* No matching value *)
 Rsome of 'a (* This matching value *)
let rec orify_many =
 let orify x y =
 make_pat (Tpat_or (x, y, None)) x.pat_type x.pat_env
 in
 function
  [] > assert false
  [x] > x
  x :: xs > orify x (orify_many xs)

let rec try_many f = function
 [] > Rnone
 (p,pss)::rest >
@@ 1008,6 +988,7 @@
 (p,pss)::rest >
rappend (f (p, pss)) (try_many_gadt f rest)
+(*
let rec exhaust ext pss n = match pss with
 [] > Rsome (omegas n)
 []::_ > Rnone
@@ 1068,7 +1049,7 @@
 x :: xs > iter2 x lst' @ iter xs
in
iter lst

+*)
(*
let print_pat pat =
let rec string_of_pat pat =
@@ 1119,7 +1100,7 @@
 r > r in
let before = try_many_gadt try_non_omega constrs in
if
 full_match_gadt constrs && not (should_extend ext constrs)
+ full_match false constrs && not (should_extend ext constrs)
then
before
else
@@ 1136,13 +1117,8 @@
 Rnone > before
 Rsome r >
try
 let missing_trailing = build_other_gadt ext constrs in
 let dug =
 combinations
 (fun head tail > head :: tail)
 missing_trailing
 r
 in
+ let p = build_other ext constrs in
+ let dug = List.map (fun tail > p :: tail) r in
match before with
 Rnone > Rsome dug
 Rsome x > Rsome (x @ dug)
@@ 1193,12 +1169,12 @@
try_non_omega rem && ok
 [] > true
in
 if full_match true (tdefs=None) constrs then
+ if full_match (tdefs=None) constrs then
try_non_omega constrs
else if tdefs = None then
pressure_variants None (filter_extra pss)
else
 let full = full_match true true constrs in
+ let full = full_match true constrs in
let ok =
if full then try_non_omega constrs
else try_non_omega (filter_all q0 (mark_partial pss))
@@ 1662,119 +1638,71 @@
(* Exhaustiveness check *)
(************************)

 let rec get_first f =
 function
  [] > None
  x :: xs >
 match f x with
  None > get_first f xs
  x > x


(* conversion from Typedtree.pattern to Parsetree.pattern list *)
module Conv = struct
open Parsetree
let mkpat desc = Ast_helper.Pat.mk desc
 let rec select : 'a list list > 'a list list =
 function
  xs :: [] > List.map (fun y > [y]) xs
  (x::xs)::ys >
 List.map
 (fun lst > x :: lst)
 (select ys)
 @
 select (xs::ys)
  _ > []

let name_counter = ref 0
let fresh name =
let current = !name_counter in
name_counter := !name_counter + 1;
"#$" ^ name ^ string_of_int current
 let conv (typed: Typedtree.pattern) :
 Parsetree.pattern list *
 (string, Types.constructor_description) Hashtbl.t *
 (string, Types.label_description) Hashtbl.t
 =
 let constrs = Hashtbl.create 0 in
 let labels = Hashtbl.create 0 in
+ let conv typed =
+ let constrs = Hashtbl.create 7 in
+ let labels = Hashtbl.create 7 in
let rec loop pat =
match pat.pat_desc with
 Tpat_or (a,b,_) >
 loop a @ loop b
  Tpat_any  Tpat_constant _  Tpat_var _ >
 [mkpat Ppat_any]
+ Tpat_or (pa,pb,_) >
+ mkpat (Ppat_or (loop pa, loop pb))
+  Tpat_any
+  Tpat_var _ >
+ mkpat Ppat_any
+  Tpat_constant c >
+ mkpat (Ppat_constant c)
 Tpat_alias (p,_,_) > loop p
 Tpat_tuple lst >
 let results = select (List.map loop lst) in
 List.map
 (fun lst > mkpat (Ppat_tuple lst))
 results
  Tpat_construct (cstr_lid, cstr,lst) >
+ mkpat (Ppat_tuple (List.map loop lst))
+  Tpat_construct (cstr_lid, cstr, lst) >
let id = fresh cstr.cstr_name in
let lid = { cstr_lid with txt = Longident.Lident id } in
Hashtbl.add constrs id cstr;
 let results = select (List.map loop lst) in
 begin match lst with
 [] >
 [mkpat (Ppat_construct(lid, None))]
  _ >
 List.map
 (fun lst >
 let arg =
 match lst with
 [] > assert false
  [x] > Some x
  _ > Some (mkpat (Ppat_tuple lst))
 in
 mkpat (Ppat_construct(lid, arg)))
 results
 end
+ let arg =
+ match List.map loop lst with
+  [] > None
+  [p] > Some p
+  lst > Some (mkpat (Ppat_tuple lst))
+ in
+ mkpat (Ppat_construct(lid, arg))
 Tpat_variant(label,p_opt,row_desc) >
 begin match p_opt with
  None >
 [mkpat (Ppat_variant(label, None))]
  Some p >
 let results = loop p in
 List.map
 (fun p >
 mkpat (Ppat_variant(label, Some p)))
 results
 end
+ let arg = Misc.may_map loop p_opt in
+ mkpat (Ppat_variant(label, arg))
 Tpat_record (subpatterns, _closed_flag) >
 let pats =
 select
 (List.map (fun (_,_,x) > loop x) subpatterns)
 in
 let label_idents =
 List.map
 (fun (_,lbl,_) >
+ let fields =
+ List.map
+ (fun (_, lbl, p) >
let id = fresh lbl.lbl_name in
Hashtbl.add labels id lbl;
 Longident.Lident id)
 subpatterns
 in
 List.map
 (fun lst >
 let lst = List.map2 (fun lid pat >
 (mknoloc lid, pat)
 ) label_idents lst in
 mkpat (Ppat_record (lst, Open)))
 pats
+ (mknoloc (Longident.Lident id), loop p))
+ subpatterns
+ in
+ mkpat (Ppat_record (fields, Open))
 Tpat_array lst >
 let results = select (List.map loop lst) in
 List.map (fun lst > mkpat (Ppat_array lst)) results
+ mkpat (Ppat_array (List.map loop lst))
 Tpat_lazy p >
 let results = loop p in
 List.map (fun p > mkpat (Ppat_lazy p)) results
+ mkpat (Ppat_lazy (loop p))
in
let ps = loop typed in
(ps, constrs, labels)
end
+let ppat_of_type env ty =
+ match pats_of_type env ty with
+ [{pat_desc = Tpat_any}] >
+ (Conv.mkpat Parsetree.Ppat_any, Hashtbl.create 0, Hashtbl.create 0)
+  pats >
+ Conv.conv (orify_many pats)
let do_check_partial ?pred exhaust loc casel pss = match pss with
 [] >
@@ 1798,12 +1726,12 @@
let v =
match pred with
 Some pred >
 let (patterns,constrs,labels) = Conv.conv u in
+ let (pattern,constrs,labels) = Conv.conv u in
(* Hashtbl.iter (fun s (path, _) >
Printf.fprintf stderr "CONV: %s > %s \n%!" s (Path.name path))
constrs
; *)
 get_first (pred constrs labels) patterns
+ pred constrs labels pattern
 None > Some u
in
begin match v with
@@ 1839,8 +1767,10 @@
fatal_error "Parmatch.check_partial"
end
+(*
let do_check_partial_normal loc casel pss =
do_check_partial exhaust loc casel pss
+ *)
let do_check_partial_gadt pred loc casel pss =
do_check_partial ~pred exhaust_gadt loc casel pss
@@ 1916,7 +1846,7 @@
 Rsome _ > ())
exts
let do_check_fragile_normal = do_check_fragile_param exhaust
+(*let do_check_fragile_normal = do_check_fragile_param exhaust*)
let do_check_fragile_gadt = do_check_fragile_param exhaust_gadt
(********************************)
@@ 2012,19 +1942,11 @@
end else
Partial
let check_partial =
+(*let check_partial =
check_partial_param
do_check_partial_normal
 do_check_fragile_normal
+ do_check_fragile_normal*)
let check_partial_gadt pred loc casel =
 (*ignores GADT constructors *)
 let first_check = check_partial loc casel in
 match first_check with
  Partial > Partial
  Total >
 (* checks for missing GADT constructors *)
 (* let casel =
 match casel with [] > []  a :: l > a :: l @ [a] in *)
 check_partial_param (do_check_partial_gadt pred)
 do_check_fragile_gadt loc casel
+ check_partial_param (do_check_partial_gadt pred)
+ do_check_fragile_gadt loc casel
Index: typing/parmatch.mli
===================================================================
 typing/parmatch.mli (revision 16123)
+++ typing/parmatch.mli (working copy)
@@ 51,6 +51,11 @@
val pat_of_constr : pattern > constructor_description > pattern
val complete_constrs :
pattern > constructor_tag list > constructor_description list
+val ppat_of_type :
+ Env.t > type_expr >
+ Parsetree.pattern *
+ (string, constructor_description) Hashtbl.t *
+ (string, label_description) Hashtbl.t
val pressure_variants: Env.t > pattern list > unit
val check_partial_gadt:
Index: typing/typecore.ml
===================================================================
 typing/typecore.ml (revision 16123)
+++ typing/typecore.ml (working copy)
@@ 827,7 +827,11 @@
 ({ txt = Longident.Ldot (modname, _) }, _) :: _ > Some modname
 _ :: rest > find_record_qual rest
let type_label_a_list ?labels loc closed env type_lbl_a opath lid_a_list =
+let map_fold_cont f xs k =
+ List.fold_right (fun x k ys > f x (fun y > k (y :: ys)))
+ xs (fun ys > k (List.rev ys)) []
+
+let type_label_a_list ?labels loc closed env type_lbl_a opath lid_a_list k =
let lbl_a_list =
match lid_a_list, labels with
({txt=Longident.Lident s}, _)::_, Some labels when Hashtbl.mem labels s >
@@ 857,7 +861,7 @@
(fun (_,lbl1,_) (_,lbl2,_) > compare lbl1.lbl_pos lbl2.lbl_pos)
lbl_a_list
in
 List.map type_lbl_a lbl_a_list
+ map_fold_cont type_lbl_a lbl_a_list k
;;
(* Checks over the labels mentioned in a record pattern:
@@ 917,32 +921,59 @@
 Normal
 Inside_or
+(* Remember current state for backtracking.
+ No variable information, as we only backtrack on
+ patterns without variables (cf. assert statements). *)
+type state =
+ { snapshot: Btype.snapshot;
+ levels: Ctype.levels;
+ env: Env.t; }
+let save_state env =
+ { snapshot = Btype.snapshot ();
+ levels = Ctype.save_levels ();
+ env = !env; }
+let set_state s env =
+ Btype.backtrack s.snapshot;
+ Ctype.set_levels s.levels;
+ env := s.env
+
(* type_pat propagates the expected type as well as maps for
constructors and labels.
Unification may update the typing environment. *)
let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
 let type_pat ?(mode=mode) ?(env=env) =
+(* constrs <> None => called from parmatch: backtrack on orpatterns
+ labels <> None => explode Ppat_any for gadts *)
+let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty k =
+ let type_pat ?(constrs=constrs) ?(labels=labels) ?(mode=mode) ?(env=env) =
type_pat ~constrs ~labels ~no_existentials ~mode ~env in
let loc = sp.ppat_loc in
+ let rp k x : pattern = if constrs = None then k (rp x) else k x in
match sp.ppat_desc with
Ppat_any >
 rp {
 pat_desc = Tpat_any;
+ let k' d = rp k {
+ pat_desc = d;
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
pat_env = !env }
+ in
+ if labels <> None then
+ let (sp, constrs, labels) = Parmatch.ppat_of_type !env expected_ty in
+ if sp.ppat_desc = Parsetree.Ppat_any then k' Tpat_any
+ else type_pat ~constrs:(Some constrs) ~labels:None sp expected_ty k
+ else k' Tpat_any
 Ppat_var name >
+ assert (constrs = None);
let id = enter_variable loc name expected_ty in
 rp {
+ rp k {
pat_desc = Tpat_var (id, name);
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
pat_env = !env }
 Ppat_unpack name >
+ assert (constrs = None);
let id = enter_variable loc name expected_ty ~is_module:true in
 rp {
+ rp k {
pat_desc = Tpat_var (id, name);
pat_loc = sp.ppat_loc;
pat_extra=[Tpat_unpack, loc, sp.ppat_attributes];
@@ 952,6 +983,7 @@
 Ppat_constraint({ppat_desc=Ppat_var name; ppat_loc=lloc},
({ptyp_desc=Ptyp_poly _} as sty)) >
(* explicitly polymorphic type *)
+ assert (constrs = None);
let cty, force = Typetexp.transl_simple_type_delayed !env sty in
let ty = cty.ctyp_type in
unify_pat_types lloc !env ty expected_ty;
@@ 963,7 +995,7 @@
end_def ();
generalize ty';
let id = enter_variable lloc name ty' in
 rp {
+ rp k {
pat_desc = Tpat_var (id, name);
pat_loc = lloc;
pat_extra = [Tpat_constraint cty, loc, sp.ppat_attributes];
@@ 974,21 +1006,22 @@
 _ > assert false
end
 Ppat_alias(sq, name) >
 let q = type_pat sq expected_ty in
 begin_def ();
 let ty_var = build_as_type !env q in
 end_def ();
 generalize ty_var;
 let id = enter_variable ~is_as_variable:true loc name ty_var in
 rp {
 pat_desc = Tpat_alias(q, id, name);
 pat_loc = loc; pat_extra=[];
 pat_type = q.pat_type;
 pat_attributes = sp.ppat_attributes;
 pat_env = !env }
+ assert (constrs = None);
+ type_pat sq expected_ty (fun q >
+ begin_def ();
+ let ty_var = build_as_type !env q in
+ end_def ();
+ generalize ty_var;
+ let id = enter_variable ~is_as_variable:true loc name ty_var in
+ rp k {
+ pat_desc = Tpat_alias(q, id, name);
+ pat_loc = loc; pat_extra=[];
+ pat_type = q.pat_type;
+ pat_attributes = sp.ppat_attributes;
+ pat_env = !env })
 Ppat_constant cst >
unify_pat_types loc !env (type_constant cst) expected_ty;
 rp {
+ rp k {
pat_desc = Tpat_constant cst;
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
@@ 1006,7 +1039,7 @@
in
let p = if c1 <= c2 then loop c1 c2 else loop c2 c1 in
let p = {p with ppat_loc=loc} in
 type_pat p expected_ty
+ type_pat ~labels:None p expected_ty k
(* TODO: record 'extra' to remember about interval *)
 Ppat_interval _ >
raise (Error (loc, !env, Invalid_interval))
@@ 1016,13 +1049,13 @@
let spl_ann = List.map (fun p > (p,newvar ())) spl in
let ty = newty (Ttuple(List.map snd spl_ann)) in
unify_pat_types loc !env ty expected_ty;
 let pl = List.map (fun (p,t) > type_pat p t) spl_ann in
 rp {
+ map_fold_cont (fun (p,t) > type_pat p t) spl_ann (fun pl >
+ rp k {
pat_desc = Tpat_tuple pl;
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
 pat_env = !env }
+ pat_env = !env })
 Ppat_construct(lid, sarg) >
let opath =
try
@@ 1090,13 +1123,14 @@
in
if constr.cstr_inlined <> None then List.iter check_non_escaping sargs;
 let args = List.map2 (fun p t > type_pat p t) sargs ty_args in
 rp {
 pat_desc=Tpat_construct(lid, constr, args);
 pat_loc = loc; pat_extra=[];
 pat_type = expected_ty;
 pat_attributes = sp.ppat_attributes;
 pat_env = !env }
+ map_fold_cont (fun (p,t) > type_pat p t) (List.combine sargs ty_args)
+ (fun args >
+ rp k {
+ pat_desc=Tpat_construct(lid, constr, args);
+ pat_loc = loc; pat_extra=[];
+ pat_type = expected_ty;
+ pat_attributes = sp.ppat_attributes;
+ pat_env = !env })
 Ppat_variant(l, sarg) >
let arg_type = match sarg with None > []  Some _ > [newvar()] in
let row = { row_fields =
@@ 1107,18 +1141,19 @@
row_fixed = false;
row_name = None } in
unify_pat_types loc !env (newty (Tvariant row)) expected_ty;
 let arg =
 (* PR#6235: propagate type information *)
 match sarg, arg_type with
 Some p, [ty] > Some (type_pat p ty)
  _ > None
 in
 rp {
+ let k arg =
+ rp k {
pat_desc = Tpat_variant(l, arg, ref {row with row_more = newvar()});
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
pat_env = !env }
+ in begin
+ (* PR#6235: propagate type information *)
+ match sarg, arg_type with
+ Some p, [ty] > type_pat p ty (fun p > k (Some p))
+  _ > k None
+ end
 Ppat_record(lid_sp_list, closed) >
if lid_sp_list = [] then
Syntaxerr.ill_formed_ast loc "Records cannot be empty.";
@@ 1128,7 +1163,7 @@
Some (p0, p, true), expected_ty
with Not_found > None, newvar ()
in
 let type_label_pat (label_lid, label, sarg) =
+ let type_label_pat (label_lid, label, sarg) k =
begin_def ();
let (vars, ty_arg, ty_res) = instance_label false label in
if vars = [] then end_def ();
@@ 1138,55 +1173,72 @@
raise(Error(label_lid.loc, !env,
Label_mismatch(label_lid.txt, trace)))
end;
 let arg = type_pat sarg ty_arg in
 if vars <> [] then begin
 end_def ();
 generalize ty_arg;
 List.iter generalize vars;
 let instantiated tv =
 let tv = expand_head !env tv in
 not (is_Tvar tv)  tv.level <> generic_level in
 if List.exists instantiated vars then
 raise (Error(label_lid.loc, !env, Polymorphic_label label_lid.txt))
 end;
 (label_lid, label, arg)
+ type_pat sarg ty_arg (fun arg >
+ if vars <> [] then begin
+ end_def ();
+ generalize ty_arg;
+ List.iter generalize vars;
+ let instantiated tv =
+ let tv = expand_head !env tv in
+ not (is_Tvar tv)  tv.level <> generic_level in
+ if List.exists instantiated vars then
+ raise
+ (Error(label_lid.loc, !env, Polymorphic_label label_lid.txt))
+ end;
+ k (label_lid, label, arg))
in
 let lbl_pat_list =
 wrap_disambiguate "This record pattern is expected to have" expected_ty
 (type_label_a_list ?labels loc false !env type_label_pat opath)
 lid_sp_list
 in
 check_recordpat_labels loc lbl_pat_list closed;
 unify_pat_types loc !env record_ty expected_ty;
 rp {
+ let k' k lbl_pat_list =
+ check_recordpat_labels loc lbl_pat_list closed;
+ unify_pat_types loc !env record_ty expected_ty;
+ rp k {
pat_desc = Tpat_record (lbl_pat_list, closed);
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
pat_env = !env }
+ in
+ if constrs = None then
+ k (wrap_disambiguate "This record pattern is expected to have"
+ expected_ty
+ (type_label_a_list ?labels loc false !env type_label_pat opath
+ lid_sp_list)
+ (k' (fun x > x)))
+ else
+ type_label_a_list ?labels loc false !env type_label_pat opath
+ lid_sp_list (k' k)
 Ppat_array spl >
let ty_elt = newvar() in
unify_pat_types
loc !env (instance_def (Predef.type_array ty_elt)) expected_ty;
let spl_ann = List.map (fun p > (p,newvar())) spl in
 let pl = List.map (fun (p,t) > type_pat p ty_elt) spl_ann in
 rp {
+ map_fold_cont (fun (p,t) > type_pat p ty_elt) spl_ann (fun pl >
+ rp k {
pat_desc = Tpat_array pl;
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
 pat_env = !env }
+ pat_env = !env })
 Ppat_or(sp1, sp2) >
+ if constrs <> None &&
+ match sp1.ppat_desc, sp2.ppat_desc with
+ Ppat_constant _, _  _, Ppat_constant _ > false
+  _ > true
+ then
+ let state = save_state env in
+ try type_pat sp1 expected_ty k with exn when exn <> Exit >
+ set_state state env;
+ type_pat sp2 expected_ty k
+ else
let initial_pattern_variables = !pattern_variables in
 let p1 = type_pat ~mode:Inside_or sp1 expected_ty in
+ let p1 = type_pat ~mode:Inside_or sp1 expected_ty (fun x > x) in
let p1_variables = !pattern_variables in
pattern_variables := initial_pattern_variables;
 let p2 = type_pat ~mode:Inside_or sp2 expected_ty in
+ let p2 = type_pat ~mode:Inside_or sp2 expected_ty (fun x > x) in
let p2_variables = !pattern_variables in
let alpha_env =
enter_orpat_variables loc !env p1_variables p2_variables in
pattern_variables := p1_variables;
 rp {
+ rp k {
pat_desc = Tpat_or(p1, alpha_pat alpha_env p2, None);
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
@@ 1196,13 +1248,13 @@
let nv = newvar () in
unify_pat_types loc !env (instance_def (Predef.type_lazy_t nv))
expected_ty;
 let p1 = type_pat sp1 nv in
 rp {
+ type_pat sp1 nv (fun p1 >
+ rp k {
pat_desc = Tpat_lazy p1;
pat_loc = loc; pat_extra=[];
pat_type = expected_ty;
pat_attributes = sp.ppat_attributes;
 pat_env = !env }
+ pat_env = !env })
 Ppat_constraint(sp, sty) >
(* Separate when not already separated by !principal *)
let separate = true in
@@ 1217,27 +1269,28 @@
end else ty, ty
in
unify_pat_types loc !env ty expected_ty;
 let p = type_pat sp expected_ty' in
 (*Format.printf "%a@.%a@."
 Printtyp.raw_type_expr ty
 Printtyp.raw_type_expr p.pat_type;*)
 pattern_force := force :: !pattern_force;
 let extra = (Tpat_constraint cty, loc, sp.ppat_attributes) in
 if separate then
 match p.pat_desc with
 Tpat_var (id,s) >
 {p with pat_type = ty;
 pat_desc = Tpat_alias
 ({p with pat_desc = Tpat_any; pat_attributes = []}, id,s);
 pat_extra = [extra];
 }
  _ > {p with pat_type = ty;
 pat_extra = extra :: p.pat_extra}
 else p
+ type_pat sp expected_ty' (fun p >
+ (*Format.printf "%a@.%a@."
+ Printtyp.raw_type_expr ty
+ Printtyp.raw_type_expr p.pat_type;*)
+ pattern_force := force :: !pattern_force;
+ let extra = (Tpat_constraint cty, loc, sp.ppat_attributes) in
+ let p =
+ if not separate then p else
+ match p.pat_desc with
+ Tpat_var (id,s) >
+ {p with pat_type = ty;
+ pat_desc = Tpat_alias
+ ({p with pat_desc = Tpat_any; pat_attributes = []}, id,s);
+ pat_extra = [extra];
+ }
+  _ > {p with pat_type = ty;
+ pat_extra = extra :: p.pat_extra}
+ in k p)
 Ppat_type lid >
let (path, p,ty) = build_or_pat !env loc lid.txt in
unify_pat_types loc !env ty expected_ty;
 { p with pat_extra =
+ k { p with pat_extra =
(Tpat_type (path, lid), loc, sp.ppat_attributes) :: p.pat_extra }
 Ppat_exception _ >
raise (Error (loc, !env, Exception_pattern_below_toplevel))
@@ 1250,7 +1303,7 @@
try
let r =
type_pat ~no_existentials:(not allow_existentials) ~constrs ~labels
 ~mode:Normal ~env sp expected_ty in
+ ~mode:Normal ~env sp expected_ty (fun x > x) in
iter_pattern (fun p > p.pat_env < !env) r;
newtype_level := None;
r
@@ 2089,9 +2142,9 @@
let lbl_exp_list =
wrap_disambiguate "This record expression is expected to have" ty_record
(type_label_a_list loc closed env
 (type_label_exp true env loc ty_record)
 opath)
 lid_sexp_list
+ (fun e k > k (type_label_exp true env loc ty_record e))
+ opath lid_sexp_list)
+ (fun x > x)
in
unify_exp_types loc env ty_record (instance env ty_expected);
