Fix PR#6158

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

2 files changed, 74 insertions, 73 deletions

diff --git a/Changes b/Changes
index c874ea8c4..8f920dc17 100644
--- a/Changes
+++ b/Changes
@@ -239,6 +239,7 @@ Bug fixes:
 - PR#6090: Module constraint + private type seems broken in ocaml 4.01.0
 - PR#6109: Typos in ocamlbuild error messages
 - PR#6123: Assert failure when self escapes its class
+- PR#6158: Fatal error using GADTs
 
 Feature wishes:
 - PR#5181: Merge common floating point constants in ocamlopt
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 5b1f1c2e9..1d91fb767 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -1919,78 +1919,78 @@ let non_aliasable p decl =
    and that both their objects and variants are closed
  *)
 
-let rec mcomp type_pairs subst env t1 t2 =
+let rec mcomp type_pairs env t1 t2 =
   if t1 == t2 then () else
   let t1 = repr t1 in
   let t2 = repr t2 in
   if t1 == t2 then () else
-    match (t1.desc, t2.desc) with
-      | (Tvar _, _)
-      | (_, Tvar _)  ->
-        fatal_error "types should not include variables"
-      | (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 ->
-        ()
-      | _ ->
-        let t1' = expand_head_opt env t1 in
-        let t2' = expand_head_opt env t2 in
-        (* Expansion may have changed the representative of the types... *)
-        let t1' = repr t1' and t2' = repr t2' in
-        if t1' == t2' then () else
-          begin try TypePairs.find type_pairs (t1', t2')
-          with Not_found ->
-              TypePairs.add type_pairs (t1', t2') ();
-              match (t1'.desc, t2'.desc) with
-                  (Tvar _, Tvar _) -> assert false
-                | (Tarrow (l1, t1, u1, _), Tarrow (l2, t2, u2, _))
-                  when l1 = l2 || not (is_optional l1 || is_optional l2) ->
-                  mcomp type_pairs subst env t1 t2;
-                  mcomp type_pairs subst env u1 u2;
-                | (Ttuple tl1, Ttuple tl2) ->
-                  mcomp_list type_pairs subst env tl1 tl2
-                | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) ->
-                  mcomp_type_decl type_pairs subst env p1 p2 tl1 tl2
-                | (Tconstr (p, _, _), _) | (_, Tconstr (p, _, _)) ->
-                  let decl = Env.find_type p env in
-                  if non_aliasable p decl then raise (Unify [])
-                | (Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2))
-                  when Path.same p1 p2 && n1 = n2 ->
-                  mcomp_list type_pairs subst env tl1 tl2
-                | (Tvariant row1, Tvariant row2) ->
-                  mcomp_row type_pairs subst env row1 row2
-                | (Tobject (fi1, _), Tobject (fi2, _)) ->
-                  mcomp_fields type_pairs subst env fi1 fi2
-                | (Tfield _, Tfield _) ->       (* Actually unused *)
-                  mcomp_fields type_pairs subst env t1' t2'
-                | (Tnil, Tnil) ->
-                  ()
-                | (Tpoly (t1, []), Tpoly (t2, [])) ->
-                  mcomp type_pairs subst env t1 t2
-                | (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
-                  enter_poly env univar_pairs t1 tl1 t2 tl2
-                    (mcomp type_pairs subst env)
-                | (Tunivar _, Tunivar _) ->
-                  unify_univar t1' t2' !univar_pairs
-                | (_, _) ->
-                  raise (Unify [])
-          end
+  match (t1.desc, t2.desc) with
+  | (Tvar _, _)
+  | (_, Tvar _)  ->
+      ()
+  | (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 ->
+      ()
+  | _ ->
+      let t1' = expand_head_opt env t1 in
+      let t2' = expand_head_opt env t2 in
+      (* Expansion may have changed the representative of the types... *)
+      let t1' = repr t1' and t2' = repr t2' in
+      if t1' == t2' then () else
+      begin try TypePairs.find type_pairs (t1', t2')
+      with Not_found ->
+        TypePairs.add type_pairs (t1', t2') ();
+        match (t1'.desc, t2'.desc) with
+          (Tvar _, Tvar _) -> assert false
+        | (Tarrow (l1, t1, u1, _), Tarrow (l2, t2, u2, _))
+          when l1 = l2 || not (is_optional l1 || is_optional l2) ->
+            mcomp type_pairs env t1 t2;
+            mcomp type_pairs env u1 u2;
+        | (Ttuple tl1, Ttuple tl2) ->
+            mcomp_list type_pairs env tl1 tl2
+        | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) ->
+            mcomp_type_decl type_pairs env p1 p2 tl1 tl2
+        | (Tconstr (p, _, _), _) | (_, Tconstr (p, _, _)) ->
+            let decl = Env.find_type p env in
+            if non_aliasable p decl then raise (Unify [])
+        | (Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2))
+          when Path.same p1 p2 && n1 = n2 ->
+            mcomp_list type_pairs env tl1 tl2
+        | (Tvariant row1, Tvariant row2) ->
+            mcomp_row type_pairs env row1 row2
+        | (Tobject (fi1, _), Tobject (fi2, _)) ->
+            mcomp_fields type_pairs env fi1 fi2
+        | (Tfield _, Tfield _) ->       (* Actually unused *)
+            mcomp_fields type_pairs env t1' t2'
+        | (Tnil, Tnil) ->
+            ()
+        | (Tpoly (t1, []), Tpoly (t2, [])) ->
+            mcomp type_pairs env t1 t2
+        | (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
+            enter_poly env univar_pairs t1 tl1 t2 tl2
+              (mcomp type_pairs env)
+        | (Tunivar _, Tunivar _) ->
+            unify_univar t1' t2' !univar_pairs
+        | (_, _) ->
+            raise (Unify [])
+      end
 
-and mcomp_list type_pairs subst env tl1 tl2 =
+and mcomp_list type_pairs env tl1 tl2 =
   if List.length tl1 <> List.length tl2 then
     raise (Unify []);
-  List.iter2 (mcomp type_pairs subst env) tl1 tl2
+  List.iter2 (mcomp type_pairs env) tl1 tl2
 
-and mcomp_fields type_pairs subst env ty1 ty2 =
+and mcomp_fields type_pairs env ty1 ty2 =
   if not (concrete_object ty1 && concrete_object ty2) then assert false;
   let (fields2, rest2) = flatten_fields ty2 in
   let (fields1, rest1) = flatten_fields ty1 in
   let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
-  mcomp type_pairs subst env rest1 rest2;
+  mcomp type_pairs env rest1 rest2;
   if miss1 <> []  && (object_row ty1).desc = Tnil
   || miss2 <> []  && (object_row ty2).desc = Tnil then raise (Unify []);
   List.iter
     (function (n, k1, t1, k2, t2) ->
        mcomp_kind k1 k2;
-       mcomp type_pairs subst env t1 t2)
+       mcomp type_pairs env t1 t2)
     pairs
 
 and mcomp_kind k1 k2 =
