fix problem with constraints outside of matching, see typing-gadts/test.ml

git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@11068 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

testsuite/tests/typing-gadts/omega07.ml

@@ -143,7 +143,7 @@ let rec sameNat : type a b. a nat -> b nat -> (a,b) equal option = fun a b ->
   | NZ, NZ -> Some Eq
   | NS a', NS b' ->
       begin match sameNat a' b' with
-      | Some Eq -> Some (Eq : (a, b) equal)
+      | Some Eq -> Some Eq
       | None -> None
       end
   | _ -> None

testsuite/tests/typing-gadts/test.ml

@@ -204,3 +204,29 @@ let test2 : type a. a t -> a option = fun x ->
     !u
   in a
 ;; (* fail *)
+
+(* Effect of external consraints *)
+
+let f (type a) (x : a t) y =
+  ignore (y : a);
+  let r = match x with Int -> (y : a) in (* fails *)
+  r
+;;
+let f (type a) (x : a t) y =
+  let r = match x with Int -> (y : a) in
+  ignore (y : a); (* fails *)
+  r
+;;
+let f (type a) (x : a t) y =
+  ignore (y : a);
+  let r = match x with Int -> y in
+  r
+;;
+let f (type a) (x : a t) y =
+  let r = match x with Int -> y in
+  ignore (y : a);
+  r
+;;
+let f (type a) (x : a t) (y : a) =
+  match x with Int -> y
+;;

typing/ctype.ml

@@ -1253,7 +1253,7 @@ let expand_abbrev_gen kind find_type_expansion env ty =
           ty
       | None ->
           let (params, body) =
-            try find_type_expansion path env with Not_found ->
+            try find_type_expansion level path env with Not_found ->
               raise Cannot_expand
           in
           (* prerr_endline
@@ -1274,7 +1274,8 @@ let expand_abbrev_gen kind find_type_expansion env ty =
    use local constraints *)
 let expand_abbrev ty =
   let use_local = use_local () in
-  expand_abbrev_gen Public (Env.find_type_expansion ~use_local) ty
+  expand_abbrev_gen Public
+    (fun level -> Env.find_type_expansion ~use_local ~level) ty
 
 let safe_abbrev env ty =
   let snap = Btype.snapshot () in
@@ -1332,7 +1333,8 @@ let expand_head env ty =
    normally hidden to the type-checker out of the implementation module of
    the private abbreviation. *)
 
-let expand_abbrev_opt = expand_abbrev_gen Private Env.find_type_expansion_opt
+let expand_abbrev_opt =
+  expand_abbrev_gen Private (fun level -> Env.find_type_expansion_opt)
 
 let try_expand_once_opt env ty =
   let ty = repr ty in

typing/env.ml

@@ -280,9 +280,15 @@ and find_cltype =
 (* Find the manifest type associated to a type when appropriate:
    - the type should be public or should have a private row,
    - the type should have an associated manifest type. *)
-let find_type_expansion ?(use_local=true) path env =
+let find_type_expansion ?(use_local=true) ?level path env =
   let decl = find_type path env in
   if not use_local && not (decl.type_newtype_level = None) then raise Not_found;
+  (* the level is changed when updating newtype definitions *)
+  if !Clflags.principal then begin
+    match level, decl.type_newtype_level with
+      Some level, Some def_level when level < def_level -> raise Not_found
+    | _ -> ()
+  end;
   match decl.type_manifest with
   | Some body when decl.type_private = Public
               || decl.type_kind <> Type_abstract
@@ -770,7 +776,8 @@ and add_cltype id ty env =
 let add_local_constraint id info mlv env =
   match info with
     {type_manifest = Some ty; type_newtype_level = Some lv} ->
-      let env = add_type id info env in
+      (* use the newtype level for this definition, lv is the old one *)
+      let env = add_type id {info with type_newtype_level = Some mlv} env in
       let level_map =
         if lv < mlv then add_level lv mlv env.level_map else env.level_map in
       { env with local_constraints = true; level_map = level_map }

typing/env.mli

@@ -32,7 +32,7 @@ val find_modtype: Path.t -> t -> modtype_declaration
 val find_class: Path.t -> t -> class_declaration
 val find_cltype: Path.t -> t -> cltype_declaration
 
-val find_type_expansion: ?use_local:bool -> Path.t -> t -> type_expr list * type_expr
+val find_type_expansion: ?use_local:bool -> ?level:int -> Path.t -> t -> type_expr list * type_expr
 val find_type_expansion_opt: Path.t -> t -> type_expr list * type_expr
 (* Find the manifest type information associated to a type for the sake
    of the compiler's type-based optimisations. *)