Skip to content
Permalink
Browse files

type_cases: decrease the sharing between the type of the scrutiny and…

… that of each pattern

See discussion on MPR#7618 .
We also add a late check of ambiguous type escape.
  • Loading branch information...
trefis committed Feb 12, 2018
1 parent 355a4bb commit d43ccfc5d48ce86202de3c7c4f58317602d6d417
@@ -128,7 +128,14 @@ let g1 (type a b) (x : (a, b) eq) =
| _, [(_ : b)] -> []
;;
[%%expect{|
val g1 : ('a, 'b) eq -> 'c list = <fun>
Line _, characters 2-77:
..match x, [] with
| Refl, [(_ : a) | (_ : b)] -> []
| _, [(_ : b)] -> []
Error: This pattern matches values of type (a, b) eq * b list
but a pattern was expected which matches values of type 'a
This instance of b is ambiguous:
it would escape the scope of its equation
|}]

let g2 (type a b) (x : (a, b) eq) =
@@ -152,7 +159,13 @@ let h1 (type a b) (x : (a, b) eq) =
| Refl, [(_ : a) | (_ : b)] -> []
;;
[%%expect{|
val h1 : ('a, 'b) eq -> 'c list = <fun>
Line _, characters 4-29:
| Refl, [(_ : a) | (_ : b)] -> []
^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This pattern matches values of type (a, b) eq * b list
but a pattern was expected which matches values of type
(a, b) eq * a list
Type b is not compatible with type a
|}]

let h2 (type a b) (x : (a, b) eq) =
@@ -161,7 +174,14 @@ let h2 (type a b) (x : (a, b) eq) =
| Refl, [(_ : a) | (_ : b)] -> []
;;
[%%expect{|
val h2 : ('a, 'b) eq -> 'c list = <fun>
Line _, characters 2-77:
..match x, [] with
| _, [(_ : b)] -> []
| Refl, [(_ : a) | (_ : b)] -> []
Error: This pattern matches values of type (a, b) eq * b list
but a pattern was expected which matches values of type 'a
This instance of b is ambiguous:
it would escape the scope of its equation
|}]

let h3 (type a b) (x : (a, b) eq) =
@@ -170,5 +190,11 @@ let h3 (type a b) (x : (a, b) eq) =
| Refl, [(_ : b) | (_ : a)] -> []
;;
[%%expect{|
val h3 : ('a, 'b) eq -> 'c list = <fun>
Line _, characters 4-29:
| Refl, [(_ : b) | (_ : a)] -> []
^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This pattern matches values of type (a, b) eq * b list
but a pattern was expected which matches values of type
(a, b) eq * a list
Type b is not compatible with type a
|}]
@@ -25,11 +25,13 @@ Line _, characters 2-54:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
(Refl, _::_::_)
Line _, characters 22-23:
Line _, characters 2-54:
..match x, [] with
| Refl, [(_ : a) | (_ : b)] -> []
^
Warning 12: this sub-pattern is unused.
val ok : ('a, 'b) eq -> 'c list = <fun>
Error: This pattern matches values of type (a, b) eq * b list
but a pattern was expected which matches values of type 'a
This instance of b is ambiguous:
it would escape the scope of its equation
|}]
let fails (type a b) (x : (a, b) eq) =
match x, [] with
@@ -44,15 +46,14 @@ Line _, characters 2-90:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
(Refl, _::_::_)
Line _, characters 22-23:
Line _, characters 2-90:
..match x, [] with
| Refl, [(_ : a) | (_ : b)] -> []
^
Warning 12: this sub-pattern is unused.
Line _, characters 4-29:
| Refl, [(_ : b) | (_ : a)] -> []
^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 11: this match case is unused.
val fails : ('a, 'b) eq -> 'c list = <fun>
Error: This pattern matches values of type (a, b) eq * b list
but a pattern was expected which matches values of type 'a
This instance of b is ambiguous:
it would escape the scope of its equation
|}]