@@ -2001,7 +2001,7 @@ and mcomp_kind k1 k2 =
   | (Fpresent, Fpresent) -> ()
   | _                    -> raise (Unify [])
 
-and mcomp_row type_pairs subst env row1 row2 =
+and mcomp_row type_pairs env row1 row2 =
   let row1 = row_repr row1 and row2 = row_repr row2 in
   let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in
   let cannot_erase (_,f) =
@@ -2020,15 +2020,15 @@ and mcomp_row type_pairs subst env row1 row2 =
       | (Reither (true, _, _, _) | Rabsent), Rpresent (Some _) ->
           raise (Unify [])
       | Rpresent(Some t1), Rpresent(Some t2) ->
-          mcomp type_pairs subst env t1 t2
+          mcomp type_pairs env t1 t2
       | Rpresent(Some t1), Reither(false, tl2, _, _) ->
-          List.iter (mcomp type_pairs subst env t1) tl2
+          List.iter (mcomp type_pairs env t1) tl2
       | Reither(false, tl1, _, _), Rpresent(Some t2) ->
-          List.iter (mcomp type_pairs subst env t2) tl1
+          List.iter (mcomp type_pairs env t2) tl1
       | _ -> ())
     pairs
 
-and mcomp_type_decl type_pairs subst env p1 p2 tl1 tl2 =
+and mcomp_type_decl type_pairs env p1 p2 tl1 tl2 =
   try
     let decl = Env.find_type p1 env in
     let decl' = Env.find_type p2 env in
