Skip to content

Strange constraints generated by GUT inference for type variable uses #81

Description

@AndrewShf

Testcase:

import universe.qual.*;

class Demo<T extends Box> {
    T f;
    void test() {
        f.v = new Object();
    }
}

class Box {
    Object v;
}

Using debug solver, we can know how varslot is inserted and constraints are generated.

class Demo<@VarAnnot(8) T extends @VarAnnot(9) Box> {
    @VarAnnot(7)
    T f;
    void test(@VarAnnot(15) Demo<@VarAnnot(16) T> this) {
        f.v = new @VarAnnot(20) Object();
    }
}

class Box {
    @VarAnnot(22)
    Object v;
}

Several constraints are questionable
18 = ( 15 ▷ 10: ( 7 | 9 ) )
19 = ( 15 ▷ 11: ( 7 | 8 ) )
20 <: 26
22 == 5 @ Rep weight = 80
23 = ( 10: ( 7 | 9 ) ▷ 22 )
24 != 3 @ Lost
24 = ( 10: ( 7 | 9 ) ▷ 23 )
25[ ↧ 24 ] == 20
26 = ( 10: ( 7 | 9 ) ▷ 25[ ↧ 24 ] )

this.f has viewpoint adaptation of the lower and upper bound, which is encoded by 19 = ( 15 ▷ 11: ( 7 | 8 ) ) and 18 = ( 15 ▷ 10: ( 7 | 9 ) ) respectively.

However, if 23 = ( 10: ( 7 | 9 ) ▷ 22 ) represents f.v, it's an incomplete viewpoint adaptation. it should use varslot 18 computed earlier for viewpoint adaptation, rather than varslot 10.

didn't understand why reuse varslot 10 to viewpoint adapt 23 again.

varslot 25 is the refinement variable, but why use that for viewpoint adaptation for varslot 26? Then there is a subtype constraint from 20 to 26 (which is likely to the the this.v = new object() assignment).

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions