Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

MPR7565 bis: more context for universal variable in error messages #2140

Merged
merged 4 commits into from Nov 24, 2018
Merged
Changes from 1 commit
Commits
File filter...
Filter file types
Jump to…
Jump to file or symbol
Failed to load files and symbols.

Always

Just for now

@@ -171,14 +171,16 @@ Working version
(Arthur Charguéraud and Armaël Guéneau, with help and advice
from Gabriel Scherer, Frédéric Bour, Xavier Clerc and Leo White)

- GPR#1733,1993,1998,2058,2094: Typing error message improvements
- GPR#1733,1993,1998,2058,2094,2140: Typing error message improvements
- GPR#1733, change the perspective of the unexpected existential error
message.
- GPR#1993, expanded error messages for universal quantification failure
- GPR#1998, more context for unbound type parameter error
- GPR#2058, full explanation for unsafe cycles in recursive module
definitions (suggestion by Ivan Gotovchits)
- GPR#2094, rewording for "constructor has no type" error
- MPR#7565, GPR#2140, more context for universal variable escape
in method type
(Florian Angeletti, reviews by Jacques Garrique, Gabriel Radanne,
Gabriel Scherer and Jeremy Yallop)

@@ -38,5 +38,48 @@ Line 4, characters 49-50:
^
Error: This expression has type < a : 'a; b : 'a >
but an expression was expected of type < a : 'a; b : 'a0. 'a0 >
The method b has type 'a, but the expected method type was 'a0. 'a0
The universal variable 'a0 would escape its scope
|}]


(** MPR 7565 *)
class type t_a = object
method f: 'a. 'a -> int
end
let f (o:t_a) = o # f 0
let _ = f (object
method f _ = 0
end);;
[%%expect {|
class type t_a = object method f : 'a -> int end
val f : t_a -> int = <fun>
Line 5, characters 10-42:
5 | ..........(object
6 | method f _ = 0
7 | end)..
Error: This expression has type < f : 'a -> int >
but an expression was expected of type t_a
The method f has type 'a -> int, but the expected method type was
'a0. 'a0 -> int
The universal variable 'a0 would escape its scope
|}
]

