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.

Sign up for GitHub

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

Jump to bottom

[abstracts] fix unify_with_variance for abstracts #9723

Merged
merged 1 commit into from Jul 17, 2020
Merged

[abstracts] fix unify_with_variance for abstracts #9723

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
87 changes: 56 additions & 31 deletions src/core/tUnification.ml
View file
Open in desktop
Expand Up @@ -295,6 +295,8 @@ let fast_eq_check type_param_check a b =

let rec fast_eq a b = fast_eq_check fast_eq a b

let fast_eq_pair (a,b) (a',b') = fast_eq a a' && fast_eq b b'

let rec fast_eq_unbound_mono a b =
match a, b with
| TMono { tm_type = None }, TMono { tm_type = None } -> true
Expand Down Expand Up @@ -480,8 +482,7 @@ let rec type_eq uctx a b =
| TType (t,tl) , _ when can_follow a ->
try_apply_params_rec t.t_params tl t.t_type (fun a -> type_eq uctx a b)
| _ , TType (t,tl) when can_follow b ->
rec_stack eq_stack (a,b)
(fun (a2,b2) -> fast_eq a a2 && fast_eq b b2)
rec_stack eq_stack (a,b) (fast_eq_pair (a,b))
(fun() -> try_apply_params_rec t.t_params tl t.t_type (type_eq uctx a))
(fun l -> error (cannot_unify a b :: l))
| TEnum (e1,tl1) , TEnum (e2,tl2) ->
Expand Down Expand Up @@ -881,10 +882,17 @@ and unify_anons uctx a b a1 a2 =
and does_func_unify f =
try f(); true with Unify_error _ -> false

and does_func_unify_arg f arg =
try f arg; true with Unify_error _ -> false

and get_abstract_context uctx a b ab =
if (Meta.has Meta.CoreType ab.a_meta) || (Meta.has Meta.Transitive ab.a_meta) then
uctx
else if uctx.allow_abstract_cast then
else
get_after_abstract_context uctx a b

and get_after_abstract_context uctx a b =
if uctx.allow_abstract_cast then
{uctx with allow_abstract_cast = false}
else
error [cannot_unify a b]
Expand All @@ -893,7 +901,7 @@ and get_nested_context uctx =
{uctx with allow_abstract_cast = true}

and unifies_with_abstract uctx a b f =
rec_stack_default abstract_cast_stack (a,b) (fun (a',b') -> fast_eq a a' && fast_eq b b') (fun() ->
rec_stack_default abstract_cast_stack (a,b) (fast_eq_pair (a,b)) (fun() ->
(uctx.allow_transitive_cast && f {uctx with allow_transitive_cast = false}) || f uctx
) false

Expand Down Expand Up @@ -968,37 +976,54 @@ and unifies_to_field uctx a b ab tl (t,cf) =
| _ -> die "" __LOC__)