(* branches must be unified! *)
@@ -21,13 +21,6 @@ Line _, characters 31-34:
Error: This pattern matches values of type [? `B ]
but a pattern was expected which matches values of type [ `A ]
The second variant type does not allow tag(s) `B
|}, Principal{|
Line _, characters 31-34:
let f x = ignore (match x with #ab -> 1); ignore (x : [`A]);;
^^^
Error: This pattern matches values of type [? `B ]
but a pattern was expected which matches values of type [ `A ]
Types for tag `B are incompatible
|}];;
let f x = ignore (match x with `A|`B -> 1); ignore (x : [`A]);;
[%%expect{|
@@ -37,13 +30,6 @@ Line _, characters 34-36:
Error: This pattern matches values of type [? `B ]
but a pattern was expected which matches values of type [ `A ]
The second variant type does not allow tag(s) `B
|}, Principal{|
Line _, characters 34-36:
let f x = ignore (match x with `A|`B -> 1); ignore (x : [`A]);;
^^
Error: This pattern matches values of type [? `B ]
but a pattern was expected which matches values of type [ `A ]
Types for tag `B are incompatible
|}];;

let f (x : [< `A | `B]) = match x with `A | `B | `C -> 0;; (* warn *)
@@ -4606,9 +4606,13 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
in
if !Clflags.principal then begin_def (); (* propagation of pattern *)
let scope = Some (Annot.Idef loc) in
begin_def ();
let ty_arg = instance ?partial:take_partial_instance ty_arg in
end_def ();
generalize_structure ty_arg;
let expected_ty_arg = instance ty_arg in
let (pat, ext_env, force, unpacks) =
let ty_arg = instance ?partial:take_partial_instance ty_arg in
type_pattern ~lev env pc_lhs scope ty_arg
type_pattern ~lev env pc_lhs scope expected_ty_arg
in
pattern_force := force @ !pattern_force;
let pat =
@@ -4618,16 +4622,18 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
{ pat with pat_type = instance pat.pat_type }
end else pat
in
(pat, (ext_env, unpacks)))
(pat, ty_arg, (ext_env, unpacks)))
caselist in
(* Unify all cases (delayed to keep it order-free) *)
let ty_arg' = newvar () in
let unify_pats ty =
List.iter (fun (pat, (ext_env, _)) -> unify_pat ext_env pat ty)
pat_env_list in
List.iter (fun (pat, pat_ty, _) ->
unify_pat_types pat.pat_loc env pat_ty ty
) pat_env_list
in
unify_pats ty_arg';
(* Check for polymorphic variants to close *)
let patl = List.map fst pat_env_list in
let patl = List.map (fun (pat, _, _) -> pat) pat_env_list in
if List.exists has_variants patl then begin
Parmatch.pressure_variants env patl;
List.iter (iter_pattern finalize_variant) patl
@@ -4647,7 +4653,7 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
let in_function = if List.length caselist = 1 then in_function else None in
let cases =
List.map2
(fun (pat, (ext_env, unpacks)) {pc_lhs; pc_guard; pc_rhs} ->
(fun (pat, _, (ext_env, unpacks)) {pc_lhs; pc_guard; pc_rhs} ->
let sexp = wrap_unpacks pc_rhs unpacks in
let ty_res' =
if !Clflags.principal then begin
@@ -4698,7 +4704,7 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
Partial
in
let unused_check () =
List.iter (fun (pat, (env, _)) -> check_absent_variant env pat)
List.iter (fun (pat, _, (env, _)) -> check_absent_variant env pat)
pat_env_list;
check_unused ~lev env (instance ty_arg_check) cases ;
Parmatch.check_ambiguous_bindings cases
@@ -4712,6 +4718,8 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
end_def ();
(* Ensure that existential types do not escape *)
unify_exp_types loc env (instance ty_res) (newvar ()) ;
(* Ensure that no ambivalent pattern type escapes its branch *)
unify_pat_types loc env ty_arg' (newvar ()) ;
end;
cases, partial

0 comments on commit d43ccfc

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