PR#7233: GADT equations for non-local abstract types

15 files changed, 166 insertions, 37 deletions

diff --git a/Changes b/Changes
index 41d90bb230..fe03410952 100644
--- a/Changes
+++ b/Changes
@@ -12,6 +12,9 @@ OCaml 4.04.0:
 - GPR#301: local exception declarations "let exception ... in"
   (Alain Frisch)
 
+- PR#7233: Support GADT equations on non-local abstract types
+  (Jacques Garrigue)
+
 ### Compilers:
 
 - PR#7023, GPR#336: Better unboxing strategy
diff --git a/debugger/loadprinter.ml b/debugger/loadprinter.ml
index 2e467a729f..1f4ceebe1d 100644
--- a/debugger/loadprinter.ml
+++ b/debugger/loadprinter.ml
@@ -109,7 +109,7 @@ let () =
   ignore (Env.read_signature "Topdirs" topdirs)
 
 let match_printer_type desc typename =
-  let (printer_type, _) =
+  let printer_type =
     try
       Env.lookup_type (Ldot(Lident "Topdirs", typename)) Env.empty
     with Not_found ->
diff --git a/testsuite/tests/typing-gadts/nested_equations.ml b/testsuite/tests/typing-gadts/nested_equations.ml
new file mode 100644
index 0000000000..4eb39daa79
--- /dev/null
+++ b/testsuite/tests/typing-gadts/nested_equations.ml
@@ -0,0 +1,41 @@
+(* Tests for nested equations (bind abstract types from other modules) *)
+
+type _ t = Int : int t;;
+
+let to_int (type a) (w : a t) (x : a) : int = let Int = w in x;;
+
+let w_bool : bool t = Obj.magic 0;;
+let f_bool (x : bool) : int = let Int = w_bool in x;; (* fail *)
+
+let w_buffer : Buffer.t t = Obj.magic 0;;
+let f_buffer (x : Buffer.t) : int = let Int = w_buffer in x;; (* ok *)
+
+let w_spec : Arg.spec t = Obj.magic 0;;
+let f_spec (x : Arg.spec) : int = let Int = w_spec in x;; (* ok *)
+
+module M : sig type u val w : u t val x : u end =
+  struct type u = int let w = Int let x = 33 end;;
+let m_x : int = let Int = M.w in M.x;;
+
+module F (X : sig type u = int val x : u end) = struct let x : int = X.x end;;
+let fm_x : int = let Int = M.w in let module FM = F(M) in FM.x;; (* ok *)
+
+module M' = struct module M : sig type u val w : u t val x : u end = M end;;
+module F' (X : sig module M : sig type u = int val x : u end end) =
+  struct let x : int = X.M.x end;;
+let fm'_x : int =
+  let Int = M'.M.w in let module FM' = F'(M') in FM'.x;; (* ok *)
+
+(* PR#7233 *)
+
+type (_, _) eq = Refl : ('a, 'a) eq
+
+module type S = sig
+  type t
+  val eql : (t, int) eq
+end
+
+module F (M : S) = struct
+  let zero : M.t =
+    let Refl = M.eql in 0
+end;;
diff --git a/testsuite/tests/typing-gadts/nested_equations.ml.principal.reference b/testsuite/tests/typing-gadts/nested_equations.ml.principal.reference
new file mode 100644
index 0000000000..db41c37005
--- /dev/null
+++ b/testsuite/tests/typing-gadts/nested_equations.ml.principal.reference
@@ -0,0 +1,33 @@
+
+#     type _ t = Int : int t
+#   val to_int : 'a t -> 'a -> int = <fun>
+#   val w_bool : bool t = Int
+# Characters 34-37:
+  let f_bool (x : bool) : int = let Int = w_bool in x;; (* fail *)
+                                    ^^^
+Error: This pattern matches values of type int t
+       but a pattern was expected which matches values of type bool t
+       Type int is not compatible with type bool 
+#   val w_buffer : Buffer.t t = Int
+# val f_buffer : Buffer.t -> int = <fun>
+#   val w_spec : Arg.spec t = Int
+# Characters 38-41:
+  let f_spec (x : Arg.spec) : int = let Int = w_spec in x;; (* ok *)
+                                        ^^^
+Error: This pattern matches values of type int t
+       but a pattern was expected which matches values of type Arg.spec t
+       Type int is not compatible with type Arg.spec 
+#     module M : sig type u val w : u t val x : u end
+# val m_x : int = 33
+#   module F :
+  functor (X : sig type u = int val x : u end) -> sig val x : int end
+# val fm_x : int = 33
+#   module M' : sig module M : sig type u val w : u t val x : u end end
+#   module F' :
+  functor (X : sig module M : sig type u = int val x : u end end) ->
+    sig val x : int end
+#   val fm'_x : int = 33
+#                           type (_, _) eq = Refl : ('a, 'a) eq
+module type S = sig type t val eql : (t, int) eq end
+module F : functor (M : S) -> sig val zero : M.t end
+# 
diff --git a/testsuite/tests/typing-gadts/nested_equations.ml.reference b/testsuite/tests/typing-gadts/nested_equations.ml.reference
new file mode 100644
index 0000000000..db41c37005
--- /dev/null
+++ b/testsuite/tests/typing-gadts/nested_equations.ml.reference
@@ -0,0 +1,33 @@
+
+#     type _ t = Int : int t
+#   val to_int : 'a t -> 'a -> int = <fun>
+#   val w_bool : bool t = Int
+# Characters 34-37:
+  let f_bool (x : bool) : int = let Int = w_bool in x;; (* fail *)
+                                    ^^^
+Error: This pattern matches values of type int t
+       but a pattern was expected which matches values of type bool t
+       Type int is not compatible with type bool 
+#   val w_buffer : Buffer.t t = Int
+# val f_buffer : Buffer.t -> int = <fun>
+#   val w_spec : Arg.spec t = Int
+# Characters 38-41:
+  let f_spec (x : Arg.spec) : int = let Int = w_spec in x;; (* ok *)
+                                        ^^^
+Error: This pattern matches values of type int t
+       but a pattern was expected which matches values of type Arg.spec t
+       Type int is not compatible with type Arg.spec 
+#     module M : sig type u val w : u t val x : u end
+# val m_x : int = 33
+#   module F :
+  functor (X : sig type u = int val x : u end) -> sig val x : int end
+# val fm_x : int = 33
+#   module M' : sig module M : sig type u val w : u t val x : u end end
+#   module F' :
+  functor (X : sig module M : sig type u = int val x : u end end) ->
+    sig val x : int end
+#   val fm'_x : int = 33
+#                           type (_, _) eq = Refl : ('a, 'a) eq
+module type S = sig type t val eql : (t, int) eq end
+module F : functor (M : S) -> sig val zero : M.t end
+# 
diff --git a/toplevel/opttopdirs.ml b/toplevel/opttopdirs.ml
index fe3119cecd..6d833ddf19 100644
--- a/toplevel/opttopdirs.ml
+++ b/toplevel/opttopdirs.ml
@@ -111,7 +111,7 @@ type 'a printer_type_new = Format.formatter -> 'a -> unit
 type 'a printer_type_old = 'a -> unit
 
 let match_printer_type ppf desc typename =
-  let (printer_type, _) =
+  let printer_type =
     try
       Env.lookup_type (Ldot(Lident "Topdirs", typename)) !toplevel_env
     with Not_found ->
diff --git a/toplevel/topdirs.ml b/toplevel/topdirs.ml
index b9c25692f0..a8c237c3a4 100644
--- a/toplevel/topdirs.ml
+++ b/toplevel/topdirs.ml
@@ -281,7 +281,7 @@ type 'a printer_type_new = Format.formatter -> 'a -> unit
 type 'a printer_type_old = 'a -> unit
 
 let printer_type ppf typename =
-  let (printer_type, _) =
+  let printer_type =
     try
       Env.lookup_type (Ldot(Lident "Topdirs", typename)) !toplevel_env
     with Not_found ->
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 153bcfc519..7328f93be5 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -1938,6 +1938,17 @@ let non_aliasable p decl =
   (* in_pervasives p ||  (subsumed by in_current_module) *)
   in_current_module p && decl.type_newtype_level = None
 
+let is_instantiable env p =
+  try
+    let decl = Env.find_type p env in
+    decl.type_kind = Type_abstract &&
+    decl.type_private = Public &&
+    decl.type_arity = 0 &&
+    decl.type_manifest = None &&
+    not (non_aliasable p decl)
+  with Not_found -> false
+  
+
 (* PR#7113: -safe-string should be a global property *)
 let compatible_paths p1 p2 =
   let open Predef in
@@ -2167,13 +2178,13 @@ let find_lowest_level ty =
 let find_newtype_level env path =
   try match (Env.find_type path env).type_newtype_level with
     Some x -> x
-  | None -> assert false
-  with Not_found -> assert false
+  | None -> raise Not_found
+  with Not_found -> let lev = Path.binding_time path in (lev, lev)
 
 let add_gadt_equation env source destination =
-  if local_non_recursive_abbrev !env (Path.Pident source) destination then begin
+  if local_non_recursive_abbrev !env source destination then begin
     let destination = duplicate_type destination in
-    let source_lev = find_newtype_level !env (Path.Pident source) in
+    let source_lev = find_newtype_level !env source in
     let decl = new_declaration (Some source_lev) (Some destination) in
     let newtype_level = get_newtype_level () in
     env := Env.add_local_constraint source decl newtype_level !env;
@@ -2223,10 +2234,10 @@ let complete_type_list ?(allow_absent=false) env nl1 lv2 mty2 nl2 tl2 =
         nt2 :: complete (if n = n2 then nl else nl1) ntl'
     | n :: nl, _ ->
         try
-          let (_, decl) =
+          let path =
             Env.lookup_type (concat_longident (Longident.Lident "Pkg") n) env'
           in
-          match decl with
+          match Env.find_type path env' with
             {type_arity = 0; type_kind = Type_abstract;
              type_private = Public; type_manifest = Some t2} ->
                (n, nondep_instance env' lv2 id2 t2) :: complete nl ntl2
@@ -2424,24 +2435,24 @@ and unify3 env t1 t1' t2 t2' =
                       reify env t1; reify env t2
                   end)
               inj (List.combine tl1 tl2)
-      | (Tconstr ((Path.Pident p) as path,[],_),
-         Tconstr ((Path.Pident p') as path',[],_))
-        when is_newtype !env path && is_newtype !env path'
+      | (Tconstr (path,[],_),
+         Tconstr (path',[],_))
+        when is_instantiable !env path && is_instantiable !env path'
         && !generate_equations ->
           let source, destination =
             if find_newtype_level !env path > find_newtype_level !env path'
-            then  p,t2'
-            else  p',t1'
+            then  path , t2'
+            else  path', t1'
           in
           add_gadt_equation env source destination
-      | (Tconstr ((Path.Pident p) as path,[],_), _)
-        when is_newtype !env path && !generate_equations ->
+      | (Tconstr (path,[],_), _)
+        when is_instantiable !env path && !generate_equations ->
           reify env t2';
-          add_gadt_equation env p t2'
-      | (_, Tconstr ((Path.Pident p) as path,[],_))
-        when is_newtype !env path && !generate_equations ->
+          add_gadt_equation env path t2'
+      | (_, Tconstr (path,[],_))
+        when is_instantiable !env path && !generate_equations ->
           reify env t1';
-          add_gadt_equation env p t1'
+          add_gadt_equation env path t1'
       | (Tconstr (_,_,_), _) | (_, Tconstr (_,_,_)) when !umode = Pattern ->
           reify env t1';
           reify env t2';
@@ -3656,7 +3667,8 @@ let rec lid_of_path ?(hash="") = function
       Longident.Lapply (lid_of_path ~hash p1, lid_of_path p2)
 
 let find_cltype_for_path env p =
-  let _path, cl_abbr = Env.lookup_type (lid_of_path ~hash:"#" p) env in
+  let cl_path = Env.lookup_type (lid_of_path ~hash:"#" p) env in
+  let cl_abbr = Env.find_type cl_path env in
 
   match cl_abbr.type_manifest with
     Some ty ->
diff --git a/typing/env.ml b/typing/env.ml
index 346d628dc3..512f3b85d9 100644
--- a/typing/env.ml
+++ b/typing/env.ml
@@ -1009,7 +1009,7 @@ let lookup_value ?loc lid env =
 let lookup_type ?loc lid env =
   let (path, (decl, _)) = lookup_type ?loc lid env in
   mark_type_used env (Longident.last lid) decl;
-  (path, decl)
+  path
 
 let mark_type_path env path =
   try
@@ -1685,12 +1685,12 @@ let add_local_type path info env =
   { env with
     local_constraints = PathMap.add path info env.local_constraints }
 
-let add_local_constraint id info elv env =
+let add_local_constraint path info elv env =
   match info with
     {type_manifest = Some _; type_newtype_level = Some (lv, _)} ->
       (* elv is the expansion level, lv is the definition level *)
       let info = {info with type_newtype_level = Some (lv, elv)} in
-      add_local_type (Pident id) info env
+      add_local_type path info env
   | _ -> assert false
 
 
diff --git a/typing/env.mli b/typing/env.mli
index db4368832c..31982c2bf5 100644
--- a/typing/env.mli
+++ b/typing/env.mli
@@ -107,7 +107,10 @@ val lookup_all_labels:
   ?loc:Location.t ->
   Longident.t -> t -> (label_description * (unit -> unit)) list
 val lookup_type:
-  ?loc:Location.t -> Longident.t -> t -> Path.t * type_declaration
+  ?loc:Location.t -> Longident.t -> t -> Path.t
+  (* Since 4.04, this function no longer returns [type_description].
+     To obtain it, you should either call [Env.find_type], or replace
+     it by [Typetexp.find_type] *)
 val lookup_module:
   load:bool -> ?loc:Location.t -> Longident.t -> t -> Path.t
 val lookup_modtype:
@@ -137,7 +140,7 @@ val add_module_declaration: ?arg:bool -> Ident.t -> module_declaration -> 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 -> class_type_declaration -> t -> t
-val add_local_constraint: Ident.t -> type_declaration -> int -> t -> t
+val add_local_constraint: Path.t -> type_declaration -> int -> t -> t
 val add_local_type: Path.t -> type_declaration -> t -> t
 
 (* Insertion of all fields of a signature. *)
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index d8c8878741..4a99ca2259 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -336,7 +336,7 @@ let is_unambiguous path env =
       (* also allow repeatedly defining and opening (for toplevel) *)
       let id = lid_of_path p in
       List.for_all (fun p -> lid_of_path p = id) rem &&
-      Path.same p (fst (Env.lookup_type id env))
+      Path.same p (Env.lookup_type id env)
 
 let rec get_best_path r =
   match !r with
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 2bf4568730..e3dfdd6eed 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -1655,7 +1655,8 @@ let rec approx_type env sty =
       newty (Ttuple (List.map (approx_type env) args))
   | Ptyp_constr (lid, ctl) ->
       begin try
-        let (path, decl) = Env.lookup_type lid.txt env in
+        let path = Env.lookup_type lid.txt env in
+        let decl = Env.find_type path env in
         if List.length ctl <> decl.type_arity then raise Not_found;
         let tyl = List.map (approx_type env) ctl in
         newconstr path tyl
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index 4f5a088e5f..eb12ac3778 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -320,7 +320,7 @@ let transl_declaration env sdecl id =
     Ctype.end_def ();
   (* Add abstract row *)
     if is_fixed_type sdecl then begin
-      let (p, _) =
+      let p =
         try Env.lookup_type (Longident.Lident(Ident.name id ^ "#row")) env
         with Not_found -> assert false in
       set_fixed_row env sdecl.ptype_loc p decl
diff --git a/typing/typemod.ml b/typing/typemod.ml
index 09889c7945..2fdf9458b3 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -266,7 +266,7 @@ let merge_constraint initial_env loc sg constr =
           with Exit ->
             raise(Error(sdecl.ptype_loc, initial_env, With_need_typeconstr))
         in
-        let (path, _) =
+        let path =
           try Env.lookup_type lid.txt initial_env with Not_found -> assert false
         in
         let sub = Subst.add_type id path Subst.identity in
diff --git a/typing/typetexp.ml b/typing/typetexp.ml
index 103454d5c0..95524c80bf 100644
--- a/typing/typetexp.ml
+++ b/typing/typetexp.ml
@@ -112,25 +112,26 @@ let rec narrow_unbound_lid_error : 'a. _ -> _ -> _ -> _ -> 'a =
   end;
   raise (Error (loc, env, make_error lid))
 
-let find_component lookup make_error env loc lid =
+let find_component (lookup : ?loc:_ -> _) make_error env loc lid =
   try
     match lid with
     | Longident.Ldot (Longident.Lident "*predef*", s) ->
-        lookup ?loc:(Some loc) (Longident.Lident s) Env.initial_safe_string
+        lookup ~loc (Longident.Lident s) Env.initial_safe_string
     | _ ->
-        lookup ?loc:(Some loc) lid env
+        lookup ~loc lid env
   with Not_found ->
     narrow_unbound_lid_error env loc lid make_error
   | Env.Recmodule ->
     raise (Error (loc, env, Illegal_reference_to_recursive_module))
 
 let find_type env loc lid =
-  let (path, decl) as r =
+  let path =
     find_component Env.lookup_type (fun lid -> Unbound_type_constructor lid)
       env loc lid
   in
+  let decl = Env.find_type path env in
   Builtin_attributes.check_deprecated loc decl.type_attributes (Path.name path);
-  r
+  (path, decl)
 
 let find_constructor =
   find_component Env.lookup_constructor (fun lid -> Unbound_constructor lid)
@@ -381,7 +382,8 @@ let rec transl_type env policy styp =
   | Ptyp_class(lid, stl) ->
       let (path, decl, _is_variant) =
         try
-          let (path, decl) = Env.lookup_type lid.txt env in
+          let path = Env.lookup_type lid.txt env in
+          let decl = Env.find_type path env in
           let rec check decl =
             match decl.type_manifest with
               None -> raise Not_found
@@ -402,7 +404,8 @@ let rec transl_type env policy styp =
             | Longident.Ldot(r, s)   -> Longident.Ldot (r, "#" ^ s)
             | Longident.Lapply(_, _) -> fatal_error "Typetexp.transl_type"
           in
-          let (path, decl) = Env.lookup_type lid2 env in
+          let path = Env.lookup_type lid2 env in
+          let decl = Env.find_type path env in
           (path, decl, false)
         with Not_found ->
           ignore (find_class env styp.ptyp_loc lid.txt); assert false