unify return type first

ocaml · May 20, 2020 · 951cf8b · 951cf8b
1 parent c172b2a
commit 951cf8b
Show file tree

Hide file tree

Showing 2 changed files with 40 additions and 8 deletions.
diff --git a/testsuite/tests/typing-gadts/name_existentials.ml b/testsuite/tests/typing-gadts/name_existentials.ml
@@ -49,3 +49,29 @@ Line 1, characters 36-53:
 Error: This type does not bind all existentials in the constructor:
          type a. a * (a -> a list)
 |}]
+
+(* with GADT unification *)
+type _ expr =
+  | Int : int -> int expr
+  | Add : (int -> int -> int) expr
+  | App : ('a -> 'b) expr * 'a expr -> 'b expr
+
+let rec eval : type t. t expr -> t = function
+    Int n -> n
+  | Add -> (+)
+  | App (type a) (f, x : _ * a expr) -> eval f (eval x : a)
+[%%expect{|
+type _ expr =
+    Int : int -> int expr
+  | Add : (int -> int -> int) expr
+  | App : ('a -> 'b) expr * 'a expr -> 'b expr
+val eval : 't expr -> 't = <fun>
+|}]
+
+let rec test : type a. a expr -> a = function
+  | Int (type b) (n : a) -> n
+  | Add -> (+)
+  | App (type b) (f, x : (b -> a) expr * _) -> test f (test x : b)
+[%%expect{|
+val test : 'a expr -> 'a = <fun>
+|}]
diff --git a/typing/typecore.ml b/typing/typecore.ml
@@ -1546,12 +1546,23 @@ and type_pat_aux
         raise(Error(loc, !env, Constructor_arity_mismatch(lid.txt,
                                      constr.cstr_arity, List.length sargs)));
       begin_def ();
+      let expected_ty = instance expected_ty in
+      (* PR#7214: do not use gadt unification for toplevel lets *)
+      let unify_res ty_res =
+        unify_pat_types loc env ty_res expected_ty
+          ~refine:(refine || constr.cstr_generalized && no_existentials = None)
+      in
       let expansion_scope = get_gadt_equations_level () in
-      let (ty_args, ty_res, _ty_ex) =
+      let ty_args, ty_res =
         match oty with
           None ->
-            instance_constructor ~in_pattern:(env, expansion_scope) constr
+            let ty_args, ty_res, _ =
+              instance_constructor ~in_pattern:(env, expansion_scope) constr in
+            unify_res ty_res;
+            ty_args, ty_res
         | Some (nl, sty) ->
+            let ty_args, ty_res, ty_ex = instance_constructor constr in
+            unify_res ty_res;
             let ids =
               List.map
                 (fun name ->
@@ -1565,7 +1576,6 @@ and type_pat_aux
             let cty, force = Typetexp.transl_simple_type_delayed !env sty in
             pattern_force := force :: !pattern_force;
             let ty = cty.ctyp_type in
-            let ty_args, ty_res, ty_ex = instance_constructor constr in
             begin match ty_args with
               [] -> ()
             | [ty_arg] ->
@@ -1584,12 +1594,8 @@ and type_pat_aux
                     raise (Error (cty.ctyp_loc, !env,
                                   Unbound_existential (ids, ty))))
               ids ty_ex);
-            ty_args, ty_res, ty_ex
+            ty_args, ty_res
       in
-      let expected_ty = instance expected_ty in
-      (* PR#7214: do not use gadt unification for toplevel lets *)
-      unify_pat_types loc env ty_res expected_ty
-        ~refine:(refine || constr.cstr_generalized && no_existentials = None);
       end_def ();
       generalize_structure expected_ty;
       generalize_structure ty_res;