type uv = [ `A of <f: 'a. 'a -> int > ]
type 'a v = [ `A of <f: 'a -> int > ]
let f (`A o:uv) = o # f 0
let () = f ( `A (object method f _ = 0 end): _ v);;
[%%expect {|
type uv = [ `A of < f : 'a. 'a -> int > ]
type 'a v = [ `A of < f : 'a -> int > ]
val f : uv -> int = <fun>
Line 4, characters 11-49:
4 | let () = f ( `A (object method f _ = 0 end): _ v);;
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This expression has type 'a v but an expression was expected of type
uv
The method f has type 'a -> int, but the expected method type was
'a0. 'a0 -> int
The universal variable 'a0 would escape its scope
|}]
@@ -456,6 +456,8 @@ Line 9, characters 41-42:
^
Error: This expression has type < m : 'b. 'b -> 'b list >
but an expression was expected of type < m : 'b. 'b -> 'c >
The method m has type 'b. 'b -> 'b list,
but the expected method type was 'b. 'b -> 'c
The universal variable 'b would escape its scope
|}];;

@@ -1098,6 +1100,8 @@ Line 2, characters 3-4:
Error: This expression has type < m : 'a. 'a * < m : 'a * 'b > > as 'b
but an expression was expected of type
< m : 'a. 'a * (< m : 'a * < m : 'c. 'c * 'd > > as 'd) >
The method m has type 'a. 'a * 'd, but the expected method type was
'c. 'c * 'd
The universal variable 'a would escape its scope
|}];;

@@ -1721,16 +1721,37 @@ let rec trace fst txt ppf = function
(trace false txt) rem
| _ -> ()

let rec filter_trace keep_last = function
| Trace.(Diff ({ got=t1, t1'; expected=t2, t2'} as elt)) :: rem ->
let rem' = filter_trace keep_last rem in
let is_discarded is_last = function
| Trace.(Diff { got=t1, t1'; expected=t2, t2'}) ->
if is_constr_row ~allow_ident:true t1'
|| is_constr_row ~allow_ident:true t2'
|| same_path t1 t1' && same_path t2 t2' && not (keep_last && rem' = [])
then rem'
else elt :: rem'
| _elt :: rem -> filter_trace keep_last rem
| _ -> []
|| same_path t1 t1' && same_path t2 t2' && not is_last then
true
else false
This conversation was marked as resolved by Octachron

This comment has been minimized.

Copy link
@Armael

Armael Nov 18, 2018

Member

if b then true else false ~> b?

This comment has been minimized.

Copy link
@Octachron

Octachron Nov 24, 2018

Author Contributor

Fixed

| _ -> false

(** Flatten the trace and remove elements that are always discarded
during printing *)
let prepare_trace f tr =
let rec clean_trace = function
| [] -> []
| x :: q -> let rem = clean_trace q in
if is_discarded (rem=[]) x then rem
else x :: rem
in
match Trace.flatten f tr with
| [] -> []
| elt :: rem -> (* the first element is always kept *)
This conversation was marked as resolved by Armael

This comment has been minimized.

Copy link
@Armael

Armael Nov 23, 2018

Member

the first element is always kept why? Is this true in the current code? I couldn't find if this was true and why.

This comment has been minimized.

Copy link
@Octachron

Octachron Nov 23, 2018

Author Contributor

In the current code, both unification_trace and the second trace function take care to only apply filter_trace starting from the second element.

This comment has been minimized.

Copy link
@Armael

Armael Nov 23, 2018

Member

Ugh, indeed, I had not noticed that. Thanks.

elt :: clean_trace rem

(** Keep elements that are not [Diff _ ] and take the decision
for the last element, require a prepared trace *)

This comment has been minimized.

Copy link
@Armael

Armael Nov 23, 2018

Member

So, AFAIU, the semantics of filter_trace change a bit since it now requires a prepared trace, while previously it "prepared" the trace itself.

github doesn't seem to allow me to comment on the relevant lines directly, but I checked that the call sites of filter_trace satisfy this new precondition.

  • First one is in unification_error; the precondition is trivially satisfied by the call to prepare_trace a few lines above in the same function
  • Second one is in trace, and a bit less obvious. I have no idea what this function is doing, but it only seems to be called in report_subtyping_error, on traces that have been prepared. Maybe it would be good to write down that trace assumes that its input trace has been "prepared".
let rec filter_trace keep_last = function
| [] -> []
| [Trace.Diff d as elt] when is_discarded false elt ->

This comment has been minimized.

Copy link
@Armael

Armael Nov 23, 2018

Member

I find is_discarded false elt confusing. The name of the first argument of is_discarded is is_last, and you set it to false, but elt is the last element! At this point I'm a bit too confused to understand whether this line and the next one are actually correct, but I would think something like follows is more natural:

| [Trace.Diff d as elt] ->
  if is_discarded keep_last elt then [] else [d]

This comment has been minimized.

Copy link
@Octachron

Octachron Nov 23, 2018

Author Contributor

Maybe a more natural solution would be to make is_discarded returns a variant Discard | Keep_if_last | Keep then the previous line would be checking when is_discarded elt = Keep_if_last .

This comment has been minimized.

Copy link
@Octachron

Octachron Nov 24, 2018

Author Contributor

I went ahead with this solution.

if keep_last then [d] else []
| Trace.Diff d :: rem -> d :: filter_trace keep_last rem
| _ :: rem -> filter_trace keep_last rem

let type_path_list =
Format.pp_print_list ~pp_sep:(fun ppf () -> Format.pp_print_break ppf 2 0)
@@ -1809,10 +1830,15 @@ let explain_variant = function
| Trace.Incompatible_types_for s ->
Some(dprintf "@,Types for tag `%s are incompatible" s)

let explain_escape intro ctx e =
let explain_escape intro prev ctx e =
let pre = match ctx with
| None -> ignore
| Some ctx -> dprintf "@[%t@;<1 2>%a@]" intro type_expr ctx in
| Some ctx -> dprintf "@[%t@;<1 2>%a@]" intro type_expr ctx
| None -> match e, prev with
| Trace.Univ _, Some(Trace.Incompatible_fields {name; diff}) ->
dprintf "@,@[The method %s has type@ %a,@ \
but the expected method type was@ %a@]" name
type_expr diff.Trace.got type_expr diff.Trace.expected
| _ -> ignore in
match e with
| Trace.Univ u -> Some(
dprintf "%t@,The universal variable %a would escape its scope"
@@ -1846,9 +1872,9 @@ let explain_object = function
)


let explanation intro env = function
let explanation intro prev env = function
| Trace.Diff { Trace.got = _, s; expected = _,t } -> explanation_diff env s t
| Trace.Escape {kind;context} -> explain_escape intro context kind
| Trace.Escape {kind;context} -> explain_escape intro prev context kind
| Trace.Incompatible_fields { name; _ } ->
Some(dprintf "@,Types for method %s are incompatible" name)
| Trace.Variant v -> explain_variant v
@@ -1858,13 +1884,15 @@ let explanation intro env = function
Some(dprintf "@,@[<hov>The type variable %a occurs inside@ %a@]"
type_expr x type_expr y)

let rec mismatch intro env = function
h :: rem ->
begin match mismatch intro env rem with
Some _ as m -> m
| None -> explanation intro env h
end
| [] -> None
let mismatch intro env =
let rec mismatch intro prev env = function
h :: rem ->
begin match mismatch intro (Some h) env rem with
Some _ as m -> m
| None -> explanation intro prev env h
end
| [] -> None in
mismatch intro None env

let explain mis ppf =
match mis with
@@ -1906,7 +1934,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 tr = prepare_trace (fun t t' -> t, hide_variant_name t') tr in
let mis = mismatch txt1 env tr in
match tr with
| [] -> assert false
@@ -1964,8 +1992,8 @@ let trace fst keep_last txt ppf tr =
let report_subtyping_error ppf env tr1 txt1 tr2 =
wrap_printing_env ~error:true env (fun () ->
reset ();
let tr1 = Trace.flatten (fun t t' -> prepare_expansion (t, t')) tr1 in
let tr2 = Trace.flatten (fun t t' -> prepare_expansion (t, t')) tr2 in
let tr1 = prepare_trace (fun t t' -> prepare_expansion (t, t')) tr1 in
let tr2 = prepare_trace (fun t t' -> prepare_expansion (t, t')) tr2 in
let keep_first = match tr2 with
| Trace.[Obj _ | Variant _ | Escape _ ] | [] -> true
| _ -> false in
ProTip! Use n and p to navigate between commits in a pull request.
You can’t perform that action at this time.