import liquidjava.specification.*;

@StateSet(name = "phase", value = {"closed", "opened"})
@RefinementAlias("Closed(AliasState x) { closed(x) }")
public class AliasState {
    @StateRefinement(to = "closed(this)")
    public AliasState() {}

    @StateRefinement(from = "closed(this)", to = "opened(this)")
    public void open() {}

    static void needsClosed(@Refinement("Closed(_)") AliasState a) {}

    public static void main(String[] args) {
        AliasState a = new AliasState();
        needsClosed(a);
        a.open();
        needsClosed(a); // should fail
    }
}

Refinement Error: closed(a) is not a subtype of Closed(a)
  where Closed(x) = closed(x)