fix principality by expanding local definitions when exporting a value

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

testsuite/tests/typing-gadts/test.ml

@@ -131,8 +131,7 @@ module Polymorphic_variants =
   end    
 ;;
 
-module Propagation = 
-  struct
+module Propagation = struct
   type _ t = 
       IntLit : int -> int t
     | BoolLit : bool -> bool t
@@ -140,12 +139,38 @@ module Propagation =
   let check : type s. s t -> s = function
     | IntLit n -> n
     | BoolLit b -> b
-;;
+
   let check : type s. s t -> s = fun x ->
     let r = match x with
     | IntLit n -> (n : s )
     | BoolLit b -> b
     in r
-;;
 end
 ;;
+
+type _ t = Int : int t ;;
+
+let ky x y = ignore (x = y); x ;;
+
+let test : type a. a t -> a = fun x ->
+  let r = match x with Int -> ky (1 : a) 1
+  in r
+;;
+let test : type a. a t -> a = fun x ->
+  let r = match x with Int -> ky 1 (1 : a)
+  in r
+;;
+let test : type a. a t -> a = fun x ->
+  let r = match x with Int -> (1 : a)
+  in r (* fails too *)
+;;
+let test2 : type a. a t -> a option = fun x ->
+  let r = ref None in
+  begin match x with Int -> r := Some (1 : a) end;
+  !r (* normalized to int option *)
+;;
+let test2 : type a. a t -> a option = fun x ->
+  let r = ref (None : a option) in
+  begin match x with Int -> r := Some 1 end;
+  !r (* ok *)
+;;

testsuite/tests/typing-gadts/test.ml.principal.reference