and unify_with_variance uctx f t1 t2 =
let allows_variance_to t tf = type_iseq uctx tf t in
match follow t1,follow t2 with
let t1 = follow t1 in
let t2 = follow t2 in
let unify_param t1 t2 = with_variance (get_nested_context uctx) f t1 t2 in
let get_after_abstract_context () = get_after_abstract_context uctx t1 t2 in
let rec get_underlying_type t = match follow t with
| TAbstract(a,tl) ->
let tl = List.map get_underlying_type tl in
let t = apply_params a.a_params tl a.a_this in
if Meta.has Meta.CoreType a.a_meta then t else get_underlying_type t
| t -> t
in
let compare_underlying equality_kind a b = type_eq {uctx with equality_kind = equality_kind} a b in
let unifies_abstract uctx t ab tl ats =
List.exists (does_func_unify_arg (fun at ->
let at = apply_params ab.a_params tl at in
if ats == ab.a_to then
with_variance uctx f at t
else
with_variance uctx f t at
)) ats
in
let fail () = error [cannot_unify t1 t2] in
match t1,t2 with
| TInst(c1,tl1),TInst(c2,tl2) when c1 == c2 ->
List.iter2 f tl1 tl2
List.iter2 unify_param tl1 tl2
| TEnum(en1,tl1),TEnum(en2,tl2) when en1 == en2 ->
List.iter2 f tl1 tl2
| TAbstract(a1,tl1),TAbstract(a2,tl2) when a1 == a2 && Meta.has Meta.CoreType a1.a_meta ->
List.iter2 f tl1 tl2
| TAbstract(a1,pl1),TAbstract(a2,pl2) ->
if (Meta.has Meta.CoreType a1.a_meta) && (Meta.has Meta.CoreType a2.a_meta) then begin
let ta1 = apply_params a1.a_params pl1 a1.a_this in
let ta2 = apply_params a2.a_params pl2 a2.a_this in
type_eq {uctx with equality_kind = EqStrict} ta1 ta2;
end;
if not (List.exists (allows_variance_to t2) a1.a_to) && not (List.exists (allows_variance_to t1) a2.a_from) then
error [cannot_unify t1 t2]
| TAbstract(a,pl),t ->
type_eq {uctx with equality_kind = EqBothDynamic} (apply_params a.a_params pl a.a_this) t;
if not (List.exists (fun t2 -> allows_variance_to t (apply_params a.a_params pl t2)) a.a_to) then error [cannot_unify t1 t2]
| t,TAbstract(a,pl) ->
type_eq {uctx with equality_kind = EqBothDynamic} t (apply_params a.a_params pl a.a_this);
if not (List.exists (fun t2 -> allows_variance_to t (apply_params a.a_params pl t2)) a.a_from) then error [cannot_unify t1 t2]
| (TAnon a1 as t1), (TAnon a2 as t2) ->
rec_stack unify_stack (t1,t2)
(fun (a,b) -> fast_eq a t1 && fast_eq b t2)
(fun() -> unify_anons uctx t1 t2 a1 a2)
(fun l -> error l)
List.iter2 unify_param tl1 tl2
| TAbstract(a1,tl1),TAbstract(a2,tl2) when a1 == a2 ->
List.iter2 unify_param tl1 tl2
| TAbstract(a1,tl1),TAbstract(a2,tl2) ->
let uctx = get_after_abstract_context() in
compare_underlying EqStrict (get_underlying_type t1) (get_underlying_type t2);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looking at this I'm wondering why we do something with the underlying type here. I realize that the previous implementation already does this as well, but I can't immediately tell why.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess there might be two reasons:

  1. For static targets physical difference matters and so if you have Array<Int> you can't simply cast it to Array<Float>, even though Int defines to Float. Though allowed cast from/to dynamic in abstract-t/t-abstract contradicts this (if i understand it right).

  2. If you allow an abstract over a child with defined cast to a parent to unify with a parent in a type param, this will permit unchecked covariance.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But Array<Int> to Array<Float> has nothing to do with underlying types. Array is a normal class.

Shouldn't all this be covered by the to and from declarations? I don't see why the relationship of underlying types is significant here.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

About <Int> to <Float> - issue: #2844, commit: 6c22897. If underlying type checks are removed, only tests related to this fail.

But if we go only by tests, then underlying type checks can be skipped for t-abstract and abstract-t.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added commit with removal of underlying checks for abstract/non-abstract.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Removed that commit. Instead added assertions showcasing second reason (so first reason covers abstract-abstract, second one - abstract-t). Example here:

class Parent {}
class Child extends Parent {}
abstract MyChild(Child) to Parent {}

class Main {
  public static function main() {
    ((null: Array<Child>): Array<Parent>); // fails as expected
    ((null: Array<MyChild>): Array<Parent>); // works if no underlying type checks are made
  }
}

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the correct behavior here is to require bidirectional unification for type-parameters. This will then work when the abstract has to Parent from Parent, in which case there's no variance issue.

And then if we ever allow variance annotations on type parameters, we would only have to check one of the directions instead of both.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What about <Array> to <ReadOnlyArray>?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure, that looks like it shouldn't work without to Array<T>, but at the same time I don't see what harm it could do.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think those breaking changes will require more discussion and input...
In the meantime, i would prefer to fix bugs in current behaviour (and express it in tests).
Are there some considerations that prevent this from being merged?
Performance or complexity of code?

