Fix #10735 as suggested by @lpw25 (#10738)

Changes

@@ -350,6 +350,9 @@ Working version
   implementation of stat
   (Antonin Décimo, review by David Allsopp)
 
+- #10735: Uncaught unify exception from `build_as_type`
+  (Jacques Garrigue, report and review by Leo White)
+
 
 
 OCaml 4.13 maintenance branch

testsuite/tests/typing-gadts/pr10735.ml

@@ -0,0 +1,30 @@
+(* TEST
+   * expect
+*)
+
+module X : sig
+  type 'a t
+end = struct
+  type 'a t
+end
+
+type 'a t
+
+type (_,_) eq = Refl : ('a,'a) eq
+[%%expect{|
+module X : sig type 'a t end
+type 'a t
+type (_, _) eq = Refl : ('a, 'a) eq
+|}]
+
+let () =
+  let (Refl : (bool X.t, bool t) eq) as t = Obj.magic  () in ()
+[%%expect{|
+Line 2, characters 7-11:
+2 |   let (Refl : (bool X.t, bool t) eq) as t = Obj.magic  () in ()
+           ^^^^
+Error: This pattern matches values of type (bool X.t, bool X.t) eq
+       but a pattern was expected which matches values of type
+         (bool X.t, bool t) eq
+       Type bool X.t is not compatible with type bool t
+|}]

typing/typecore.ml

@@ -525,8 +525,8 @@ let enter_orpat_variables loc env  p1_vs p2_vs =
           raise (Error (loc, env, err)) in
   unify_vars p1_vs p2_vs
 
-let rec build_as_type env p =
-  let as_ty = build_as_type_aux env p in
+let rec build_as_type ~refine (env : Env.t ref) p =
+  let as_ty = build_as_type_aux ~refine env p in
   (* Cf. #1655 *)
   List.fold_left (fun as_ty (extra, _loc, _attrs) ->
     match extra with
@@ -542,11 +542,12 @@ let rec build_as_type env p =
       end_def ();
       generalize_structure ty;
       (* This call to unify can't fail since the pattern is well typed. *)
-      unify !env (instance as_ty) (instance ty);
+      unify_pat_types ~refine p.pat_loc env (instance as_ty) (instance ty);
       ty
   ) as_ty p.pat_extra
 
-and build_as_type_aux env p =
+and build_as_type_aux ~refine (env : Env.t ref) p =
+  let build_as_type = build_as_type ~refine in
   match p.pat_desc with
     Tpat_alias(p1,_, _) -> build_as_type env p1
   | Tpat_tuple pl ->
@@ -559,7 +560,7 @@ and build_as_type_aux env p =
       if keep then p.pat_type else
       let tyl = List.map (build_as_type env) pl in
       let ty_args, ty_res, _ = instance_constructor cstr in
-      List.iter2 (fun (p,ty) -> unify_pat env {p with pat_type = ty})
+      List.iter2 (fun (p,ty) -> unify_pat ~refine env {p with pat_type = ty})
         (List.combine pl tyl) ty_args;
       ty_res
   | Tpat_variant(l, p', _) ->
@@ -574,25 +575,26 @@ and build_as_type_aux env p =
       let ppl = List.map (fun (_, l, p) -> l.lbl_pos, p) lpl in
       let do_label lbl =
         let _, ty_arg, ty_res = instance_label false lbl in
-        unify_pat env {p with pat_type = ty} ty_res;
+        unify_pat ~refine env {p with pat_type = ty} ty_res;
         let refinable =
           lbl.lbl_mut = Immutable && List.mem_assoc lbl.lbl_pos ppl &&
           match get_desc lbl.lbl_arg with Tpoly _ -> false | _ -> true in
         if refinable then begin
           let arg = List.assoc lbl.lbl_pos ppl in
-          unify_pat env {arg with pat_type = build_as_type env arg} ty_arg
+          unify_pat ~refine env
+            {arg with pat_type = build_as_type env arg} ty_arg
         end else begin
           let _, ty_arg', ty_res' = instance_label false lbl in
-          unify !env ty_arg ty_arg';
-          unify_pat env p ty_res'
+          unify_pat_types ~refine p.pat_loc env ty_arg ty_arg';
+          unify_pat ~refine env p ty_res'
         end in
       Array.iter do_label lbl.lbl_all;
       ty
   | Tpat_or(p1, p2, row) ->
       begin match row with
         None ->
           let ty1 = build_as_type env p1 and ty2 = build_as_type env p2 in
-          unify_pat env {p2 with pat_type = ty2} ty1;
+          unify_pat ~refine env {p2 with pat_type = ty2} ty1;
           ty1
       | Some row ->
           let Row {fields; fixed; name} = row_repr row in
@@ -617,9 +619,9 @@ let solve_Ppat_poly_constraint ~refine env loc sty expected_ty =
       (cty, ty, ty')
   | _ -> assert false
 
-let solve_Ppat_alias env pat =
+let solve_Ppat_alias ~refine env pat =
   begin_def ();
-  let ty_var = build_as_type env pat in
+  let ty_var = build_as_type ~refine env pat in
   end_def ();
   generalize ty_var;
   ty_var
@@ -1708,7 +1710,7 @@ and type_pat_aux
   | Ppat_alias(sq, name) ->
       assert construction_not_used_in_counterexamples;
       type_pat Value sq expected_ty (fun q ->
-        let ty_var = solve_Ppat_alias env q in
+        let ty_var = solve_Ppat_alias ~refine env q in
         let id =
           enter_variable ~is_as_variable:true loc name ty_var sp.ppat_attributes
         in