@@ -67,8 +67,22 @@ Error: This pattern matches values of type int t
      ^^^^^^^^^^^^^
 Error: This pattern matches values of type ([? `A ] as 'a) * bool t
        but a pattern was expected which matches values of type 'a * int t
-#                                     Characters 288-289:
+#                                 Characters 300-301:
       | BoolLit b -> b
                      ^
 Error: This expression has type bool but an expression was expected of type s
+#   type 'a t = Int : int t
+#   val ky : 'a -> 'a -> 'a = <fun>
+#         val test : 'a t -> 'a = <fun>
+#       Characters 87-88:
+    in r
+       ^
+Error: This expression has type int but an expression was expected of type a
+#       val test : 'a t -> 'a = <fun>
+#         Characters 122-124:
+    !r (* normalized to int option *)
+    ^^
+Error: This expression has type int option
+       but an expression was expected of type a option
+#         val test2 : 'a t -> 'a option = <fun>
 # 

testsuite/tests/typing-gadts/test.ml.reference

@@ -66,9 +66,29 @@ Error: This pattern matches values of type int t
      ^^^^^^^^^^^^^
 Error: This pattern matches values of type ([? `A ] as 'a) * bool t
        but a pattern was expected which matches values of type 'a * int t
-#                                     module Propagation :
-  sig
-    type 'a t = IntLit : int -> int t | BoolLit : bool -> bool t
-    val check : 'a t -> 'a
-  end
+#                                 Characters 300-301:
+      | BoolLit b -> b
+                     ^
+Error: This expression has type bool but an expression was expected of type
+         int
+#   type 'a t = Int : int t
+#   val ky : 'a -> 'a -> 'a = <fun>
+#         Characters 88-89:
+    in r
+       ^
+Error: This expression has type int but an expression was expected of type a
+#       Characters 87-88:
+    in r
+       ^
+Error: This expression has type int but an expression was expected of type a
+#       Characters 82-83:
+    in r (* fails too *)
+       ^
+Error: This expression has type int but an expression was expected of type a
+#         Characters 122-124:
+    !r (* normalized to int option *)
+    ^^
+Error: This expression has type int option
+       but an expression was expected of type a option
+#         val test2 : 'a t -> 'a option = <fun>
 # 

typing/ctype.ml

@@ -698,16 +698,18 @@ let rec update_level env level ty =
   let ty = repr ty in
   if ty.level > level then begin
     begin match ty.desc with
-      Tconstr(p, tl, abbrev)  when level < get_level env p ->
+      Tconstr(p, tl, abbrev)
+      when level < Env.map_newtype_level env (get_level env p) ->
         (* Try first to replace an abbreviation by its expansion. *)
         begin try
-          if is_newtype env p then raise Cannot_expand;
+          (* if is_newtype env p then raise Cannot_expand; *)
           link_type ty (!forward_try_expand_once env ty);
           update_level env level ty
         with Cannot_expand ->
           (* +++ Levels should be restored... *)
           (* Format.printf "update_level: %i < %i@." level (get_level env p); *)
-          raise (Unify [(ty, newvar2 level)])
+          if level < get_level env p then raise (Unify [(ty, newvar2 level)]);
+          iter_type_expr (update_level env level) ty
         end
     | Tpackage (p, _, _) when level < get_level env p ->
         raise (Unify [(ty, newvar2 level)])
@@ -1699,15 +1701,16 @@ let deep_occur t0 ty =
 
 let newtype_level = ref None
 
+let get_newtype_level () = 
+  match !newtype_level with
+  | None -> assert false
+  | Some x -> x
+
 (* a local constraint can be added only if the rhs 
    of the constraint does not contain any Tvars.
    They need to be removed using this function *)
 let reify env t =
-  let newtype_level = 
-    match !newtype_level with
-    | None -> assert false
-    | Some x -> x
-  in
+  let newtype_level = get_newtype_level () in
   let create_fresh_constr lev row = 
       let decl = new_declaration (Some (newtype_level)) None in
       let name = 
@@ -1997,7 +2000,7 @@ and mcomp_record_description type_pairs subst env =
 let mcomp env t1 t2 = 
   mcomp (TypePairs.create 4) () env t1 t2
 
-let get_newtype_level env path = 
+let find_newtype_level env path = 
   match (Env.find_type path env).type_newtype_level with
     | None -> assert false
     | Some x -> x
@@ -2128,32 +2131,35 @@ and unify3 env t1 t1' t2 t2' =
           when is_abstract_newtype !env path && is_abstract_newtype !env path'
           && umode = Pattern -> 
             let source,destination = 
-              if get_newtype_level !env path > get_newtype_level !env path'
+              if find_newtype_level !env path > find_newtype_level !env path'
               then  p,t2'
               else  p',t1'
             in
             let destination = duplicate_type destination in 
-            let source_lev = get_newtype_level !env (Path.Pident source) in
+            let source_lev = find_newtype_level !env (Path.Pident source) in
             let decl = new_declaration (Some source_lev) (Some destination) in
-            env := Env.add_local_constraint source decl !env;
+            let newtype_level = get_newtype_level () in
+            env := Env.add_local_constraint source decl newtype_level !env;
             cleanup_abbrev ()          
         | (Tconstr ((Path.Pident p) as path,[],_), _)
           when is_abstract_newtype !env path && umode = Pattern -> 
             reify env t2';
             local_non_recursive_abbrev !env (Path.Pident p) t2';
             let t2' = duplicate_type t2' in
-            let source_level = get_newtype_level !env path in
+            let source_level = find_newtype_level !env path in
             let decl = new_declaration (Some source_level) (Some t2') in
-            env := Env.add_local_constraint p decl !env;
+            let newtype_level = get_newtype_level () in
+            env := Env.add_local_constraint p decl newtype_level !env;
             cleanup_abbrev ()          
         | (_, Tconstr ((Path.Pident p) as path,[],_))
           when is_abstract_newtype !env path && umode = Pattern -> 
             reify env t1' ;
             local_non_recursive_abbrev !env (Path.Pident p) t1';
             let t1' = duplicate_type t1' in
-            let source_level = get_newtype_level !env path in
+            let source_level = find_newtype_level !env path in
             let decl = new_declaration (Some source_level) (Some t1') in
-            env := Env.add_local_constraint p decl !env; 
+            let newtype_level = get_newtype_level () in
+            env := Env.add_local_constraint p decl newtype_level !env;
             cleanup_abbrev ()
         | (Tconstr (p1,_,_), Tconstr (p2,_,_)) when umode = Pattern ->
             reify env t1';

typing/env.ml

@@ -56,6 +56,7 @@ type t = {
   cltypes: (Path.t * cltype_declaration) Ident.tbl;
   summary: summary;
   local_constraints: bool;
+  level_map: (int * int) list;
 }
 
 and module_components = module_components_repr Lazy.t
@@ -95,7 +96,7 @@ let empty = {
   modules = Ident.empty; modtypes = Ident.empty;
   components = Ident.empty; classes = Ident.empty;
   cltypes = Ident.empty; 
-  summary = Env_empty; local_constraints = false; }
+  summary = Env_empty; local_constraints = false; level_map = [] }
 
 let diff_keys is_local tbl1 tbl2 =
   let keys2 = Ident.keys tbl2 in
@@ -446,6 +447,33 @@ and lookup_class =
 and lookup_cltype =
   lookup (fun env -> env.cltypes) (fun sc -> sc.comp_cltypes)
 
+(* Level handling *)
+
+(* The level map is a list of pairs describing separate segments (lv,lv'),
+   lv < lv', organized in decreasing order.
+   The definition level is obtained by mapping a level in a segment to the
+   high limit of this segment.
+   The definition level of a newtype should be greater or equal to
+   the highest level of the newtypes in its manifest type.
+ *)
+
+let rec map_level lv = function
+  | [] -> lv
+  | (lv1, lv2) :: rem ->
+      if lv > lv2 then lv else
+      if lv >= lv1 then lv2 else map_level lv rem
+
+let map_newtype_level env lv = map_level lv env.level_map
+
+(* precondition: lv < lv' *)
+let rec add_level lv lv' = function
+  | [] -> [lv, lv']
+  | (lv1, lv2) :: rem as l ->
+      if lv2 < lv then (lv, lv') :: l else
+      if lv' < lv1 then (lv1, lv2) :: add_level lv lv' rem
+      else add_level (max lv lv1) (min lv' lv2) rem      
+
+
 (* Expand manifest module type names at the top of the given module type *)
 
 let rec scrape_modtype mty env =
@@ -739,9 +767,14 @@ and add_class id ty env =
 and add_cltype id ty env =
   store_cltype id (Pident id) ty env
 
-let add_local_constraint id info 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
-  { env with local_constraints = true }
+      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 }
+  | _ -> assert false
 
 (* Insertion of bindings by name *)
 

typing/env.mli

@@ -21,6 +21,7 @@ type t
 val empty: t
 val initial: t
 val diff: t -> t -> Ident.t list
+val map_newtype_level: t -> int -> int
 
 (* Lookup by paths *)
 
@@ -64,7 +65,7 @@ val add_module: Ident.t -> module_type -> t -> t
 val add_modtype: Ident.t -> modtype_declaration -> t -> t
 val add_class: Ident.t -> class_declaration -> t -> t
 val add_cltype: Ident.t -> cltype_declaration -> t -> t
-val add_local_constraint: Ident.t -> type_declaration -> t -> t
+val add_local_constraint: Ident.t -> type_declaration -> int -> t -> t
 
 (* Insertion of all fields of a signature. *)