if not (unifies_abstract uctx t2 a1 tl1 a1.a_to) && not (unifies_abstract uctx t1 a2 tl2 a2.a_from) then fail();
| TAbstract(a,tl),_ ->
let uctx = get_after_abstract_context() in
compare_underlying EqBothDynamic (get_underlying_type t1) t2;
if not (unifies_abstract uctx t2 a tl a.a_to) then fail()
| _,TAbstract(a,tl) ->
let uctx = get_after_abstract_context() in
compare_underlying EqBothDynamic t1 (get_underlying_type t2);
if not (unifies_abstract uctx t1 a tl a.a_from) then fail()
| TAnon(a1),TAnon(a2) ->
rec_stack_default unify_stack (t1,t2) (fast_eq_pair (t1,t2)) (fun() -> unify_anons uctx t1 t2 a1 a2) ()
| _ ->
error [cannot_unify t1 t2]
fail()

and unify_type_params uctx a b tl1 tl2 =
let uctx = get_nested_context uctx in
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Technically, this uctx should not go into type_eq, but I don't think it makes a difference in the current implementation.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Question is why type_eq needs a unification context? I mean there is no need for it right now, but is there some idea for future property in the unification context that will be used both by unify and type_eq?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was contemplating merging type_eq and unify, but I've moved away from that idea. It's hard to tell if a unification context could be useful for it, so I wouldn't mind removing it again for now.

let i = ref 0 in
List.iter2 (fun t1 t2 ->
incr i;
Expand All @@ -1013,7 +1038,7 @@ and with_variance uctx f t1 t2 =
try
f t1 t2
with Unify_error l -> try
unify_with_variance uctx (with_variance uctx f) t1 t2
unify_with_variance uctx f t1 t2
with Unify_error _ ->
raise (Unify_error l)

Expand Down
40 changes: 40 additions & 0 deletions tests/unit/src/unit/issues/Issue9721.hx
View file
Open in desktop
@@ -0,0 +1,40 @@
package unit.issues;

class Issue9721 extends Test {
function test() {
((null: {x: Array<Array<Int>>}): {x: MyArray<Array<Int>>});
((null: {x: Array<Array<Int>>}): {x: Array<MyArray<Int>>});
((null: {x: Array<Array<Int>>}): {x: MyArray<MyArray<Int>>});

((null: {x: MyArray<Array<Int>>}): {x: Array<Array<Int>>});
((null: {x: Array<MyArray<Int>>}): {x: Array<Array<Int>>});
((null: {x: MyArray<MyArray<Int>>}): {x: Array<Array<Int>>});

((null: Array<Array<Array<Int>>>): MyArray<MyArray<MyArray<Int>>>);
((null: MyArray<MyArray<MyArray<Int>>>): Array<Array<Array<Int>>>);

((null: {x: Int}): {x: Foo<Int>});
((null: {x: Int}): {x: Bar<Int>});
((null: {x: Foo<Int>}): {x: Int});
((null: {x: Bar<Int>}): {x: Int});

((null: {x: String}): {x: Foo<String>});
((null: {x: String}): {x: Bar<String>});
((null: {x: Foo<String>}): {x: String});
((null: {x: Bar<String>}): {x: String});

t(unit.HelperMacros.typeError(((null: Array<Int>): Array<Float>)));
t(unit.HelperMacros.typeError(((null: Array<MyInt>): Array<Float>)));

t(unit.HelperMacros.typeError(((null: Array<Child>): Array<Parent>)));
t(unit.HelperMacros.typeError(((null: Array<MyChild>): Array<Parent>)));
}
}

private abstract MyArray<T>(Array<T>) from Array<T> to Array<T> {}
private abstract MyInt(Int) from Int to Int to Float {}
private abstract Foo<T>(T) from T to T {}
private abstract Bar<T>(Foo<T>) from T to T {}
private class Parent {}
private class Child extends Parent {}
private abstract MyChild(Child) to Parent {}