Skip to content
Permalink
Browse files

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

…2140)

This PR is a follow-up of #1212, it proposes to give more context for universal type variables that escape their scope when unifying methods, by precising the actual type and expected type at the method level, as suggested by @garrigue in #1212 .
  • Loading branch information...
Octachron authored and Armael committed Nov 24, 2018
1 parent ef4f76b commit 385223e007724af6bdd2210b3d978ff7f1d24f7c
Showing with 116 additions and 27 deletions.
  1. +5 −3 Changes
  2. +43 −0 testsuite/tests/typing-poly/error_messages.ml
  3. +4 −0 testsuite/tests/typing-poly/poly.ml
  4. +64 −24 typing/printtyp.ml
@@ -212,16 +212,18 @@ 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
(Florian Angeletti, reviews by Jacques Garrique, Gabriel Radanne,
Gabriel Scherer and Jeremy Yallop)
- MPR#7565, GPR#2140, more context for universal variable escape
in method type
(Florian Angeletti, reviews by Jacques Garrique, Armaël Guéneau,
Gabriel Radanne, Gabriel Scherer and Jeremy Yallop)

- GPR#1748: do not error when instantiating polymorphic fields in patterns.
(Thomas Refis, review by Gabriel Scherer)
@@ -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,49 @@ let rec trace fst txt ppf = function
(trace false txt) rem
| _ -> ()


type printing_status =
| Discard
| Keep
| Optional_refinement
(** An [Optional_refinement] printing status is attributed to trace
elements that are focusing on a new subpart of a structural type.
Since the whole type should have been printed earlier in the trace,
we only print those elements if they are the last printed element
of a trace, and there is no explicit explanation for the
type error.
*)

let printing_status = function
| Trace.(Diff { got=t1, t1'; expected=t2, t2'}) ->
if is_constr_row ~allow_ident:true t1'
|| is_constr_row ~allow_ident:true t2'
then Discard
else if same_path t1 t1' && same_path t2 t2' then Optional_refinement
else Keep
| _ -> Keep

(** Flatten the trace and remove elements that are always discarded
during printing *)
let prepare_trace f tr =
let clean_trace x l = match printing_status x with
| Keep -> x :: l
| Optional_refinement when l = [] -> [x]
| Optional_refinement | Discard -> l
in
match Trace.flatten f tr with
| [] -> []
| elt :: rem -> (* the first element is always kept *)
elt :: List.fold_right clean_trace rem []

(** Keep elements that are not [Diff _ ] and take the decision
for the last element, require a prepared trace *)
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
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
| _ -> []
| [] -> []
| [Trace.Diff d as elt] when printing_status elt = Optional_refinement ->
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 +1842,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 +1884,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 +1896,14 @@ 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 trace =
let rec mismatch intro env = function
| [] -> None
| [h] -> explanation intro None env h
| h :: (prev :: _ as rem) -> match explanation intro (Some prev) env h with
| Some _ as m -> m
| None -> mismatch intro env rem in
mismatch intro env (List.rev trace)

let explain mis ppf =
match mis with
@@ -1906,7 +1945,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
@@ -1942,6 +1981,7 @@ let report_unification_error ppf env tr
~error:true
;;
(** [trace] requires the trace to be prepared *)
let trace fst keep_last txt ppf tr =
print_labels := not !Clflags.classic;
try match tr with
@@ -1964,8 +2004,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

0 comments on commit 385223e

Please sign in to comment.
You can’t perform that action at this time.