diff --git a/testsuite/tests/typing-gadts/ambiguity.ml b/testsuite/tests/typing-gadts/ambiguity.ml index 2d78347c9..5bdf9ba04 100644 --- a/testsuite/tests/typing-gadts/ambiguity.ml +++ b/testsuite/tests/typing-gadts/ambiguity.ml @@ -116,7 +116,7 @@ let f (type a b) (x : (a, b) eq) = Line 3, characters 4-29: | Refl, [(_ : a) | (_ : b)] -> [] ^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: +Error: This pattern matches values of type (a, b) eq * b list This instance of b is ambiguous: it would escape the scope of its equation |}] @@ -130,7 +130,7 @@ let g1 (type a b) (x : (a, b) eq) = Line 3, characters 4-29: | Refl, [(_ : a) | (_ : b)] -> [] ^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: +Error: This pattern matches values of type (a, b) eq * b list This instance of b is ambiguous: it would escape the scope of its equation |}] @@ -144,7 +144,7 @@ let g2 (type a b) (x : (a, b) eq) = Line 3, characters 4-29: | Refl, [(_ : b) | (_ : a)] -> [] ^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: +Error: This pattern matches values of type (a, b) eq * b list This instance of b is ambiguous: it would escape the scope of its equation |}] @@ -158,7 +158,7 @@ let h1 (type a b) (x : (a, b) eq) = Line 4, characters 4-29: | Refl, [(_ : a) | (_ : b)] -> [] ^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: +Error: This pattern matches values of type (a, b) eq * b list This instance of b is ambiguous: it would escape the scope of its equation |}] @@ -172,7 +172,7 @@ let h2 (type a b) (x : (a, b) eq) = Line 4, characters 4-29: | Refl, [(_ : a) | (_ : b)] -> [] ^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: +Error: This pattern matches values of type (a, b) eq * b list This instance of b is ambiguous: it would escape the scope of its equation |}] @@ -186,7 +186,7 @@ let h3 (type a b) (x : (a, b) eq) = Line 4, characters 4-29: | Refl, [(_ : b) | (_ : a)] -> [] ^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: +Error: This pattern matches values of type (a, b) eq * b list This instance of b is ambiguous: it would escape the scope of its equation |}] diff --git a/testsuite/tests/typing-gadts/pr7618.ml b/testsuite/tests/typing-gadts/pr7618.ml index 6df3290a4..27e319b47 100644 --- a/testsuite/tests/typing-gadts/pr7618.ml +++ b/testsuite/tests/typing-gadts/pr7618.ml @@ -22,7 +22,7 @@ type ('a, 'b) eq = Refl : ('a, 'a) eq Line 4, characters 4-29: | Refl, [(_ : a) | (_ : b)] -> [] ^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: +Error: This pattern matches values of type (a, b) eq * b list This instance of b is ambiguous: it would escape the scope of its equation |}] @@ -35,7 +35,7 @@ let fails (type a b) (x : (a, b) eq) = Line 3, characters 4-29: | Refl, [(_ : a) | (_ : b)] -> [] ^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: +Error: This pattern matches values of type (a, b) eq * b list This instance of b is ambiguous: it would escape the scope of its equation |}] diff --git a/typing/ctype.ml b/typing/ctype.ml index 1c4b0dc94..8b314c6bb 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -76,7 +76,7 @@ module Unification_trace = struct type 'a elt = | Diff of 'a diff | Variant of variant - | Escape of 'a escape + | Escape of {context:type_expr option; kind: 'a escape} | Incompatible_fields of {name:string; diff:type_expr diff } | Rec_occur of type_expr * type_expr @@ -91,9 +91,9 @@ module Unification_trace = struct let map_elt f = function | Diff x -> Diff (map_diff f x) - | Escape (Equation x) -> Escape (Equation(f x)) + | Escape {kind=Equation x; context} -> Escape {kind=Equation(f x); context} | Rec_occur (_,_) - | Escape (Univ _ | Self|Constructor _ | Module_type _ ) + | Escape {kind=(Univ _ | Self|Constructor _ | Module_type _ ); _} | Variant _ | Incompatible_fields _ as x -> x let map f = List.map (map_elt f) @@ -116,7 +116,8 @@ module Unification_trace = struct exception Unify of t - let scope_escape x = Unify[Escape (Equation (short x))] + let escape kind = Escape { kind; context = None} + let scope_escape x = Unify[escape (Equation (short x))] let rec_occur x y = Unify[Rec_occur(x, y)] let incompatible_fields name got expected = Incompatible_fields {name; diff={got; expected} } @@ -758,8 +759,11 @@ let check_scope_escape level ty = iter_type_expr aux ty end in + try aux ty; unmark_type ty + with Unify [Trace.Escape x] -> + raise Trace.(Unify[Escape { x with context = Some ty }]) let update_scope scope ty = let ty = repr ty in @@ -786,7 +790,7 @@ let rec update_level env level expand ty = link_type ty (!forward_try_expand_once env ty); update_level env level expand ty with Cannot_expand -> - raise Trace.(Unify [Escape(Constructor p)]) + raise Trace.(Unify [escape(Constructor p)]) end | Tconstr(_, _ :: _, _) when expand -> begin try @@ -798,7 +802,7 @@ let rec update_level env level expand ty = end | Tpackage (p, nl, tl) when level < Path.scope p -> let p' = normalize_package_path env p in - if Path.same p p' then raise Trace.(Unify [Escape (Module_type p)]); + if Path.same p p' then raise Trace.(Unify [escape (Module_type p)]); log_type ty; ty.desc <- Tpackage (p', nl, tl); update_level env level expand ty | Tobject(_, ({contents=Some(p, _tl)} as nm)) @@ -817,7 +821,7 @@ let rec update_level env level expand ty = iter_type_expr (update_level env level expand) ty | Tfield(lab, _, ty1, _) when lab = dummy_method && (repr ty1).level > level -> - raise Trace.(Unify [Escape Self]) + raise Trace.(Unify [escape Self]) | _ -> set_level ty level; (* XXX what about abbreviations in Tconstr ? *) @@ -1800,7 +1804,7 @@ let occur_univar env ty = match ty.desc with Tunivar u -> if not (TypeSet.mem ty bound) then - raise Trace.(Unify [Escape (Univ u)]) + raise Trace.(Unify [escape (Univ u)]) | Tpoly (ty, tyl) -> let bound = List.fold_right TypeSet.add (List.map repr tyl) bound in occur_rec bound ty @@ -1852,7 +1856,7 @@ let univars_escape env univar_pairs vl ty = if List.exists (fun t -> TypeSet.mem (repr t) family) tl then () else occur t | Tunivar u -> - if TypeSet.mem t family then raise Trace.(Unify [Escape(Univ u)]) + if TypeSet.mem t family then raise Trace.(Unify [escape(Univ u)]) | Tconstr (_, [], _) -> () | Tconstr (p, tl, _) -> begin try @@ -2012,7 +2016,7 @@ let reify env t = let path, t = create_fresh_constr ty.level o in link_type ty t; if ty.level < fresh_constr_scope then - raise Trace.(Unify [Escape (Constructor path)]) + raise Trace.(Unify [escape (Constructor path)]) | Tvariant r -> let r = row_repr r in if not (static_row r) then begin @@ -2025,7 +2029,7 @@ let reify env t = {r with row_fields=[]; row_fixed=true; row_more = t} in link_type m (newty2 m.level (Tvariant row)); if m.level < fresh_constr_scope then - raise Trace.(Unify [Escape (Constructor path)]) + raise Trace.(Unify [escape (Constructor path)]) | _ -> assert false end; iter_row iterator r diff --git a/typing/ctype.mli b/typing/ctype.mli index 859e46035..950f5be90 100644 --- a/typing/ctype.mli +++ b/typing/ctype.mli @@ -43,7 +43,7 @@ module Unification_trace: sig type 'a elt = | Diff of 'a diff | Variant of variant - | Escape of 'a escape + | Escape of {context: type_expr option; kind:'a escape} | Incompatible_fields of {name:string; diff: type_expr diff } | Rec_occur of type_expr * type_expr diff --git a/typing/printtyp.ml b/typing/printtyp.ml index 504e235c9..cd87cd2fe 100644 --- a/typing/printtyp.ml +++ b/typing/printtyp.ml @@ -1822,34 +1822,38 @@ let explain_variant = function | Trace.Incompatible_types_for s -> Some(dprintf "@,Types for tag `%s are incompatible" s) -let explain_escape = function +let explain_escape intro ctx e = + let pre = match ctx with + | None -> ignore + | Some ctx -> dprintf "@[%t@;<1 2>%a@]" intro type_expr ctx in + match e with | Trace.Univ Some u -> Some( - dprintf "@,The universal variable '%s would escape its scope" - u) + dprintf "%t@,The universal variable '%s would escape its scope" + pre u) | Trace.Univ None -> - Some(dprintf "@,An universal variable would escape its scope") + Some(dprintf "%t@,An universal variable would escape its scope" pre) | Trace.Constructor p -> Some( dprintf - "@,@[The type constructor@;<1 2>%a@ would escape its scope@]" - path p + "%t@,@[The type constructor@;<1 2>%a@ would escape its scope@]" + pre path p ) | Trace.Module_type p -> Some( dprintf - "@,@[The module type@;<1 2>%a@ would escape its scope@]" - path p + "%t@,@[The module type@;<1 2>%a@ would escape its scope@]" + pre path p ) | Trace.Equation (_,t) -> Some( - dprintf "@,@[This instance of %a is ambiguous:@ %s@]" - type_expr t + dprintf "%t @,@[This instance of %a is ambiguous:@ %s@]" + pre type_expr t "it would escape the scope of its equation" ) | Trace.Self -> - Some (dprintf "@,Self type cannot escape its class") + Some (dprintf "%t@,Self type cannot escape its class" pre) -let explanation env = function +let explanation intro env = function | Trace.Diff { Trace.got = _, s; expected = _,t } -> explanation_diff env s t - | Trace.Escape e -> explain_escape e + | Trace.Escape {kind;context} -> explain_escape intro context kind | Trace.Incompatible_fields { name; _ } -> Some(dprintf "@,Types for method %s are incompatible" name) | Trace.Variant v -> explain_variant v @@ -1858,11 +1862,11 @@ let explanation env = function Some(dprintf "@,@[The type variable %a occurs inside@ %a@]" type_expr x type_expr y) -let rec mismatch env = function +let rec mismatch intro env = function h :: rem -> - begin match mismatch env rem with + begin match mismatch intro env rem with Some _ as m -> m - | None -> explanation env h + | None -> explanation intro env h end | [] -> None @@ -1907,7 +1911,7 @@ let warn_on_missing_defs env ppf = function let unification_error env tr txt1 ppf txt2 ty_expect_explanation = reset (); let tr = Trace.flatten (fun t t' -> t, hide_variant_name t') tr in - let mis = mismatch env tr in + let mis = mismatch txt1 env tr in match tr with | [] -> assert false | elt :: tr -> @@ -1968,7 +1972,7 @@ let report_subtyping_error ppf env tr1 txt1 tr2 = let tr2 = Trace.flatten (fun t t' -> prepare_expansion (t, t')) tr2 in fprintf ppf "@[%a" (trace true (tr2 = []) txt1) tr1; if tr2 = [] then fprintf ppf "@]" else - let mis = mismatch env tr2 in + let mis = mismatch (dprintf "Within this type") env tr2 in fprintf ppf "%a%t%t@]" (trace false (mis = None) "is not compatible with type") tr2 (explain mis)