@@ -2042,16 +2042,16 @@ and mcomp_type_decl type_pairs subst env p1 p2 tl1 tl2 =
         with Not_found -> List.map (fun _ -> false) tl1
       in
       List.iter2
-        (fun i (t1,t2) -> if i then mcomp type_pairs subst env t1 t2)
+        (fun i (t1,t2) -> if i then mcomp type_pairs env t1 t2)
         inj (List.combine tl1 tl2)
     end
     else match decl.type_kind, decl'.type_kind with
     | Type_record (lst,r), Type_record (lst',r') when r = r' ->
-        mcomp_list type_pairs subst env tl1 tl2;
-        mcomp_record_description type_pairs subst env lst lst'
+        mcomp_list type_pairs env tl1 tl2;
+        mcomp_record_description type_pairs env lst lst'
     | Type_variant v1, Type_variant v2 ->
-        mcomp_list type_pairs subst env tl1 tl2;
-        mcomp_variant_description type_pairs subst env v1 v2
+        mcomp_list type_pairs env tl1 tl2;
+        mcomp_variant_description type_pairs env v1 v2
     | Type_variant _, Type_record _
     | Type_record _, Type_variant _ -> raise (Unify [])
     | _ ->
@@ -2059,18 +2059,18 @@ and mcomp_type_decl type_pairs subst env p1 p2 tl1 tl2 =
         || is_datatype decl && non_aliasable p2 decl' then raise (Unify [])
   with Not_found -> ()
 
-and mcomp_type_option type_pairs subst env t t' =
+and mcomp_type_option type_pairs env t t' =
   match t, t' with
     None, None -> ()
-  | Some t, Some t' -> mcomp type_pairs subst env t t'
+  | Some t, Some t' -> mcomp type_pairs env t t'
   | _ -> raise (Unify [])
 
-and mcomp_variant_description type_pairs subst env xs ys =
+and mcomp_variant_description type_pairs env xs ys =
   let rec iter = fun x y ->
     match x, y with
     (id, tl, t) :: xs, (id', tl', t') :: ys   ->
-      mcomp_type_option type_pairs subst env t t';
-      mcomp_list type_pairs subst env tl tl';
+      mcomp_type_option type_pairs env t t';
+      mcomp_list type_pairs env tl tl';
       if Ident.name id = Ident.name id'
       then iter xs ys
       else raise (Unify [])
@@ -2079,11 +2079,11 @@ and mcomp_variant_description type_pairs subst env xs ys =
   in
   iter xs ys
 
-and mcomp_record_description type_pairs subst env =
+and mcomp_record_description type_pairs env =
   let rec iter = fun x y ->
     match x, y with
       (id, mutable_flag, t) :: xs, (id', mutable_flag', t') :: ys ->
-        mcomp type_pairs subst env t t';
+        mcomp type_pairs env t t';
         if Ident.name id = Ident.name id' && mutable_flag = mutable_flag'
         then iter xs ys
         else raise (Unify [])
@@ -2093,7 +2093,7 @@ and mcomp_record_description type_pairs subst env =
   iter
 
 let mcomp env t1 t2 =
-  mcomp (TypePairs.create 4) () env t1 t2
+  mcomp (TypePairs.create 4) env t1 t2
 
 (* Real unification *)