Add context for unification errors
parent
3de40984ba
commit
233d66611c
|
@ -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
|
||||
|}]
|
||||
|
|
|
@ -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
|
||||
|}]
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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 "@,@[<hov>This instance of %a is ambiguous:@ %s@]"
|
||||
type_expr t
|
||||
dprintf "%t @,@[<hov>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 "@,@[<hov>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 "@[<v>%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)
|
||||
|
|
Loading…
Reference in New Issue